module demo where
+{-
+ cubicaltt: Cubical type theory
+--------------------------------------------------------------------------
+ Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
--- Cubical type theory!
------------------------
--- (j.w.w. Cyril Cohen, Thierry Coquand, Anders M\"ortberg)
--- Try it:
--- https://github.com/mortberg/cubicaltt
+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.
--- Ordinary type theory (without Id-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.
-identity (A : U) (a : A) : A = a
+Mini-TT is a variant Martin-Löf type theory with data
+types. cubiclaltt extends Mini-TT with:
-data bool = false | true
+ o Name abstraction and application
+ o Compositions
+ o Equivalences can be transformed into equalities
+ o Some higher inductive types
-neg : bool -> bool = split
- false -> true
- true -> false
+Try it: https://github.com/mortberg/cubicaltt
-data nat = zero
- | suc (n : nat)
+-}
-one : nat = suc zero
-two : nat = suc one
+ ------------------------------------------
+ -- Some examples of programs in Mini-TT --
+ ------------------------------------------
-data list (A : U) = nil
- | cons (a : A) (as : list A)
+-- 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 A0 A1 is a line in the universe connecting A0 and A1:
+An element in ID A B is a line in the universe connecting A and B:
- |- A0 Type |- A1 Type
------------------------------
- |- ID A0 A1 Type
+ |- A Type |- B Type
+ ------------------------------
+ |- ID A B Type
- |- P : ID A0 A1 |- a0 : A0 |- a1 : A1
---------------------------------------------------------
- |- IdP P a0 a1 Type
+IdP is heterogeneous equality:
-Note: As we have U : U the type ID is not needed in the
- implementation.
+
+ |- 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
--- Here "<i> A" is a constant path in the universe:
-constPath (A : U) : Id U A A = <i> A
-
--- "<i>" abstracts the name/color/dimension i.
+-- "<i>" abstracts the name/color/dimension i:
refl (A : U) (a : A) : Id A a a = <i> a
-inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
-test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
-test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
+{-
-mapOnPath (A B : U) (f : A -> B) (a b : A)
- (p : Id A a b) : Id B (f a) (f b) =
+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 =
+ (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 that the definition of funExt makes sense we can compute its
+faces:
+
+funExt @ 0 = \(a : A) -> (p a) @ 0
+ = \(a : A) -> f a
+ = f
+
+The last equality holds because of 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))
+ <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
-reflRefl (A : U) (a : A) : Id (Id A a a) (refl A a) (refl A a) =
- refl (Id A a a) (refl A a)
--- <i j> a
+{-
+
+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
-test2 (A : U) (a b : A) (p : Id A a b) : Id A a a =
- <i> p @ (i /\ -i)
-test3 (A : U) (a b : A) (p : Id A a b) : Id A b b =
- <i> p @ (i \/ -i)
+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 ]
--- Transport.
+-- Names and compisitions provides a convenient way for reasoning with
+-- equalities:
--- transport is another built-in.
--- It takes a path p in U and an element
--- in p @ 0; produces an element in p @ 1
-subst (A : U) (P : A -> U) (a b : A)
- (p : Id A a b) (e : P a) : P b =
- transport (mapOnPath A U P a b p) e
+data nat = zero
+ | suc (n : nat)
-substEq (A : U) (P : A -> U) (a : A) (e : P a) :
- Id (P a) (subst A P a a (refl A a) e) e =
- refl (P a) e
+one : nat = suc zero
+two : nat = suc one
+
+add (a : nat) : nat -> nat = split
+ zero -> a
+ suc b -> suc (add a b)
+
+addZero : (a : nat) -> Id nat (add zero a) a = split
+ zero -> <i> zero
+ suc a' -> <i> suc (addZero a' @ i)
+
+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)
+
+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 ]
+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 is defined internally as a composition with an empty system.
+
+-}
+
+-- 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 (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)
+ where T (bp : singl A a) : U = C bp.1 bp.2
+
+-- Note: Transporting with refl is not the identity function:
--- Examples:
+-- transRefl (A : U) (a : A) : Id A a a = refl A (transport (refl U A) a)
-ptU : U = (X : U) * X
+-- This implies that the elimination rule for J does not hold definitonally:
-lemPt (A B : U) (p : Id U A B) (a : A) : Id ptU (A,a) (B,transport p a) =
- <i> (p @ i,transport (<j> p @ (i/\j)) a)
+-- 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
-S : U = (A : U) (a : A) * (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.
-lemS (A B : U) (p : Id U A B) (a : A) (f : A -> A) :
- Id S (A,a,f) (B, transport p a, transport (<i> p @ i -> p @ i) f) =
- <i> ( p @ i
- , transport (<j> p @ (i/\j)) a
- , transport (<j> p @ (i /\ j) -> p @ (i /\ j)) f)
--- Composition.
--- Any type is a weak omega-groupoid.
--- Given a cube, we form a new cube by replacing some faces along equalities.
+{-
+ Glueing
+--------------------------------------------------------------------------
-transitive (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 = 1) -> q ]
+The univalence axiom says that equivalent (written as ~) types are
+equal:
---- comp A (p @ (i /\ j)) [ (i=1)(j=1) -> q]
+ (A = B) ~ (A ~ B)
-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) -> <j> q @ j, (i = 1) -> r ]
+Glueing is a weaker form of this for producing non-trivial equalities
+from equivalences. In particular glueing gives a map from Equiv(A,B)
+to A = B. This weak form of univalence is useful for developing a lot
+of examples. For examples see:
-regKan (A : U) (a b : A) (p : Id A a b) :
- Id (Id A a b) p (kan A a b a b p (refl A a) (refl A b)) =
- refl (Id A a b) p
+ - examples/bool.ctt: Non-trivial equality between bool and bool
+ given by negation.
--- Example: any proposition is a set.
+ - examples/int.ctt: Non-trivial equality between Z and Z given by
+ successor and predecessor.
-prop (A : U) : U = (a b : A) -> Id A a b
-set (A : U) : U = (a b : A) -> prop (Id A a b)
+ - examples/pi.ctt: Equality in pi types.
-propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b)
- : Id (Id A a b) p q =
- <j i> comp A a [ (i=0) -> h a a
- , (i=1) -> h a b
- , (j=0) -> h a (p @ i)
- , (j=1) -> h a (q @ i)]
+Further, the full form of univalence is provable in the system. See
+the file examples/univalence.ctt for a proof of this.
+-}
--- Glueing.
--- A way to produce non-trivial equalities.
-
-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 B [ (i = 0) -> (A,f,g,s,t) ]
-negK : (b : bool) -> Id bool (neg (neg b)) b = split
- false -> refl bool false
- true -> refl bool true
-negEq : Id U bool bool =
- <i> (glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ])
+{-
+ 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. For further examples see:
-testFalse : bool = transport negEq true
+ - examples/circle.ctt: The circle as a HIT.
--- Continue with: integer, circle, suspension
+ - examples/integer.ctt: The integers as a HIT.
+-}
projects / cubicaltt.git / commitdiff