+++ /dev/null
--- Talk given by Anders Mörtberg at AIMXXI:
--- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXI
-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 UF/HoTT, 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
-
-
--}
-
- ------------------------------------------
- -- 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
-
-{-
- Path 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
-
-
-PathP is heterogeneous equality:
-
-
- |- P : ID A B |- a : A |- b : B
- -----------------------------------------------
- |- PathP P a b Type
-
--}
-
--- The constant Path type can be seen a special case of PathP:
-Path (A : U) (a b : A) : U = PathP (<i> A) a b
-
--- "<i>" abstracts the name/color/dimension i:
-refl (A : U) (a : A) : Path A a a = <i> a
-
-{-
-
-A proof "p : Path A a b" is thought of as a line between a and b:
-
- p
- a ------> b
-
-
-A proof "sq : Path (Path 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 : Path A a b) : Path A a a = refl A (p @ 0)
-face1 (A : U) (a b : A) (p : Path A a b) : Path 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 : Path A a b) : Path 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) -> Path (B x) (f x) (g x)) : Path ((y : A) -> B y) f g =
- <i> \(x : A) -> (p x) @ 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 : Path A a b) : Path A b a = <i> p @ -i
-
--- This operation is an involution:
-symK (A : U) (a b : A) (p : Path A a b) : Path (Path A a b) p p =
- refl (Path 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) * Path A a x
-
-contrSingl (A : U) (a b : A) (p : Path A a b) :
- Path (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 : Path A a b) :
- Path (Path A a a) (<_> p @ 0) (<_> p @ 0) =
- refl (Path 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 : Path A a b) : Path A a a = <i> p @ i /\ -i
-testDisj (A : U) (a b : A) (p : Path A a b) : Path A b b = <i> p @ i \/ -i
-
-
-
-{-
-
-So far we have: MLTT + Path, <i>, @, 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 : Path 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
-------------------------------------------------------------------------
-
-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 Path is obtained from a composition of this open square:
-
-i : I, j : I |-
-
- a - - - - - - - - > c
- ^ ^
- | |
- | |
- (<_> a)@j| | q @ j
- | |
- | |
- | |
- a ----------------> b
- p @ i
-
-The composition computes the dashed line at the top of the square.
- ( <i>(<_>a)@i ) = (<j> (<_>a)@j) : Path (Path A a a) (<i> a) (<j> a)
-
-p = <i> p @ i
-
-i : I |- (<_>a) @i
-|- <i> (<_> a) @ i
-|- <_> a
--}
-
-
-pathscomp0 (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c =
- <i> comp (<_> A) (p @ i) [ (i = 0) -> <_> a
- , (i = 1) -> q ]
-
-
--- The first two nonzero h-levels are propositions and sets:
-prop (A : U) : U = (a b : A) -> Path A a b
-set (A : U) : U = (a b : A) -> prop (Path 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 : Path 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 : Path A a0 a1) (v : Path A b0 b1)
- (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U
- = PathP (<i> (PathP (<j> A) (u @ i) (v @ i))) r0 r1
-
-constSquare (A : U) (a : A) (p : Path 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 ]
-
-
-
--- 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 : Path A a b)
- (q : Path A a c) (r : Path A b d) : Path A c d =
- <i> comp (<_> A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
-
--- Generalized Kan composition:
-kan' (A B : U) (P : Path U A B) (a b : A) (c d : B) (p : Path A a b)
- (q : PathP P a c) (r : PathP P b d) : Path B c d =
- <i> comp P (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
-
-kan'' (A : U) (a b c d : A) (p : Path A a b)
- (q : Path A a c) (r : Path A b d) : Path 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:
-
-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) -> Path nat (add zero a) a = undefined
-
-addSuc (a : nat) : (b : nat) -> Path 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) -> Path nat (add a b) (add b a) = undefined
-
-addAssoc (a b : nat) : (c : nat) -> Path 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 : Path U A B -> A -> B
-
--}
-
--- This gives a simple proof of subst (called transportf above and in
--- UniMath):
-subst (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b =
- transport (cong 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 : Path U A B) (a : A) : B = comp p a []
-
--- However these are not exactly the same because the lack of implicit
--- arguments.
-
--- subst with the fact that singletons are contractible this gives
--- the J eliminator:
-J (A : U) (a : A) (C : (x : A) -> Path A a x -> U)
- (d : C a (refl A a)) (x : A) (p : Path 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) : Path 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) -> Path A a x -> U) (d : C a (refl A a)) :
--- Path (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) : Path 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 : Path A a b) (q : Path A b c) :
--- Path A (comp (<_> A) a []) c =
--- <i> comp (<_> A) (p @ i) [ (i = 1) -> q ]
-
-
-
--- It seems like we can recover a new Path type with the correct
--- definitional equalities using ideas from awfs of Andrew
--- Swan... Simon has implemented this in the branch "defeq".
-
-
-
-
-
-
-
-
-
-{-
-
-So far we have: MLTT + Path, <i>, @, i/\j, compositions, transport
-
-With all of this we get J, but so far without def. eq.
-
-We also want univalence and HITs.
-
--}
-
-
-
-
-
-
-{-
- Glueing
---------------------------------------------------------------------------
-
-Glueing is what enables us to prove univalence by producing
-non-trivial equalities from equivalences. In particular glueing gives
-a map from Equiv(A,B) to A = B.
-
--}
-
-isContr (A : U) : U = (x : A) * ((y : A) -> Path A x y)
-
-fiber (A B : U) (f : A -> B) (y : B) : U =
- (x : A) * Path B y (f x)
-
-isEquiv (A B : U) (f : A -> B) : U =
- (y : B) -> isContr (fiber A B f y)
-
-idIsEquiv (A : U) : isEquiv A A (idfun A) =
- \(a : A) -> ((a, refl A a)
- ,\(z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2)
-
--- Using the grad lemma we can transform isomorphisms into equalities.
-lemIso (A B : U) (f : A -> B) (g : B -> A)
- (s : (y : B) -> Path B (f (g y)) y)
- (t : (x : A) -> Path A (g (f x)) x)
- (y : B) (x0 x1 : A) (p0 : Path B y (f x0)) (p1 : Path B y (f x1)) :
- Path (fiber A B f y) (x0,p0) (x1,p1) = <i> (p @ i,sq1 @ i)
- where
- rem0 : Path A (g y) x0 =
- <i> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ]
-
- rem1 : Path A (g y) x1 =
- <i> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ]
-
- p : Path A x0 x1 =
- <i> comp (<_> A) (g y) [ (i = 0) -> rem0
- , (i = 1) -> rem1 ]
-
- fill0 : Square A (g y) (g (f x0)) (g y) x0
- (<i> g (p0 @ i)) rem0 (<i> g y) (t x0) =
- <i j> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
- , (i = 0) -> <_> g y
- , (j = 0) -> <_> g (p0 @ i) ]
-
- fill1 : Square A (g y) (g (f x1)) (g y) x1
- (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =
- <i j> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k
- , (i = 0) -> <_> g y
- , (j = 0) -> <_> g (p1 @ i) ]
-
- fill2 : Square A (g y) (g y) x0 x1
- (<_> g y) p rem0 rem1 =
- <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
- , (i = 1) -> <k> rem1 @ j /\ k
- , (j = 0) -> <_> g y ]
-
- sq : Square A (g y) (g y) (g (f x0)) (g (f x1))
- (<i> g y) (<i> g (f (p @ i)))
- (<j> g (p0 @ j)) (<j> g (p1 @ j)) =
- <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
- , (i = 1) -> <k> fill1 @ j @ -k
- , (j = 0) -> <_> g y
- , (j = 1) -> <k> t (p @ i) @ -k ]
-
- sq1 : Square B y y (f x0) (f x1)
- (<_>y) (<i> f (p @ i)) p0 p1 =
- <i j> comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)
- , (i = 1) -> s (p1 @ j)
- , (j = 1) -> s (f (p @ i))
- , (j = 0) -> s y ]
-
-gradLemma (A B : U) (f : A -> B) (g : B -> A)
- (s : (y : B) -> Path B (f (g y)) y)
- (t : (x : A) -> Path A (g (f x)) x) : isEquiv A B f =
- \ (y:B) -> ((g y,<i>s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (<i>s y@-i) z.2)
-
-
-
-isoPath (A B : U) (f : A -> B) (g : B -> A)
- (s : (y : B) -> Path B (f (g y)) y)
- (t : (x : A) -> Path A (g (f x)) x) : Path U A B =
- <i> Glue B [ (i = 0) -> (A,f,gradLemma A B f g s t)
- , (i = 1) -> (B,idfun B,idIsEquiv B) ]
-
-
-
-
-
-
- ---------------------------------------------------------
- -- Example: Non-trivial equality between bool and bool --
- ---------------------------------------------------------
-
--- Not is involutive:
-notK : (b : bool) -> Path bool (not (not b)) b = split
- false -> <i> false
- true -> <i> true
-
--- This defines a non-trivial equality between bool and bool:
-notEq : Path U bool bool = isoPath bool bool not not notK notK
-
--- We can transport true along this non-trivial equality:
-testFalse : bool = transport 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) -> Path Z (sucZ (predZ x)) x = split
- inl u -> <i> inl u
- inr v -> lem v
- where
- lem : (u : nat) -> Path Z (sucZ (predZ (inr u))) (inr u) = split
- zero -> <i> inr zero
- suc n -> <i> inr (suc n)
-
-predsucZ : (x : Z) -> Path Z (predZ (sucZ x)) x = split
- inl u -> lem u
- where
- lem : (u : nat) -> Path Z (predZ (sucZ (inl u))) (inl u) = split
- zero -> <i> inl zero
- suc n -> <i> inl (suc n)
- inr v -> <i> inr v
-
-sucPathZ : Path U Z Z = isoPath Z Z sucZ predZ sucpredZ predsucZ
-
--- We can transport along the proof forward and backwards:
-testOneZ : Z = transport sucPathZ zeroZ
-testNOneZ : Z = transport (<i> sucPathZ @ - i) zeroZ
-
-
--- transport sucPathZ = sucZ ?
-
-
-
-
------------------------------------------------------------------
--- Using Glue we get a proof of univalence, see univalence.ctt --
-
-
-
-
-
-
-{-
- 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 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:
-zeroPath : Path 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) -> Path Z (toZ (fromZ a)) a = split
- inl n -> <i> inl n
- inr n -> <i> inr n
-
-fromZK : (a : int) -> Path int (fromZ (toZ a)) a = split
- pos n -> <i> pos n
- neg n -> rem n
- where rem : (n : nat) -> Path int (fromZ (toZ (neg n))) (neg n) = split
- zero -> zeroPath
- suc m -> <i> neg (suc m)
- zeroP @ i -> <j> zeroPath @ i /\ j -- A connection makes this proof easy!
-
-isoIntZ : Path U Z int = isoPath Z int fromZ toZ fromZK toZK
-
-
-
- ----------------------------------
- -- Example: The circle as a HIT --
- ----------------------------------
-
-data S1 = base
- | loop <i> [ (i = 0) -> base, (i = 1) -> base]
-
-loopS1 : U = Path S1 base base
-
--- The loop constructor
-loop1 : loopS1 = <i> loop{S1} @ i
-
-invLoop : loopS1 = <i> loop1 @ -i
-
-helix : S1 -> U = split
- base -> Z
- loop @ i -> sucPathZ @ i
-
--- The winding number:
-winding (p : loopS1) : Z = transport (<i> helix (p @ i)) zeroZ
-
--- Loop composition:
-compS1 : loopS1 -> loopS1 -> loopS1 = pathscomp0 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) -> Path 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)
-
-doubleLoop' (l : loopS1) : loopS1 = compS1 l l
-
-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 : Path loopS1 (<i> base) (<i> loop{S1} @ (i /\ -i)) =
- <j i> loop{S1} @ j /\ i /\ -i
-
-
-
---------------------------------------------------------------------------
--- For a higher dimensional HIT see, torus.ctt
-
-
-
-
-
-
-
-
-
-{-
- 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 might still work without regularity (this is what is being
- implemented in the no_regular branch).
-
- o Meta-theoretical properties of the system and correctness of the
- model. Formalization?
-
- o Integration of ideas into other proof assistants (e.g. Agda)?
-
--}
-
-
-
-{- Solutions:
-
-addZero : (a : nat) -> Path nat (add zero a) a = split
- zero -> <i> zero
- suc a' -> <i> suc (addZero a' @ i)
-
-addCom (a : nat) : (b : nat) -> Path 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