--- /dev/null
+module aim where
+
+{-
+ cubicaltt: Cubical type theory
+--------------------------------------------------------------------------
+ (j.w.w. Cyril Cohen, Thierry Coquand, Simon Huber)
+
+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
+the univalence axiom and higher inductive types.
+
+The system is based on Mini-TT: "A simple type-theoretic language:
+Mini-TT" by Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström and
+Makoto Takeya.
+
+Mini-TT is a variant Martin-Löf type theory with data
+types. cubiclaltt extends Mini-TT with:
+
+ o Name abstraction and application
+ o Compositions
+ o Isomorphisms can be transformed into equalities
+ o Some higher inductive types
+
+
+Try it: https://github.com/mortberg/cubicaltt
+
+Note: At the moment one should use the no_regular branch.
+
+-}
+
+ ------------------------------------------
+ -- Some examples of programs in Mini-TT --
+ ------------------------------------------
+
+-- The identity function:
+idfun (A : U) (a : A) : A = a
+
+-- The booleans:
+data bool = false
+ | true
+
+not : bool -> bool = split
+ false -> true
+ true -> false
+
+
+{-
+ Identity types, names and formulas
+--------------------------------------------------------------------------
+
+An element in ID A B is a line in the universe connecting A and B:
+
+
+ |- A Type |- B Type
+ ------------------------------
+ |- ID A B Type
+
+
+IdP is heterogeneous equality:
+
+
+ |- P : ID A B |- a : A |- b : B
+ -----------------------------------------------
+ |- IdP P a b Type
+
+-}
+
+-- The usual identity can be seen a special case of IdP:
+Id (A : U) (a b : A) : U = IdP (<i> A) a b
+
+-- "<i>" abstracts the name/color/dimension i:
+refl (A : U) (a : A) : Id A a a = <i> a
+
+
+{-
+
+A proof "p : Id A a b" is thought of as a line between a and b:
+
+ p
+ a ------> b
+
+
+A proof "sq : Id (Id A a b) p q" is thought of as a square between p and q:
+
+
+ q
+ a ------> b
+ ^ ^
+ | sq |
+ | |
+ a ------> b
+ p
+
+
+And so on...
+
+-}
+
+
+-- It is possible to take the face of a path to obtain its endpoints:
+face0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
+face1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
+
+
+-- By applying a path to a name i, "p @ i", it is seen as a path "in
+-- dimension i" connecting "p @ 0" to "p @ 1". This way we get a
+-- simple proof of cong:
+cong (A B : U) (f : A -> B) (a b : A) (p : Id A a b) : Id B (f a) (f b) =
+ <i> f (p @ i)
+
+-- 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 =
+ <i> \(a : A) -> (p a) @ i
+
+-- To see the definition of funExt makes sense we can compute its faces:
+--
+-- funExt @ 0 = \(a : A) -> (p a) @ 0 (faces commute with operations)
+-- = \(a : A) -> f a (p a proves Id (B a) (f a) (g a))
+-- = f (by eta)
+
+
+{-
+
+Paths can be applied to formulas in the free distributive lattice
+generated by names i,j,k... and negated names -i,-j,-k...
+
+A grammar for formulas is:
+
+name := i,j,k...
+
+formula := formula /\ formula
+ | formula \/ formula
+ | name
+ | - name
+ | 0
+ | 1
+
+An intuition is that the names range between [0,1] and that i /\ j is
+min(i,j), i \/ j is max(i,j) and -i is 1 - i.
+
+-}
+
+-- Applying a path to a negated name inverts it:
+sym (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
+
+-- This operation is an involution:
+symK (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p p =
+ refl (Id A a b) (sym A b a (sym A a b p))
+
+
+{- Connections:
+
+Applying a path to a conjunction:
+
+
+ p @ i
+ a ----------------> b
+ ^ ^
+ | |
+ | |
+ p @ 0 | p @ i /\ j | p @ j
+ | |
+ | |
+ | |
+ a ----------------> a
+ p @ 0
+
+
+
+And a disjunction gives:
+
+ p @ 1
+ b ----------------> b
+ ^ ^
+ | |
+ | |
+ p @ j | p @ i \/ j | p @ 1
+ | |
+ | |
+ | |
+ a ----------------> b
+ p @ i
+
+-}
+
+
+-- This gives a simple proof that singletons are contractible:
+
+singl (A : U) (a : A) : U = (x : A) * Id A a x
+
+contrSingl (A : U) (a b : A) (p : Id A a b) :
+ Id (singl A a) (a,refl A a) (b,p) =
+ <i> (p @ i, <j> p @ i /\ j)
+
+
+{-
+
+Note that formulas does not form a boolean algebra, but a de Morgan
+algebra. This means that "p @ 0" and "p @ i /\ -i" are different!
+
+testDeMorganAlgebra (A : U) (a b : A) (p : Id A a b) :
+ Id (Id A a a) (<_> p @ 0) (<_> p @ 0) =
+ refl (Id A a a) (<i> p @ i /\ -i)
+
+This is clear with the intuition that /\ correspond to min. More about
+this later...
+
+-}
+
+testConj (A : U) (a b : A) (p : Id A a b) : Id A a a = <i> p @ i /\ -i
+testDisj (A : U) (a b : A) (p : Id A a b) : Id A b b = <i> p @ i \/ -i
+
+
+{-
+ 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).
+
+
+Transitivity of Id is obtained from a composition of this open square:
+
+
+ a - - - - - - - - > c
+ ^ ^
+ | |
+ | |
+ <j> a | | q
+ | |
+ | |
+ | |
+ a ----------------> b
+ p @ i
+
+The composition computes the dashed line at the top of the square.
+
+-}
+trans (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
+ <i> comp (<_> A) (p @ i) [ (i = 0) -> <j> 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 =
+ <i> comp (<_> A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
+
+
+-- The first two nonzero h-levels are propositions and sets:
+prop (A : U) : U = (a b : A) -> Id A a b
+set (A : U) : U = (a b : A) -> prop (Id A a b)
+
+-- Using compositions we get a short proof that any prop is a set. To
+-- understand this proof one should draw an open cube with the back
+-- face being a constant square in a and the sides given by the system
+-- below.
+propSet (A : U) (h : prop A) : set A =
+ \(a b : A) (p q : Id A a b) ->
+ <i j> comp (<_> A) a [ (j=0) -> h a a
+ , (j=1) -> h a b
+ , (i=0) -> h a (p @ j)
+ , (i=1) -> h a (q @ j)]
+
+-- From this we get a short proof that the type of propositions is a
+-- proposition. Note that this uses a binary form of funext.
+propIsProp (A : U) : prop (prop A) =
+ \(f g : prop A) ->
+ <i> \(a b : A) -> (propSet A f a b (f a b) (g a b)) @ i
+
+{-
+
+We can also define the type of squares:
+
+ u
+ a0 -----> a1
+ | |
+ r0 | | r1
+ | |
+ V V
+ b0 -----> b1
+ v
+
+-}
+Square (A : U) (a0 a1 b0 b1 : A) (u : Id A a0 a1) (v : Id A b0 b1)
+ (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U
+ = IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1
+
+constSquare (A : U) (a : A) (p : Id A a a) : Square A a a a a p p p p =
+ <i j> comp (<_> A) a [ (i = 0) -> <k> p @ j \/ - k
+ , (i = 1) -> <k> p @ j /\ k
+ , (j = 0) -> <k> p @ i \/ - k
+ , (j = 1) -> <k> p @ i /\ k ]
+
+
+
+-- Names and compisitions provides a convenient way for reasoning with
+-- equalities:
+
+data nat = zero
+ | suc (n : nat)
+
+one : nat = suc zero
+two : nat = suc one
+
+add (a : nat) : nat -> nat = split
+ zero -> a
+ suc b -> suc (add a b)
+
+-- Exercise (for solution see bottom of the file):
+addZero : (a : nat) -> Id nat (add zero a) a = undefined
+
+addSuc (a : nat) : (b : nat) -> Id nat (add (suc a) b) (suc (add a b)) = split
+ zero -> <i> suc a
+ suc b' -> <i> suc (addSuc a b' @ i)
+
+-- Exercise (can be done with a composition):
+addCom (a : nat) : (b : nat) -> Id nat (add a b) (add b a) = undefined
+
+addAssoc (a b : nat) : (c : nat) -> Id nat (add a (add b c)) (add (add a b) c) = split
+ zero -> <i> add a b
+ suc c' -> <i> suc (addAssoc a b c' @ i)
+
+
+{-
+ Transport
+--------------------------------------------------------------------------
+
+Transport takes a path in the universe between A and B and produces a
+function from A to B:
+
+ transport : Id U A B -> A -> B
+
+It can be defined as a composition with an empty cube/system.
+
+-}
+
+transport (A B : U) (p : Id U A B) (a : A) : B = comp p a []
+
+-- This gives a simple proof of subst:
+subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
+ transport (P a) (P b) (cong A U P a b p) e
+
+-- Combined 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 =
+ subst (singl A a) T (a,refl A a) (x,p) (contrSingl A a x p) d
+ where T (bp : singl A a) : U = C bp.1 bp.2
+
+-- Note: Transporting with refl is not the identity function:
+
+-- transRefl (A : U) (a : A) : Id A a a = refl A (transport (refl U A) a)
+
+-- This implies that the elimination rule for J does not hold definitonally:
+
+-- 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
+
+-- 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.
+
+
+{-
+ Glueing
+--------------------------------------------------------------------------
+
+The univalence axiom says that equivalent (written as ~) types are
+equal:
+
+ (A = B) ~ (A ~ B)
+
+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.
+
+-}
+
+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 =
+ <i> 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.
+
+
+ ---------------------------------------------------------
+ -- Example: Non-trivial equality between bool and bool --
+ ---------------------------------------------------------
+
+-- Not is involutive:
+notK : (b : bool) -> Id bool (not (not b)) b = split
+ false -> <i> false
+ true -> <i> true
+
+-- This defines a non-trivial equality between bool and bool:
+notEq : Id U bool bool = isoId bool bool not not notK notK
+
+-- We can transport true along this non-trivial equality:
+testFalse : bool = transport bool bool notEq true
+
+
+ ---------------------------------------------------
+ -- Example: Non-trivial equality between Z and Z --
+ ---------------------------------------------------
+
+-- Integers:
+data or (A B : U) = inl (a : A)
+ | inr (b : B)
+
+Z : U = or nat nat
+
+{- Z represents:
+
+ +2 = inr (suc (suc zero))
+ +1 = inr (suc zero)
+ 0 = inr zero
+ -1 = inl zero
+ -2 = inl (suc zero)
+
+-}
+
+zeroZ : Z = inr zero
+
+sucZ : Z -> Z = split
+ inl u -> auxsucZ u
+ where
+ auxsucZ : nat -> Z = split
+ zero -> zeroZ
+ suc n -> inl n
+ inr v -> inr (suc v)
+
+predZ : Z -> Z = split
+ inl u -> inl (suc u)
+ inr v -> auxpredZ v
+ where
+ auxpredZ : nat -> Z = split
+ zero -> inl zero
+ suc n -> inr n
+
+sucpredZ : (x : Z) -> Id Z (sucZ (predZ x)) x = split
+ inl u -> <i> inl u
+ inr v -> lem v
+ where
+ lem : (u : nat) -> Id Z (sucZ (predZ (inr u))) (inr u) = split
+ zero -> <i> inr zero
+ suc n -> <i> inr (suc n)
+
+predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split
+ inl u -> lem u
+ where
+ lem : (u : nat) -> Id Z (predZ (sucZ (inl u))) (inl u) = split
+ zero -> <i> inl zero
+ suc n -> <i> inl (suc n)
+ inr v -> <i> inr v
+
+sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ
+
+-- We can transport along the proof forward and backwards:
+testOneZ : Z = transport Z Z sucIdZ zeroZ
+testNOneZ : Z = transport Z Z (<i> sucIdZ @ - i) zeroZ
+
+
+ -----------------------------------
+ -- Example: Equality in pi types --
+ -----------------------------------
+
+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) -> <i> (p @ i) x
+ G (p : T1) : T0 = <i> \(x : A) -> (p x) @ i
+ S (p : T1) : Id T1 (F (G p)) p = <i> p
+ T (p : T0) : Id T0 (G (F p)) p = <i> 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) -> <i> \(x : A) -> h x (f x) (g x) (p x) (q x) @ i
+ in subst U prop T (Id (pi A B) f g) (<i> idPi A B f g @ -i) rem
+
+
+
+{-
+ Higher-inductive types (HITs)
+--------------------------------------------------------------------------
+
+Another way to obtain non-trivial equalities are HITs. These
+generalize normal inductive types by allowing constructors that define
+(possibly higher) equalities.
+
+-}
+
+ ----------------------------------
+ -- Example: The circle as a HIT --
+ ----------------------------------
+
+data S1 = base
+ | loop <i> [ (i = 0) -> base, (i = 1) -> base]
+
+loopS1 : U = Id S1 base base
+
+-- The loop constructor
+loop1 : loopS1 = <i> loop{S1} @ i
+
+invLoop : loopS1 = sym S1 base base loop1
+
+helix : S1 -> U = split
+ base -> Z
+ loop @ i -> sucIdZ @ i
+
+-- The winding number:
+winding (p : loopS1) : Z = transport Z Z (<i> helix (p @ i)) zeroZ
+
+-- Loop composition:
+compS1 : loopS1 -> loopS1 -> loopS1 = trans S1 base base base
+
+-- Some examples of winding numbers:
+loopZ1 : Z = winding loop1
+loopZ2 : Z = winding (compS1 loop1 loop1)
+loopZ3 : Z = winding (compS1 loop1 (compS1 loop1 loop1))
+loopZN1 : Z = winding invLoop
+loopZ0 : Z = winding (compS1 loop1 invLoop)
+
+mLoop : (x : S1) -> Id S1 x x = split
+ base -> loop1
+ loop @ i -> constSquare S1 base loop1 @ i
+
+-- Multiplication:
+mult (x : S1) : S1 -> S1 = split
+ base -> x
+ loop @ i -> mLoop x @ i
+
+-- Squaring:
+square (x : S1) : S1 = mult x x
+
+doubleLoop (l : loopS1) : loopS1 = <i> square (l @ i)
+
+loopZ4 : Z = winding (doubleLoop (compS1 loop1 loop1))
+loopZ8 : Z = winding (doubleLoop (doubleLoop (compS1 loop1 loop1)))
+
+-- A nice example of a homotopy on the circle. The path going halfway
+-- around the circle and then back is contractible:
+hmtpy : Id loopS1 (<i> base) (<i> loop{S1} @ (i /\ -i)) =
+ <j 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> [ (i = 0) -> pos zero, (i = 1) -> neg zero ]
+
+-- Nice version of the zero constructor:
+zeroZ : Id int (pos zero) (neg zero) = <i> 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 -> <i> inl n
+ inr n -> <i> inr n
+
+fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split
+ pos n -> <i> pos n
+ neg n -> rem n
+ where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split
+ zero -> zeroZ
+ suc m -> <i> neg (suc m)
+ zeroP @ i -> <j> 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
+
+
+{-
+ Issues and Future Work
+--------------------------------------------------------------------------
+
+ o Definitional equality for J? Problem pointed out by Dan Licata
+ with regularity for composition in the universe. However the
+ system seems to work without regularity (this is work in
+ progress).
+
+ o Meta-theoretical properties of the system and correctness of the
+ model. Formalization?
+
+ o Integration of ideas into other proof assistants (eg Agda)?
+
+-}
+
+
+
+{- Solutions:
+
+addZero : (a : nat) -> Id nat (add zero a) a = split
+ zero -> <i> zero
+ suc a' -> <i> suc (addZero a' @ i)
+
+addCom (a : nat) : (b : nat) -> Id nat (add a b) (add b a) = split
+ zero -> <i> addZero a @ -i
+ suc b' -> <i> comp nat (suc (addCom a b' @ i)) [ (i = 0) -> <j> suc (add a b')
+ , (i = 1) -> <j> addSuc b' a @ -j ]
+-}
projects / cubicaltt.git / commitdiff