From b72fc4238acab69838be5967e3ab88597c132b65 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 31 Dec 2015 08:15:53 +0100 Subject: [PATCH] update aim.ctt --- examples/aim.ctt | 309 +++++++++++++++++++++++++++++++---------------- 1 file changed, 202 insertions(+), 107 deletions(-) diff --git a/examples/aim.ctt b/examples/aim.ctt index 64fbe68..4635e41 100644 --- a/examples/aim.ctt +++ b/examples/aim.ctt @@ -11,7 +11,7 @@ Experimental implementation of a type theory in which the user can directly manipulate n-dimensional cubes. It is based on a model of type theory in cubical sets with connections. The goal is to have a type theory with well behaved identity types and to give a -computational interpretation of notions from HoTT/UF, in particular +computational interpretation of notions from UF/HoTT, in particular the univalence axiom and higher inductive types. The system is based on Mini-TT: "A simple type-theoretic language: @@ -29,7 +29,6 @@ types. cubiclaltt extends Mini-TT with: Try it: https://github.com/mortberg/cubicaltt -Note: At the moment one should use the no_regular branch. -} @@ -48,7 +47,6 @@ not : bool -> bool = split false -> true true -> false - {- Identity types, names and formulas -------------------------------------------------------------------------- @@ -76,7 +74,6 @@ Id (A : U) (a b : A) : U = IdP ( A) a b -- "" abstracts the name/color/dimension i: refl (A : U) (a : A) : Id A a a = a - {- A proof "p : Id A a b" is thought of as a line between a and b: @@ -116,7 +113,7 @@ cong (A B : U) (f : A -> B) (a b : A) (p : Id A a b) : Id B (f a) (f b) = -- This also gives a short proof of function extensionality: funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) (p : (x : A) -> Id (B x) (f x) (g x)) : Id ((y : A) -> B y) f g = - \(a : A) -> (p a) @ i + \(x : A) -> (p x) @ i {- @@ -224,14 +221,33 @@ testConj (A : U) (a b : A) (p : Id A a b) : Id A a a = p @ i /\ -i testDisj (A : U) (a b : A) (p : Id A a b) : Id A b b = p @ i \/ -i + +{- + +So far we have: MLTT + Id, , @, i/\j... + +We can prove that singletons are contractible. But, we don't have +transport: + +transportf (A : U) (P : A -> U) (a b : A) (p : Id A a b) : P a -> P b + +Which is what is needed to get J as: + + J = contr. singl. + transport + +In order to get this (and a lot more) we consider compositions. + +-} + + + + + + {- Compositions ------------------------------------------------------------------------ -Given a cube, we form a new cube by replacing some faces along -equalities. This can be seen a generalization of composition of -relations. - The comp operation takes a line in the universe, a principal side and a system describing the rest of the shape, and produces the missing side (opposite of the principal side). @@ -239,12 +255,13 @@ side (opposite of the principal side). Transitivity of Id is obtained from a composition of this open square: +i : I, j : I |- a - - - - - - - - > c ^ ^ | | | | - a | | q + (<_> a)@j| | q @ j | | | | | | @@ -252,15 +269,19 @@ Transitivity of Id is obtained from a composition of this open square: p @ i The composition computes the dashed line at the top of the square. + ( (<_>a)@i ) = ( (<_>a)@j) : Id (Id A a a) ( a) ( a) + +p = p @ i +i : I |- (<_>a) @i +|- (<_> a) @ i +|- <_> a -} -trans (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = - comp (<_> A) (p @ i) [ (i = 0) -> a, (i = 1) -> q ] --- "Kan composition": -kan (A : U) (a b c d : A) (p : Id A a b) - (q : Id A a c) (r : Id A b d) : Id A c d = - comp (<_> A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] + +pathscomp0 (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = + comp (<_> A) (p @ i) [ (i = 0) -> <_> a + , (i = 1) -> q ] -- The first two nonzero h-levels are propositions and sets: @@ -310,6 +331,26 @@ constSquare (A : U) (a : A) (p : Id A a a) : Square A a a a a p p p p = +-- The first argument to comp is a line in the universe. So far we +-- have only considered constant lines.. + +-- "Kan composition": +kan (A : U) (a b c d : A) (p : Id A a b) + (q : Id A a c) (r : Id A b d) : Id A c d = + comp (<_> A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] + +-- Generalized Kan composition: +kan' (A B : U) (P : Id U A B) (a b : A) (c d : B) (p : Id A a b) + (q : IdP P a c) (r : IdP P b d) : Id B c d = + comp P (p @ i) [ (i = 0) -> q, (i = 1) -> r ] + +kan'' (A : U) (a b c d : A) (p : Id A a b) + (q : Id A a c) (r : Id A b d) : Id A c d = + kan' A A (<_> A) a b c d p q r + + + + -- Names and compisitions provides a convenient way for reasoning with -- equalities: @@ -338,6 +379,8 @@ addAssoc (a b : nat) : (c : nat) -> Id nat (add a (add b c)) (add (add a b) c) = suc c' -> suc (addAssoc a b c' @ i) + + {- Transport -------------------------------------------------------------------------- @@ -347,15 +390,22 @@ function from A to B: transport : Id U A B -> A -> B -It is defined internally as a composition with an empty cube/system. - -} --- This gives a simple proof of subst: +-- This gives a simple proof of subst (called transportf above and in +-- UniMath): subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b = - transport (cong A U P a b p) e + transport (maponpaths A U P a b p) e + + +-- Transport is defined in the Haskell code as a composition with an +-- empty cube/system. It can also be directly defined as: +trans (A B : U) (p : Id U A B) (a : A) : B = comp p a [] + +-- However these are not exactly the same because the lack of implicit +-- arguments. --- Combined with the fact that singletons are contractible this gives +-- subst with the fact that singletons are contractible this gives -- the J eliminator: J (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p = @@ -371,35 +421,74 @@ J (A : U) (a : A) (C : (x : A) -> Id A a x -> U) -- defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) : -- Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d +-- We can get the equality between a and the transport of a by filling: +transFill (A : U) (a : A) : Id A a (transport (<_> A) a) = + fill (<_> A) a [] + + -- This might not be too bad though. Nils-Anders Danielsson has -- verified in Agda that many of the consequences of univalence can be -- developed without defEqJ. +-- We used to have a system where defEqJ was definitional, however it +-- relied on a condition called "regularity" which Dan Licata showed to +-- not hold for the universe (at least for the way we define +-- composition in the universe). + +-- A "strange" term showing what happens without regularity +-- strange (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : +-- Id A (comp (<_> A) a []) c = +-- comp (<_> A) (p @ i) [ (i = 1) -> q ] + + + +-- It seems like we can recover a new Id type with the correct +-- definitional equalities using ideas from awfs of Andrew +-- Swan... Simon has implemented this in the branch "defeq". + + + + + + + + + {- - Glueing --------------------------------------------------------------------------- -The univalence axiom says that equivalent (written as ~) types are -equal: +So far we have: MLTT + Id, , @, i/\j, compositions, transport - (A = B) ~ (A ~ B) +With all of this we get J, but so far without def. eq. + +We also want univalence and HITs. + +-} + + + + + + +{- + Glueing +-------------------------------------------------------------------------- -Glueing is a weaker form of this for producing non-trivial equalities -from isomorphisms. In particular glueing gives a map from Iso(A,B) to -A = B. This weak form of univalence is useful for developing a lot of -examples. +Glueing is a alternative form of univalence for producing non-trivial +equalities from isomorphisms. In particular glueing gives a map from +Iso(A,B) to A = B. This alternative form of univalence is useful for +developing a lot of examples. -} + isoId (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Id B (f (g y)) y) (t : (x : A) -> Id A (g (f x)) x) : Id U A B = glue A [ (i = 0) -> (A,idfun A,idfun A,refl A,refl A) , (i = 1) -> (B,g,f,t,s) ] --- Note that we have to glue the identity isomorphism to (i = 0), this --- is because lack of regularity. Compare with trans. + --------------------------------------------------------- @@ -418,6 +507,11 @@ notEq : Id U bool bool = isoId bool bool not not notK notK testFalse : bool = transport notEq true + + + + + --------------------------------------------------- -- Example: Non-trivial equality between Z and Z -- --------------------------------------------------- @@ -479,30 +573,19 @@ testOneZ : Z = transport sucIdZ zeroZ testNOneZ : Z = transport ( sucIdZ @ - i) zeroZ - ----------------------------------- - -- Example: Equality in pi types -- - ----------------------------------- +-- transport sucIdZ = sucZ ? + + + + +----------------------------------------------------------------- +-- Using glue we get a proof of univalence, see univalence.ctt -- + + + -pi (A : U) (P : A -> U) : U = (x : A) -> P x --- Equality in pi types: -idPi (A : U) (B : A -> U) (f g : pi A B) : - Id U (Id (pi A B) f g) ((x : A) -> Id (B x) (f x) (g x)) = - isoId (Id (pi A B) f g) ((x : A) -> Id (B x) (f x) (g x)) F G S T - where T0 : U = Id (pi A B) f g - T1 : U = (x : A) -> Id (B x) (f x) (g x) - F (p : T0) : T1 = \(x : A) -> (p @ i) x - G (p : T1) : T0 = \(x : A) -> (p x) @ i - S (p : T1) : Id T1 (F (G p)) p = p - T (p : T0) : Id T0 (G (F p)) p = p --- If B is a family of sets then pi A B is a set: -setPi (A : U) (B : A -> U) (h : (x : A) -> set (B x)) : set (pi A B) = - \(f g : pi A B) -> - let T : U = (x : A) -> Id (B x) (f x) (g x) - rem : prop T = - \(p q : T) -> \(x : A) -> h x (f x) (g x) (p x) (q x) @ i - in subst U prop T (Id (pi A B) f g) ( idPi A B f g @ -i) rem @@ -516,6 +599,66 @@ generalize normal inductive types by allowing constructors that define -} + + ------------------------------------ + -- Example: The integers as a HIT -- + ------------------------------------ + +{- + +There is a minor issue with the definition of Z: the negative numbers +are off by one. + +What we really want is the equality "inl zero = inr zero". + +Solution: Define the integers as a HIT! + +-} + +data int = pos (n : nat) + | neg (n : nat) + | zeroP [ (i = 0) -> pos zero + , (i = 1) -> neg zero ] + +-- Nice version of the zero constructor: +zeroPath : Id int (pos zero) (neg zero) = zeroP {int} @ i + +sucInt : int -> int = split + pos n -> pos (suc n) + neg n -> sucNat n + where sucNat : nat -> int = split + zero -> pos one + suc n -> neg n + zeroP @ i -> pos one + +toZ : int -> Z = split + pos n -> inr n + neg n -> auxToZ n + where auxToZ : nat -> Z = split + zero -> inr zero + suc n -> inl n + zeroP @ i -> inr zero + +fromZ : Z -> int = split + inl n -> neg (suc n) + inr n -> pos n + +toZK : (a : Z) -> Id Z (toZ (fromZ a)) a = split + inl n -> inl n + inr n -> inr n + +fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split + pos n -> pos n + neg n -> rem n + where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split + zero -> zeroPath + suc m -> neg (suc m) + zeroP @ i -> zeroPath @ i /\ j -- A connection makes this proof easy! + +isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK + + + ---------------------------------- -- Example: The circle as a HIT -- ---------------------------------- @@ -528,7 +671,7 @@ loopS1 : U = Id S1 base base -- The loop constructor loop1 : loopS1 = loop{S1} @ i -invLoop : loopS1 = sym S1 base base loop1 +invLoop : loopS1 = loop1 @ -i helix : S1 -> U = split base -> Z @@ -538,7 +681,7 @@ helix : S1 -> U = split winding (p : loopS1) : Z = transport ( helix (p @ i)) zeroZ -- Loop composition: -compS1 : loopS1 -> loopS1 -> loopS1 = trans S1 base base base +compS1 : loopS1 -> loopS1 -> loopS1 = pathscomp0 S1 base base base -- Some examples of winding numbers: loopZ1 : Z = winding loop1 @@ -561,6 +704,8 @@ square (x : S1) : S1 = mult x x doubleLoop (l : loopS1) : loopS1 = square (l @ i) +doubleLoop' (l : loopS1) : loopS1 = compS1 l l + loopZ4 : Z = winding (doubleLoop (compS1 loop1 loop1)) loopZ8 : Z = winding (doubleLoop (doubleLoop (compS1 loop1 loop1))) @@ -570,66 +715,16 @@ hmtpy : Id loopS1 ( base) ( loop{S1} @ (i /\ -i)) = loop{S1} @ j /\ i /\ -i - ------------------------------------ - -- Example: The integers as a HIT -- - ------------------------------------ - -{- - -There is a minor issue with the definition of Z: the negative numbers -are off by one. - -What we really want is the equality "inl zero = inr zero". - -Solution: Define the integers as a HIT! --} - -data int = pos (n : nat) - | neg (n : nat) - | zeroP [ (i = 0) -> pos zero, (i = 1) -> neg zero ] - --- Nice version of the zero constructor: -zeroZ : Id int (pos zero) (neg zero) = zeroP {int} @ i - -sucInt : int -> int = split - pos n -> pos (suc n) - neg n -> sucNat n - where sucNat : nat -> int = split - zero -> pos one - suc n -> neg n - zeroP @ i -> pos one +-------------------------------------------------------------------------- +-- For a higher dimensional HIT see, torus.ctt -toZ : int -> Z = split - pos n -> inr n - neg n -> auxToZ n - where auxToZ : nat -> Z = split - zero -> inr zero - suc n -> inl n - zeroP @ i -> inr zero -fromZ : Z -> int = split - inl n -> neg (suc n) - inr n -> pos n -toZK : (a : Z) -> Id Z (toZ (fromZ a)) a = split - inl n -> inl n - inr n -> inr n -fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split - pos n -> pos n - neg n -> rem n - where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split - zero -> zeroZ - suc m -> neg (suc m) - zeroP @ i -> zeroZ @ i /\ j -- A connection makes this proof easy! -isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK --- This is proved in the library but admitted here: -ZSet : set Z = undefined -intSet : set int = subst U set Z int isoIntZ ZSet {- -- 2.34.1