diff --git a/CTT.hs b/CTT.hs index 3bc9e4c..82fa12d 100644 --- a/CTT.hs +++ b/CTT.hs @@ -123,6 +123,7 @@ data Ter = Pi Ter | Id Ter Ter Ter | IdPair Ter (System Ter) | IdJ Ter Ter Ter Ter Ter Ter + | IdComp Ter Ter Ter Ter Ter Ter deriving Eq -- For an expression t, returns (u,ts) where u is no application and t = u ts @@ -182,6 +183,7 @@ data Val = VU | VLam Ident Val Val | VUnGlueElemU Val Val (System Val) | VIdJ Val Val Val Val Val Val + | VIdComp Val Val Val Val Val Val deriving Eq isNeutral :: Val -> Bool @@ -199,6 +201,7 @@ isNeutral v = case v of VUnGlueElemU{} -> True VUnGlueElem{} -> True VIdJ{} -> True + VIdComp{} -> True _ -> False isNeutralSystem :: System Val -> Bool @@ -387,6 +390,7 @@ showTer v = case v of Id a u v -> text "Id" <+> showTers [a,u,v] IdPair b ts -> text "idC" <+> showTer1 b <+> text (showSystem ts) IdJ a t c d x p -> text "idJ" <+> showTers [a,t,c,d,x,p] + IdComp a u v w p q -> text "idComp" <+> showTers [a,u,v,w,p,q] showTers :: [Ter] -> Doc showTers = hsep . map showTer1 @@ -454,6 +458,7 @@ showVal v = case v of VId a u v -> text "Id" <+> showVals [a,u,v] VIdPair b ts -> text "idC" <+> showVal1 b <+> text (showSystem ts) VIdJ a t c d x p -> text "idJ" <+> showVals [a,t,c,d,x,p] + VIdComp a u v w p q -> text "idComp" <+> showVals [a,u,v,w,p,q] showPLam :: Val -> Doc showPLam e = case e of diff --git a/Eval.hs b/Eval.hs index e013605..8119020 100644 --- a/Eval.hs +++ b/Eval.hs @@ -85,6 +85,7 @@ instance Nominal Val where VIdPair u us -> support (u,us) VId a u v -> support (a,u,v) VIdJ a u c d x p -> support [a,u,c,d,x,p] + VIdComp a u v w p q -> support [a,u,v,w,p,q] act u (i, phi) | i `notElem` support u = u | otherwise = @@ -123,6 +124,8 @@ instance Nominal Val where VId a u v -> VId (acti a) (acti u) (acti v) VIdJ a u c d x p -> idJ (acti a) (acti u) (acti c) (acti d) (acti x) (acti p) + VIdComp a u v w p q -> + idComp (acti a) (acti u) (acti v) (acti w) (acti p) (acti q) -- This increases efficiency as it won't trigger computation. swap u ij@(i,j) = @@ -157,6 +160,8 @@ instance Nominal Val where VId a u v -> VId (sw a) (sw u) (sw v) VIdJ a u c d x p -> VIdJ (sw a) (sw u) (sw c) (sw d) (sw x) (sw p) + VIdComp a u v w p q -> + VIdComp (sw a) (sw u) (sw v) (sw w) (sw p) (sw q) ----------------------------------------------------------------------- -- The evaluator @@ -198,6 +203,8 @@ eval rho@(Env (_,_,_,Nameless os)) v = case v of IdPair b ts -> VIdPair (eval rho b) (evalSystem rho ts) IdJ a t c d x p -> idJ (eval rho a) (eval rho t) (eval rho c) (eval rho d) (eval rho x) (eval rho p) + IdComp a u v w p q -> idComp (eval rho a) (eval rho u) (eval rho v) + (eval rho w) (eval rho p) (eval rho q) _ -> error $ "Cannot evaluate " ++ show v evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)] @@ -286,6 +293,7 @@ inferType v = case v of -- VUnGlueElem _ b _ -> b -- This is wrong! Store the type?? VUnGlueElemU _ b _ -> b VIdJ _ _ c _ x p -> app (app c x) p + VIdComp a u _ w _ _ -> VId a u w _ -> error $ "inferType: not neutral " ++ show v (@@) :: ToFormula a => Val -> a -> Val @@ -444,6 +452,22 @@ isIdPair :: Val -> Bool isIdPair VIdPair{} = True isIdPair _ = False +idComp :: Val -> Val -> Val -> Val -> Val -> Val -> Val +idComp a u v w pId qId = case (pId, qId) of + (VIdPair p ps, VIdPair q qs) -> + let i:j:_ = freshs [a,u,v,w,pId,qId] in + let + rs = unionSystem + (unionSystem + (border (q @@ (Atom i :/\: Atom j)) ps) + (border (p @@ (Atom i :\/: NegAtom j)) qs)) + (mkSystem [((i ~> 0), p @@ NegAtom j), ((i ~> 1), q @@ Atom j)]) + in + VIdPair (VPLam i (comp j a v rs)) (joinSystem (border ps qs)) + (VIdPair p ps, qId) | eps `member` ps -> qId + (pId, VIdPair q qs) | eps `member` qs -> pId + _ -> VIdComp a u v w pId qId + ------------------------------------------------------------------------------- -- | HITs @@ -897,6 +921,8 @@ instance Convertible Val where (VId a u v,VId a' u' v') -> conv ns (a,u,v) (a',u',v') (VIdJ a u c d x p,VIdJ a' u' c' d' x' p') -> conv ns [a,u,c,d,x,p] [a',u',c',d',x',p'] + (VIdComp a u b w p q,VIdComp a' u' b' w' p' q') -> + conv ns [a,u,b,w,p,q] [a',u',b',w',p',q'] _ -> False instance Convertible Ctxt where diff --git a/Exp.cf b/Exp.cf index f93cc81..73e29e1 100644 --- a/Exp.cf +++ b/Exp.cf @@ -45,6 +45,7 @@ UnGlueElem. Exp3 ::= "unglue" Exp4 System ; Id. Exp3 ::= "Id" Exp4 Exp4 Exp3 ; IdPair. Exp3 ::= "idC" Exp4 System ; IdJ. Exp3 ::= "idJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ; +IdComp. Exp3 ::= "idComp" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ; Fst. Exp4 ::= Exp4 ".1" ; Snd. Exp4 ::= Exp4 ".2" ; Pair. Exp5 ::= "(" Exp "," [Exp] ")" ; diff --git a/Resolver.hs b/Resolver.hs index c61f65d..947190f 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -223,6 +223,8 @@ resolveExp e = case e of IdPair u ts -> CTT.IdPair <$> resolveExp u <*> resolveSystem ts IdJ a t c d x p -> CTT.IdJ <$> resolveExp a <*> resolveExp t <*> resolveExp c <*> resolveExp d <*> resolveExp x <*> resolveExp p + IdComp a u v w p q -> CTT.IdComp <$> resolveExp a <*> resolveExp u <*> resolveExp v + <*> resolveExp w <*> resolveExp p <*> resolveExp q _ -> do modName <- asks envModule throwError ("Could not resolve " ++ show e ++ " in module " ++ modName) diff --git a/TypeChecker.hs b/TypeChecker.hs index 12135e7..b2cc393 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -516,6 +516,20 @@ infer e = case e of check (VId va vu vx) p vp <- evalTyping p return (app (app vc vx) vp) + IdComp a u v w p q -> do + check VU a + va <- evalTyping a + check va u + vu <- evalTyping u + check va v + vv <- evalTyping v + check va w + vw <- evalTyping w + let vIduv = VId va vu vv + let vIdvw = VId va vv vw + check vIduv p + check vIdvw q + return (VId va vu vw) _ -> throwError ("infer " ++ show e) -- Not used since we have U : U diff --git a/examples/idcomp.ctt b/examples/idcomp.ctt new file mode 100644 index 0000000..c8c90f6 --- /dev/null +++ b/examples/idcomp.ctt @@ -0,0 +1,253 @@ +module idcomp where + +import prelude +import idtypes + +-- Built in composition for Id + +-- Cubicaltt now includes a primitive composition operation for Id types +-- Recall that the identity type is modelled by pairs: +-- +-- G |- (p,s) : Id A u v +-- +-- where: +-- +-- G |- p : Path A u v, G |- s : F and G,s |- p = refl +-- +-- Here F is the face lattice. We can define composition as follows, given: +-- +-- (p,s) : Id A u v +-- (q,t) : Id A v w +-- +-- Define: +-- +-- r = comp (<_> A) v +-- [ s \/ (i=1) -> q @ (i /\ j) +-- , t \/ (i=0) -> p @ (i \/ -j) ] +-- +-- It can be checked that (r , s /\ t) : Id A u w and that when p = refl then +-- r = q and when q = refl then r = p. +-- +-- Since we can't manipluate face formulae in cubicaltt we cannot define this +-- operation and so it has been added as a primitive. + +-------------------------------------------------------------------------------- +-- Left and right unit laws + +-- Using the primative composition we have the left and right +-- unit laws both proved with refl: +compReflL (A : U) (u v : A) (p : Id A u v) + : Id (Id A u v) p (idComp A u u v (refId A u) p) = refId (Id A u v) p + +compReflR (A : U) (u v : A) (p : Id A u v) + : Id (Id A u v) p (idComp A u v v p (refId A v)) = refId (Id A u v) p + +-- This is not the case with the defined composition. +-- Here the left unit law requires using J +compReflL' (A : U) (u v : A) (p : Id A u v) + : Id (Id A u v) p (compId A u u v (refId A u) p) = + -- Does not typecheck: refId (Id A u v) p + idJ A u + (\(v : A)(p : Id A u v) -> Id (Id A u v) p (compId A u u v (refId A u) p)) + (refId (Id A u u) (refId A u)) v p + +-- Whereas the right unit rule is still proved with refl +compReflR' (A : U) (u v : A) (p : Id A u v) + : Id (Id A u v) p (compId A u v v p (refId A v)) = refId (Id A u v) p + +-- We could have also defined compId to have the left unit law be refl, +-- or to have neither, but not to have both. These different definitions +-- correspond to the three different definitions of p.q discussed after +-- Lemma 2.1.2 in the HoTT book. Using pattern matching the three +-- possible definitions are: +-- +-- compId refl q = q +-- compId p refl = p -- The definition given in idtypes.ctt +-- compId refl refl = refl +-- + +-------------------------------------------------------------------------------- +-- Inverting distributes over composition + +-- Given p : a = b and q : b = c we can show: +-- +-- (p . q)^-1 = q^-1 . p^-1 +-- +-- This proof is easier if we use the primitive version of composition +-- since if we use idJ to reduce q to refl then we get: +-- +-- (p . refl)^-1 = refl^-1 . p^-1 +-- +-- Since refl^-1 = refl definitionally the goal reduces to: +-- +-- (p . refl)^-1 = refl . p^-1 +-- +-- Using the primitive composition both p . refl and refl . p^-1 will +-- reduce and leave the goal as: +-- +-- p^-1 = p^-1 +-- +-- which is easily proved by refl. However, using the defined +-- composition only one side will reduce and we will need to perform +-- another application of idJ on p. The situation where we first +-- induct on p is symmetric. + +-- The lemma we want to show +InvComp (A : U) (a b : A) (p : Id A a b) (c : A) (q : Id A b c) : U = + Id (Id A c a) + (symId A a c (idComp A a b c p q)) + (idComp A c b a (symId A b c q) (symId A a b p)) + +-- Proved using a single application of idJ +invComp (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : InvComp A a b p c q = + idJ A b (InvComp A a b p) (refId (Id A b a) (symId A a b p)) c q + +-- The lemma using compId +InvComp' (A : U) (a b : A) (p : Id A a b) (c : A) (q : Id A b c) : U = + Id (Id A c a) + (symId A a c (compId A a b c p q)) + (compId A c b a (symId A b c q) (symId A a b p)) + +-- Now requires two applications of idJ +invComp' (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : InvComp' A a b p c q = + idJ A b (InvComp' A a b p) + (idJ A a + (\(b : A)(p : Id A a b) -> InvComp' A a b p b (refId A b)) + (refId (Id A a a) (refId A a)) b p) c q + + +-------------------------------------------------------------------------------- +-- More examples/experiements + +-- Weak refl +wrefId (A : U)(a : A) : Id A a a = idC (<_> a) [] + +s2w (A : U)(a : A) : Path (Id A a a) (refId A a) (wrefId A a) = + idC (<_> a) [(i=0) -> a] + +w2s (A : U)(a : A) : Path (Id A a a) (wrefId A a) (refId A a) = + idC (<_> a) [(i=1) -> a] + +-- We now have the following two squares: +-- (The lines in the x-direction are regular paths, +-- and the lines in the y-direction are Id paths) +-- +-- refl +-- a -------> a +-- | | +-- refId | | wrefId +-- v refl v +-- a -------> a +-- | | +-- wrefId | | refId +-- v refl v +-- a -------> a +-- +-- We can now compose in the vertical direction to get a square: +-- +-- refl +-- a -------> a +-- refId | | wrefId +-- . wrefId | | . refId +-- v refl v +-- a -------> a +-- +-- where p . q is the composition of p followed by q. + +-- If . is the built-in composition then both sides are wrefId +-- and we get the following: + +square (A : U)(a : A) : Path (Id A a a) (wrefId A a) (wrefId A a) = + idComp A a a a (s2w A a @ i) (w2s A a @ i) + +-- Gives: +-- idC ( comp (<_> A) a +-- [ (i = 0) -> <_> a +-- , (i = 1) -> <_> a +-- , (j = 0) -> <_> a +-- , (j = 1) -> <_> a ]) [] + +-- Using the defined composition the left hand side of the square +-- is not definitionally equal to wref and so results in a path with +-- a starting point containing a trvial comp. + +wrefCompId (A : U)(a : A) : Id A a a = + idC ( comp (<_> A) a [(i=0) -> <_> a, (i=1) -> <_> a]) [] + +square' (A : U)(a : A) : Path (Id A a a) (wrefCompId A a) (wrefId A a) = + compId A a a a (s2w A a @ i) (w2s A a @ i) + +-- Gives: +-- idC ( comp (<_> A) a +-- [ (i = 1) -> <_> a +-- , (j = 0) -> <_> a +-- , (j = 1) -> <_> a ]) [] +-- +-- Note that here we only have 3 out of 4 edges defined, as opposed to +-- having all 4 defined previously. + + +-- Consider the following type: +data IdCompTest = a | b + | sq1 [ (i=0) -> a, (i=1) -> a, (j=0) -> a, (j=1) -> a ] + | sq2 [ (j=0) -> a, (j=1) -> b ] + +-- We can visualise sq1 and sq2 as two squares with a common +-- face, like so: +-- +-- refl +-- a -------> a +-- | | +-- refl | | refl +-- v refl v +-- a -------> a +-- | | +-- | | +-- v refl v +-- b -------> b +-- +-- Encode the top square as p1: + +p1 : Path (Id IdCompTest a a) (refId IdCompTest a) (refId IdCompTest a) = + idC ( sq1 {IdCompTest} @ i @ j) [ (i=0) -> a, (i=1) -> a ] + +-- And the left and right sides of the bottom square as: + +id1 : Id IdCompTest a b = idC ( sq2 {IdCompTest} @ 0 @ j) [] +id2 : Id IdCompTest a b = idC ( sq2 {IdCompTest} @ 1 @ j) [] + +-- The bottom square: + +p2 : Path (Id IdCompTest a b) id1 id2 = + idC ( sq2 {IdCompTest} @ i @ j) [] + +-- We can now compose in the vertical direction to get a square: +-- +-- refl +-- a -------> a +-- refId | | refId +-- . id1 | | . id2 +-- v refl v +-- b -------> b +-- +-- where p . q is the composition of p followed by q. +-- +-- This is nicely handled by the primitive composition: + +p3 : Path (Id IdCompTest a b) id1 id2 = + idComp IdCompTest a a b (p1 @ i) (p2 @ i) + +-- However, the defined composiiton of refId and id1/id2 +-- doesn't reduce definitionally and so we get a more complicated +-- type for the composite squre p3' + +id1' : Id IdCompTest a b = compId IdCompTest a a b (wrefId IdCompTest a) id1 +id2' : Id IdCompTest a b = compId IdCompTest a a b (wrefId IdCompTest a) id2 + +p3' : Path (Id IdCompTest a b) id1' id2' = + compId IdCompTest a a b (p1 @ i) (p2 @ i) + +-- N.B. this fails because of the way that we defined compId, we +-- could have defined compId to reduce on refId and p, but then +-- we could construct a symmetric problem. The key thing is that +-- the primitive composition will reduce on both sides. diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt index be8c80f..5fba758 100644 --- a/examples/idtypes.ctt +++ b/examples/idtypes.ctt @@ -32,12 +32,24 @@ transId (A B : U) (p : Id U A B) (a : A) : B = transIdRef (A B : U) (p : Id U A B) (a : A) : Id A (transId A A (refId U A) a) a = refId A a +-- NB: Use the primitive idComp for better computational properties. +-- Leaving this definition here for backwards compatibility. +-- See the end of this file for more details. compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = substId A (\ (z : A) -> Id A a z) b c q p + -- idComp A a b c p q +-- Does not reduce to p compIdRef (A : U) (a b : A) (p : Id A a b): Id A a b = compId A a a b (refId A a) p +-- Reduces to p +compIdRef' (A : U) (a b : A) (p : Id A a b): Id A a b = + compId A a b b p (refId A b) + +symId (A : U) (a b : A) (p : Id A a b) : Id A b a = + idJ A a (\(b : A)(p : Id A a b) -> Id A b a) (refId A a) b p + idToPath (A : U) (a b : A) (p : Id A a b) : Path A a b = idJ A a (\ (b : A) (p : Id A a b) -> Path A a b) ( a) b p