From 6cf058d8c6eefbb66bb99cd8d7ad4f30575fe8ed Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Fri, 5 Jun 2015 15:50:26 +0200 Subject: [PATCH] Finished eqToIso and removed constants for comp in U --- CTT.hs | 28 ------ Eval.hs | 213 ++++++++++------------------------------ TypeChecker.hs | 4 +- examples/bool.ctt | 2 +- examples/newhedberg.ctt | 2 +- examples/prelude.ctt | 10 +- 6 files changed, 64 insertions(+), 195 deletions(-) diff --git a/CTT.hs b/CTT.hs index 3dbe30c..1b8a687 100644 --- a/CTT.hs +++ b/CTT.hs @@ -108,10 +108,6 @@ data Ter = App Ter Ter -- Kan composition and filling | Comp Ter Ter (System Ter) | Fill Ter Ter (System Ter) - -- | Trans Ter Ter - -- Composition in the Universe - -- | CompElem Ter (System Ter) Ter (System Ter) - -- | ElimComp Ter (System Ter) Ter -- Glue | Glue Ter (System Ter) | GlueElem Ter (System Ter) @@ -156,9 +152,6 @@ data Val = VU | VGlue Val (System Val) | VGlueElem Val (System Val) - -- Composition in the universe (for now) - | VCompU Val (System Val) - -- Composition for HITs; the type is constant | VHComp Val Val (System Val) @@ -166,19 +159,13 @@ data Val = VU -- | VGlueLine Val Formula Formula -- | VGlueLineElem Val Formula Formula - -- Universe Composition Values - -- | VCompElem Val (System Val) Val (System Val) - -- | VElimComp Val (System Val) Val - -- Neutral values: | VVar Ident Val | VFst Val | VSnd Val -- VUnGlueElem val type hisos | VUnGlueElem Val Val (System Val) - | VUnGlueElemU Val Val (System Val) | VSplit Val Val - -- | VHSqueeze Val Val Formula | VApp Val Val | VAppFormula Val Formula | VLam Ident Val Val @@ -196,7 +183,6 @@ isNeutral v = case v of VApp{} -> True VAppFormula{} -> True VUnGlueElem{} -> True - VUnGlueElemU{} -> True _ -> False isNeutralSystem :: System Val -> Bool @@ -401,17 +387,12 @@ showTer v = case v of AppFormula e phi -> showTer1 e <+> char '@' <+> showFormula phi Comp e t ts -> text "comp" <+> showTers [e,t] <+> text (showSystem ts) Fill e t ts -> text "fill" <+> showTers [e,t] <+> text (showSystem ts) - -- Trans e0 e1 -> text "transport" <+> showTers [e0,e1] Glue a ts -> text "glue" <+> showTer1 a <+> text (showSystem ts) GlueElem a ts -> text "glueElem" <+> showTer1 a <+> text (showSystem ts) -- GlueLine a phi psi -> text "glueLine" <+> showTer1 a <+> -- showFormula phi <+> showFormula psi -- GlueLineElem a phi psi -> text "glueLineElem" <+> showTer1 a <+> -- showFormula phi <+> showFormula psi - -- CompElem a es t ts -> text "compElem" <+> showTer1 a <+> text (showSystem es) - -- <+> showTer1 t <+> text (showSystem ts) - -- ElimComp a es t -> text "elimComp" <+> showTer1 a <+> text (showSystem es) - -- <+> showTer1 t showTers :: [Ter] -> Doc showTers = hsep . map showTer1 @@ -446,7 +427,6 @@ showVal v = case v of VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us <+> hsep (map ((char '@' <+>) . showFormula) phis) VHComp v0 v1 vs -> text "hComp" <+> showVals [v0,v1] <+> text (showSystem vs) - -- VHSqueeze a u phi -> text "hSqueeze" <+> showVals [a,u] <+> showFormula phi VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b | otherwise -> char '(' <> showLam v @@ -462,23 +442,15 @@ showVal v = case v of VSnd u -> showVal1 u <> text ".2" VUnGlueElem v b hs -> text "unGlueElem" <+> showVals [v,b] <+> text (showSystem hs) - VUnGlueElemU v b es -> text "unGlueElemU" <+> showVals [v,b] - <+> text (showSystem es) VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs) - -- VTrans v0 v1 -> text "trans" <+> showVals [v0,v1] VGlue a ts -> text "glue" <+> showVal1 a <+> text (showSystem ts) VGlueElem a ts -> text "glueElem" <+> showVal1 a <+> text (showSystem ts) - VCompU a ts -> text "compU" <+> showVal1 a <+> text (showSystem ts) -- VGlueLine a phi psi -> text "glueLine" <+> showFormula phi -- <+> showFormula psi <+> showVal1 a -- VGlueLineElem a phi psi -> text "glueLineElem" <+> showFormula phi -- <+> showFormula psi <+> showVal1 a - -- VCompElem a es t ts -> text "compElem" <+> showVal1 a <+> text (showSystem es) - -- <+> showVal1 t <+> text (showSystem ts) - -- VElimComp a es t -> text "elimComp" <+> showVal1 a <+> text (showSystem es) - -- <+> showVal1 t showPath :: Val -> Doc showPath e = case e of diff --git a/Eval.hs b/Eval.hs index 2aacdab..7ffb095 100644 --- a/Eval.hs +++ b/Eval.hs @@ -64,9 +64,7 @@ instance Nominal Val where VSplit u v -> support (u,v) VGlue a ts -> support (a,ts) VGlueElem a ts -> support (a,ts) - VCompU a ts -> support (a,ts) VUnGlueElem a b hs -> support (a,b,hs) - VUnGlueElemU a b es -> support (a,b,es) act u (i, phi) | i `notElem` support u = u | otherwise = @@ -98,8 +96,6 @@ instance Nominal Val where VGlue a ts -> glue (acti a) (acti ts) VGlueElem a ts -> glueElem (acti a) (acti ts) VUnGlueElem a b hs -> unGlue (acti a) (acti b) (acti hs) - VUnGlueElemU a b es -> unGlueU (acti a) (acti b) (acti es) - VCompU a ts -> compUniv (acti a) (acti ts) -- This increases efficiency as it won't trigger computation. swap u ij@(i,j) = @@ -127,8 +123,7 @@ instance Nominal Val where VGlue a ts -> VGlue (sw a) (sw ts) VGlueElem a ts -> VGlueElem (sw a) (sw ts) VUnGlueElem a b hs -> VUnGlueElem (sw a) (sw b) (sw hs) - VUnGlueElemU a b es -> VUnGlueElemU (sw a) (sw b) (sw es) - VCompU a ts -> VCompU (sw a) (sw ts) + ----------------------------------------------------------------------- -- The evaluator @@ -247,7 +242,6 @@ inferType v = case v of ++ ", got " ++ show ty VComp a _ _ -> a @@ One VUnGlueElem _ b hs -> glue b hs - VUnGlueElemU _ b es -> compUniv b es _ -> error $ "inferType: not neutral " ++ show v (@@) :: ToFormula a => Val -> a -> Val @@ -364,9 +358,7 @@ comp i a u ts = case a of ui1 = comp i a u1 t1s comp_u2 = comp i (app f fill_u1) u2 t2s VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts) - VU -> compUniv u (Map.map (VPath i) ts) - -- VGlue u (Map.map (eqToIso i) ts) - VCompU a es -> compU i a es u ts + VU -> glue u (Map.map (eqToIso . VPath i) ts) VGlue b hisos -> compGlue i b hisos u ts Ter (Sum _ _ nass) env -> case u of VCon n us -> case lookupLabel n nass of @@ -408,19 +400,35 @@ transpHIT i a u = squeezeHIT i a u `face` (i ~> 0) -- given u(i) of type a(i) "squeezeHIT i a u" connects in the direction i -- transHIT i a u(i=0) to u(i=1) in a(1) -squeezeHIT :: Name -> Val -> Val -> Val -squeezeHIT i a@(Ter (HSum _ _ nass) env) u = case u of - VCon n us -> case lookupLabel n nass of - Just as -> VCon n (squeezes i as env us) - Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n - VPCon c _ ws0 phis -> case lookupLabel c nass of - Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) (phis `face` (i ~> 1)) - Nothing -> error $ "squeezeHIT: missing path constructor " ++ c - VHComp _ v vs -> - hComp (a `face` (i ~> 1)) (transpHIT i a v) $ - mapWithKey (\alpha vAlpha -> - VPath i $ squeezeHIT i (a `face` alpha) (vAlpha @@ i)) vs - _ -> error $ "squeezeHIT: neutral " ++ show u +-- squeezeHIT :: Name -> Val -> Val -> Val +-- squeezeHIT i a@(Ter (HSum _ _ nass) env) u = case u of +-- VCon n us -> case lookupLabel n nass of +-- Just as -> VCon n (squeezes i as env us) +-- Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n +-- VPCon c _ ws0 phis -> case lookupLabel c nass of +-- Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) (phis `face` (i ~> 1)) +-- Nothing -> error $ "squeezeHIT: missing path constructor " ++ c +-- VHComp _ v vs -> +-- hComp (a `face` (i ~> 1)) (transpHIT i a v) $ +-- mapWithKey (\alpha vAlpha -> +-- VPath i $ squeezeHIT i (a `face` alpha) (vAlpha @@ i)) vs +-- _ -> error $ "squeezeHIT: neutral " ++ show u +squeezeHIT i a@(Ter (HSum _ _ nass) env) u = + let j = fresh (a,u) + aij = swap a (i,j) + in case u of + VCon n us -> case lookupLabel n nass of + Just as -> VCon n (squeezes i as env us) + Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n + VPCon c _ ws0 phis -> case lookupLabel c nass of + Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) phis + Nothing -> error $ "squeezeHIT: missing path constructor " ++ c + VHComp _ v vs -> + hComp (a `face` (i ~> 1)) (squeezeHIT i a v) $ + mapWithKey (\alpha vAlpha -> + VPath j $ squeezeHIT j (aij `face` alpha) (vAlpha @@ j)) vs + _ -> error $ "squeezeHIT: neutral " ++ show u + hComp :: Val -> Val -> System Val -> Val hComp a u us | eps `Map.member` us = (us ! eps) @@ One @@ -444,38 +452,32 @@ hisoFun :: Val -> Val hisoFun (VPair _ (VPair f _)) = f hisoFun x = error $ "HisoFun: Not an hiso: " ++ show x --- -- Every line in the universe induces an hiso +-- -- Every path in the universe induces an hiso eqToIso :: Val -> Val -eqToIso e = VPair e0 (VPair f (VPair g (VPair s t))) - where e0 = e @@ Zero +eqToIso e = VPair e1 (VPair f (VPair g (VPair s t))) + where e1 = e @@ One (i,j,x,y,ev) = (Name "i",Name "j",Var "x",Var "y",Var "E") - inv t = Path "i" $ AppFormula t (NegAtom i) + inv t = Path i $ AppFormula t (NegAtom i) evinv = inv ev - (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) - eenv = upd ("E",e) empty - (eplus z,eminus z) = (Comp ev z Map.empty,Comp evinv z Map.empty) - -- NB: edown is not transNegFill - (eup z,edown z) = (Fill ev z Map.empty,Fill evinv z Map.empty) - f = Ter (Lam x ev1 (eminus x)) eenv - g = Ter (Lam y ev0 (eplus y)) eenv - -- s : (y : e0) -> f (g y) = y - ssys = mkSystem [(j ~> 0, inv (eup y)), - ,(j ~> 1, edown (eplus y))] - s = Ter (Lam y ev0 $ Path j $ Comp einv (eplus y) ssys) eenv - -- t : (x : e1) -> g (f x) = x - -- tsys = mkSystem [(j ~> 0, eup (eup y)), - -- ,(j ~> 1, edown (eplus y))] - -- t = Ter (Lam y ev0 $ Path j $ Comp einv (eplus y) ssys) eenv - -- t e a = VPath j $ comp j (e @@ j) (transNeg j (e @@ j) a) - -- (mkSystem [(j ~> 0, transFill j (e @@ j) - -- (transNeg j (e @@ j) a)) - -- ,(j ~> 1, transFillNeg j (e @@ j) a)]) - - --- eqToIso :: Name -> Val -> Val --- eqToIso i u = VPair a (VPair f (VPair g (VPair s t))) --- where a = u `face` (i ~> 1) --- f = Ter (Lam "x" (Var "A") (Transport )) (upd ("A",a) empty) + (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) -- (b,a) + eenv = upd ("E",e) empty + -- eplus : e0 -> e1 + eplus z = Comp ev z Map.empty + -- eminus : e1 -> e0 + eminus z = Comp evinv z Map.empty + -- NB: edown is *not* transNegFill + eup z = Fill ev z Map.empty + edown z = Fill evinv z Map.empty + f = Ter (Lam "x" ev1 (eminus x)) eenv + g = Ter (Lam "y" ev0 (eplus y)) eenv + -- s : (y : e0) -> eminus (eplus y) = y + ssys = mkSystem [(j ~> 1, inv (eup y)) + ,(j ~> 0, edown (eplus y))] + s = Ter (Lam "y" ev0 $ Path j $ Comp evinv (eplus y) ssys) eenv + -- t : (x : e1) -> eplus (eminus x) = x + tsys = mkSystem [(j ~> 0, eup (eminus x)) + ,(j ~> 1, inv (edown x))] + t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv glue :: Val -> System Val -> Val glue b ts | Map.null ts = b @@ -580,110 +582,6 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = theta'' = comp j b (app f theta') xs -------------------------------------------------------------------------------- --- | Composition in the Universe (to be replaced as glue) - -unGlueU :: Val -> Val -> System Val -> Val -unGlueU w b es - | Map.null es = w - | eps `Map.member` es = transNegLine (es ! eps) w - | otherwise = case w of - VGlueElem v us -> v - _ -> VUnGlueElemU w b es - -compUniv :: Val -> System Val -> Val -compUniv b es | Map.null es = b - | eps `Map.member` es = (es ! eps) @@ One - | otherwise = VCompU b es - - -compU :: Name -> Val -> System Val -> Val -> System Val -> Val -compU i b es wi0 ws = glueElem vi1'' usi1'' - where bi1 = b `face` (i ~> 1) - vs = mapWithKey (\alpha wAlpha -> - unGlueU wAlpha (b `face` alpha) (es `face` alpha)) ws - vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs - vi0 = unGlueU wi0 (b `face` (i ~> 0)) (es `face` (i ~> 0)) -- in b(i0) - - v = fill i b vi0 vs -- in b - vi1 = comp i b vi0 vs -- is v `face` (i ~> 1) in b(i1) - - esI1 = es `face` (i ~> 1) - es' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es - es'' = filterWithKey (\alpha _ -> not (alpha `Map.member` es')) esI1 - - us' = mapWithKey (\gamma eGamma -> - fill i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma)) - es' - usi1' = mapWithKey (\gamma eGamma -> - comp i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma)) - es' - - ls' = mapWithKey (\gamma eGamma -> - pathComp i (b `face` gamma) (v `face` gamma) - (transNegLine eGamma (us' ! gamma)) (vs `face` gamma)) - es' - - vi1' = compLine (constPath bi1) vi1 - (ls' `unionSystem` Map.map constPath vsi1) - - wsi1 = ws `face` (i ~> 1) - - -- for gamma in es'', (i1) gamma is in es, so wsi1 gamma - -- is in the domain of isoGamma - uls'' = mapWithKey (\gamma eGamma -> - gradLemmaU (bi1 `face` gamma) eGamma - ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma)) - (vi1' `face` gamma)) - es'' - - - vsi1' = Map.map constPath $ border vi1' es' `unionSystem` vsi1 - - vi1'' = compLine (constPath bi1) vi1' - (Map.map snd uls'' `unionSystem` vsi1') - - usi1'' = Map.mapWithKey (\gamma _ -> - if gamma `Map.member` usi1' then usi1' ! gamma - else fst (uls'' ! gamma)) - esI1 - - --- Grad Lemma, takes a line eq in U, a system us and a value v, s.t. f us = --- border v. Outputs (u,p) s.t. border u = us and a path p between v --- and f u, where f is transNegLine eq -gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val) -gradLemmaU b eq us v = (u, VPath i theta'') - where i:j:_ = freshs (b,eq,us,v) - a = eq @@ One - g = transLine - f = transNegLine - s e b = VPath j $ compNeg j (e @@ j) (trans j (e @@ j) b) - (mkSystem [(j ~> 0, transFill j (e @@ j) b) - ,(j ~> 1, transFillNeg j (e @@ j) - (trans j (e @@ j) b))]) - t e a = VPath j $ comp j (e @@ j) (transNeg j (e @@ j) a) - (mkSystem [(j ~> 0, transFill j (e @@ j) - (transNeg j (e @@ j) a)) - ,(j ~> 1, transFillNeg j (e @@ j) a)]) - gv = g eq v - us' = mapWithKey (\alpha uAlpha -> - t (eq `face` alpha) uAlpha @@ i) us - theta = fill i a gv us' - u = comp i a gv us' -- Same as "theta `face` (i ~> 1)" - ws = insertSystem (i ~> 0) gv $ - insertSystem (i ~> 1) (t eq u @@ j) $ - mapWithKey - (\alpha uAlpha -> - t (eq `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us - theta' = compNeg j a theta ws - xs = insertSystem (i ~> 0) (s eq v @@ j) $ - insertSystem (i ~> 1) (s eq (f eq u) @@ j) $ - mapWithKey - (\alpha uAlpha -> - s (eq `face` alpha) (f (eq `face` alpha) uAlpha) @@ j) us - theta'' = comp j b (f eq theta') xs - ------------------------------------------------------------------------------- -- | Conversion @@ -741,7 +639,6 @@ instance Convertible Val where (VGlue v hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos') (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') (VUnGlueElem u _ _,VUnGlueElem u' _ _) -> conv ns u u' - (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' _ -> False instance Convertible Ctxt where @@ -797,8 +694,6 @@ instance Normal Val where VGlue u hisos -> glue (normal ns u) (normal ns hisos) VGlueElem u us -> glueElem (normal ns u) (normal ns us) VUnGlueElem u b hs -> unGlue (normal ns u) (normal ns b) (normal ns hs) - VUnGlueElemU u b es -> unGlueU (normal ns u) (normal ns b) (normal ns es) - VCompU u es -> compUniv (normal ns u) (normal ns es) VVar x t -> VVar x t -- (normal ns t) VFst t -> fstVal (normal ns t) VSnd t -> sndVal (normal ns t) diff --git a/TypeChecker.hs b/TypeChecker.hs index 82f51bf..aa53316 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -191,7 +191,9 @@ check a t = case (a,t) of ns <- asks names rho <- asks env unlessM (a === eval rho a') $ - throwError "check: lam types don't match" + throwError $ "check: lam types don't match" + ++ "\nlambda type annotation: " ++ show a' + ++ "\ndomain of Pi: " ++ show a let var = mkVarNice ns x a local (addTypeVal (x,a)) $ check (app f var) t (VSigma a f, Pair t1 t2) -> do diff --git a/examples/bool.ctt b/examples/bool.ctt index 8825eea..9dcc6ba 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -83,5 +83,5 @@ test8 : Id U F2 F2 = test9 : Id U F2 F2 = transport ( Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) -p : Id U F2 bool = comp U bool [ (i = 0) -> boolEqF2 ] +p : Id U F2 bool = comp (<_>U) bool [ (i = 0) -> boolEqF2 ] q : Id U F2 F2 = p @ (i /\ - i) \ No newline at end of file diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt index eae59df..03bb539 100644 --- a/examples/newhedberg.ctt +++ b/examples/newhedberg.ctt @@ -8,7 +8,7 @@ hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) ((f a (refl A a))) hedberg (A:U) (a b:A) (h: (x:A) -> stable (Id A a x)) (p q : Id A a b) : Id (Id A a b) p q = - comp A a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j] + comp (<_> A) a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j] where ra : Id A a a = refl A a rem1 (x:A) : exConst (Id A a x) = stableConst (Id A a x) (h x) diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 9251182..ce3b7e7 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -41,7 +41,7 @@ J (A : U) (a : A) (C : (x : A) -> Id A a x -> U) inv (A : U) (a b : A) (p : Id A a b) : Id A b a = p @ -i compId (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 = 1) -> q, (i=0) -> <_> a ] + comp (<_>A) (p @ i) [ (i = 1) -> q, (i=0) -> <_> a ] compId' (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = subst A (Id A a) b c q p @@ -52,7 +52,7 @@ compId'' (A : U) (a b : A) (p : Id A a b) : (c : A) -> (q : Id A b c) -> Id A a compUp (A : U) (a a' b b' : A) (p : Id A a a') (q : Id A b b') (r : Id A a b) : Id A a' b' = - comp A (r @ i) [(i = 0) -> p, (i = 1) -> q] + comp (<_>A) (r @ i) [(i = 0) -> p, (i = 1) -> q] compDown (A : U) (a a' b b' : A) (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b = @@ -72,7 +72,7 @@ test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) 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 ] + comp (<_>A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] -- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) -- (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' = @@ -107,7 +107,7 @@ Square (A : U) (a0 a1 : A) (u : Id A a0 a1) = IdP ( (IdP ( A) (u @ i) (v @ i))) r0 r1 constSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p = - comp A a + comp (<_>A) a [(i = 0) -> p @ (j \/ - k), (i = 1) -> p @ (j /\ k), (j = 0) -> p @ (i \/ - k), @@ -118,7 +118,7 @@ set (A : U) : U = (a b : A) -> prop (Id A a b) groupoid (A : U) : U = (a b : A) -> set (Id A a b) propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q = - comp A a [ (i=0) -> h a a + 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)] -- 2.34.1