-- Sam Staton -- Demo for the Categorical Logic Course, ACS. -- Last modified 2010-1-25 module ProductsSumsDemo where open import ProductsSums open _×_ -- The terminal object is I . -- Base types are A B C. -- To get the × symbol, use backslash-x . -- To get an arrow, you can either type -> or backslash-r -- To get a lambda, type backslash-G-l, or just use backslash-backslash -- In emacs, load and typecheck the file by typing C-c C-l -- two examples of the unit type f1 : I -> I f1 x = x f1' : I -> I f1' x = * -- an example using products f2 : A × B -> B × A f2 p = (pi2 p , pi1 p) f2' : B × A -> A × B f2' p = (pi2 p , pi1 p) -- you can use agda to check that you have defined isomorphisms f2iso : (p : A × B) -> f2' (f2 p) == p f2iso p = refl f2iso' : (p : B × A) -> f2 (f2' p) == p f2iso' p = refl f3 : A -> A × I f3 a = (a , *) -- an example with function spaces f4 : (A -> B) -> A -> (A × B) f4 h = \a -> (a , h a) -- some examples of the empty type f5 : (O -> A) -> I f5 f = * f5' : I -> (O -> A) f5' x = absurd f5iso : (h : O -> A) -> (o : O) -> (f5' (f5 h)) o == h o f5iso h () f5iso' : (x : I) -> f5 (f5' x) == x f5iso' x = refl