-- This file:
--   http://angg.twu.net/AGDA/GLT.agda.html
--   http://angg.twu.net/AGDA/GLT.agda
--           (find-angg "AGDA/GLT.agda")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (find-books "__logic/__logic.el" "girard")
-- (find-proofsandtypespage (+ 8 81) "11 System F")
-- (find-proofsandtypespage (+ 8 81) "11.1 The calculus")
-- (find-proofsandtypespage (+ 8 82) "11.2 Comments")
-- (find-proofsandtypespage (+ 8 83) "11.3 Representation of simple types")
-- (find-proofsandtypespage (+ 8 83) "11.3.1 Booleans")
-- (find-proofsandtypespage (+ 8 83) "11.3.2 Product of types")
-- (find-proofsandtypespage (+ 8 84) "11.3.3 Empty type")
-- (find-proofsandtypespage (+ 8 84) "11.3.4 Sum type")
-- (find-proofsandtypespage (+ 8 85) "11.3.5 Existential type")
-- (find-proofsandtypespage (+ 8 85) "11.4 Representation of a free structure")
-- (find-proofsandtypespage (+ 8 86) "11.4.1 Free structure")
-- (find-proofsandtypespage (+ 8 87) "11.4.2 Representation of the constructors")
-- (find-proofsandtypespage (+ 8 87) "11.4.3 Induction")
-- (find-proofsandtypespage (+ 8 88) "11.5 Representation of inductive types")
-- (find-proofsandtypespage (+ 8 88) "11.5.1 Integers")
-- (find-proofsandtypespage (+ 8 90) "11.5.2 Lists")
-- (find-proofsandtypespage (+ 8 92) "11.5.3 Binary trees")
-- (find-proofsandtypespage (+ 8 92) "11.5.4 Trees of branching type U")

-- (sysfp 1 "bool-and-prod")
-- (sysfa   "bool-and-prod")

import Level
ℓ₁ : Level.Level
ℓ₁ = Level.suc Level.zero
ℓ₂ : Level.Level
ℓ₂ = Level.suc ℓ₁
ℓ₃ : Level.Level
ℓ₃ = Level.suc ℓ₂


GBool  : Set₁
GBool  = (A : Set) -> A -> A -> A
GTrue  : GBool
GTrue  A a₁ a₂ = a₁
GFalse : GBool
GFalse A a₁ a₂ = a₂

GD : {U : Set} -> (u : U) -> (v : U) -> (t : GBool) -> U
GD {U} u v t = t U u v


GProd : (U : Set) -> (V : Set) -> Set₁
GProd U V = {X : Set} -> (U -> V -> X) -> X

-- Gpair {U V : Set} 
-- Gpair {U} {V} u v = {X : Set} 

variable A B : Set

foo : A -> A
foo = λ a -> a




-- Local Variables:
-- coding:  utf-8-unix
-- End: