From: Simon Huber Date: Wed, 29 Apr 2015 14:16:03 +0000 (+0200) Subject: added glueLine (wip) X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=555527f1ae0bd534c2ca8c8982b579cc2aa42094;p=cubicaltt.git added glueLine (wip) --- diff --git a/CTT.hs b/CTT.hs index e4c49ff..53fed2f 100644 --- a/CTT.hs +++ b/CTT.hs @@ -112,6 +112,9 @@ data Ter = App Ter Ter -- Glue | Glue Ter (System Ter) | GlueElem Ter (System Ter) + -- GlueLine: connecting any type to its glue with identities + | GlueLine Ter Formula Formula + | GlueLineElem Ter Formula Formula deriving Eq -- For an expression t, returns (u,ts) where u is no application and t = u ts @@ -150,6 +153,10 @@ data Val = VU | VGlue Val (System Val) | VGlueElem Val (System Val) + -- GlueLine values + | VGlueLine Val Formula Formula + | VGlueLineElem Val Formula Formula + -- Universe Composition Values | VCompElem Val (System Val) Val (System Val) | VElimComp Val (System Val) Val @@ -207,6 +214,10 @@ isNeutralComp (VGlue _ as) u ts | isNeutral u = True testFace beta _ = let shasBeta = shas `face` beta in shasBeta /= Map.empty && eps `Map.notMember` shasBeta in isNeutralSystem (Map.filterWithKey testFace ts) +-- isNeutralComp (VGlueLine _ phi psi) u ts | isNeutral u = True +-- | otherwise = +-- let fs = invFormula psi One +-- in isNeutralSystem () isNeutralComp _ _ _ = False @@ -345,6 +356,10 @@ showTer v = case v of 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) @@ -399,6 +414,10 @@ showVal v = case v of 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) + VGlueLine a phi psi -> text "glueLine" <+> showVal1 a <+> + showFormula phi <+> showFormula psi + VGlueLineElem a phi psi -> text "glueLineElem" <+> showVal1 a <+> + showFormula phi <+> showFormula psi 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) diff --git a/Eval.hs b/Eval.hs index 3f2b1b8..c4135d3 100644 --- a/Eval.hs +++ b/Eval.hs @@ -48,28 +48,30 @@ instance Nominal Env where instance Nominal Val where support v = case v of - VU -> [] - Ter _ e -> support e - VPi u v -> support [u,v] - VComp a u ts -> support (a,u,ts) - VIdP a v0 v1 -> support [a,v0,v1] - VPath i v -> i `delete` support v - VTrans u v -> support (u,v) - VSigma u v -> support (u,v) - VPair u v -> support (u,v) - VFst u -> support u - VSnd u -> support u - VCon _ vs -> support vs - VPCon _ a vs phis -> support (a,vs,phis) - VVar _ v -> support v - VApp u v -> support (u,v) - VLam _ u v -> support (u,v) - VAppFormula u phi -> support (u,phi) - VSplit u v -> support (u,v) - VGlue a ts -> support (a,ts) - VGlueElem a ts -> support (a,ts) - VCompElem a es u us -> support (a,es,u,us) - VElimComp a es u -> support (a,es,u) + VU -> [] + Ter _ e -> support e + VPi u v -> support [u,v] + VComp a u ts -> support (a,u,ts) + VIdP a v0 v1 -> support [a,v0,v1] + VPath i v -> i `delete` support v + VTrans u v -> support (u,v) + VSigma u v -> support (u,v) + VPair u v -> support (u,v) + VFst u -> support u + VSnd u -> support u + VCon _ vs -> support vs + VPCon _ a vs phis -> support (a,vs,phis) + VVar _ v -> support v + VApp u v -> support (u,v) + VLam _ u v -> support (u,v) + VAppFormula u phi -> support (u,phi) + VSplit u v -> support (u,v) + VGlue a ts -> support (a,ts) + VGlueElem a ts -> support (a,ts) + VGlueLine a phi psi -> support (a,phi,psi) + VGlueLineElem a phi psi -> support (a,phi,psi) + VCompElem a es u us -> support (a,es,u,us) + VElimComp a es u -> support (a,es,u) act u (i, phi) = let acti :: Nominal a => a -> a @@ -85,50 +87,54 @@ instance Nominal Val where | j `notElem` sphi -> VPath j (acti v) | otherwise -> VPath k (acti (v `swap` (j,k))) where k = fresh (v,Atom i,phi) - VTrans u v -> transLine (acti u) (acti v) - VSigma a f -> VSigma (acti a) (acti f) - VPair u v -> VPair (acti u) (acti v) - VFst u -> fstVal (acti u) - VSnd u -> sndVal (acti u) - VCon c vs -> VCon c (acti vs) - VPCon c a vs phis -> pcon c (acti a) (acti vs) (acti phis) - VVar x v -> VVar x (acti v) - VAppFormula u psi -> acti u @@ acti psi - VApp u v -> app (acti u) (acti v) - VLam x t u -> VLam x (acti t) (acti u) - VSplit u v -> app (acti u) (acti v) - VGlue a ts -> glue (acti a) (acti ts) - VGlueElem a ts -> glueElem (acti a) (acti ts) - VCompElem a es u us -> compElem (acti a) (acti es) (acti u) (acti us) - VElimComp a es u -> elimComp (acti a) (acti es) (acti u) + VTrans u v -> transLine (acti u) (acti v) + VSigma a f -> VSigma (acti a) (acti f) + VPair u v -> VPair (acti u) (acti v) + VFst u -> fstVal (acti u) + VSnd u -> sndVal (acti u) + VCon c vs -> VCon c (acti vs) + VPCon c a vs phis -> pcon c (acti a) (acti vs) (acti phis) + VVar x v -> VVar x (acti v) + VAppFormula u psi -> acti u @@ acti psi + VApp u v -> app (acti u) (acti v) + VLam x t u -> VLam x (acti t) (acti u) + VSplit u v -> app (acti u) (acti v) + VGlue a ts -> glue (acti a) (acti ts) + VGlueElem a ts -> glueElem (acti a) (acti ts) + VGlueLine a phi psi -> glueLine (acti a) (acti phi) (acti psi) + VGlueLineElem a phi psi -> glueLineElem (acti a) (acti phi) (acti psi) + VCompElem a es u us -> compElem (acti a) (acti es) (acti u) (acti us) + VElimComp a es u -> elimComp (acti a) (acti es) (acti u) -- This increases efficiency as it won't trigger computation. swap u ij@(i,j) = let sw :: Nominal a => a -> a sw u = swap u ij in case u of - VU -> VU - Ter t e -> Ter t (sw e) - VPi a f -> VPi (sw a) (sw f) - VComp a v ts -> VComp (sw a) (sw v) (sw ts) - VIdP a u v -> VIdP (sw a) (sw u) (sw v) - VPath k v -> VPath (swapName k ij) (sw v) - VTrans u v -> VTrans (sw u) (sw v) - VSigma a f -> VSigma (sw a) (sw f) - VPair u v -> VPair (sw u) (sw v) - VFst u -> VFst (sw u) - VSnd u -> VSnd (sw u) - VCon c vs -> VCon c (sw vs) - VPCon c a vs phis -> VPCon c (sw a) (sw vs) (sw phis) - VVar x v -> VVar x (sw v) - VAppFormula u psi -> VAppFormula (sw u) (sw psi) - VApp u v -> VApp (sw u) (sw v) - VLam x u v -> VLam x (sw u) (sw v) - VSplit u v -> VSplit (sw u) (sw v) - VGlue a ts -> VGlue (sw a) (sw ts) - VGlueElem a ts -> VGlueElem (sw a) (sw ts) - VCompElem a es u us -> VCompElem (sw a) (sw es) (sw u) (sw us) - VElimComp a es u -> VElimComp (sw a) (sw es) (sw u) + VU -> VU + Ter t e -> Ter t (sw e) + VPi a f -> VPi (sw a) (sw f) + VComp a v ts -> VComp (sw a) (sw v) (sw ts) + VIdP a u v -> VIdP (sw a) (sw u) (sw v) + VPath k v -> VPath (swapName k ij) (sw v) + VTrans u v -> VTrans (sw u) (sw v) + VSigma a f -> VSigma (sw a) (sw f) + VPair u v -> VPair (sw u) (sw v) + VFst u -> VFst (sw u) + VSnd u -> VSnd (sw u) + VCon c vs -> VCon c (sw vs) + VPCon c a vs phis -> VPCon c (sw a) (sw vs) (sw phis) + VVar x v -> VVar x (sw v) + VAppFormula u psi -> VAppFormula (sw u) (sw psi) + VApp u v -> VApp (sw u) (sw v) + VLam x u v -> VLam x (sw u) (sw v) + VSplit u v -> VSplit (sw u) (sw v) + VGlue a ts -> VGlue (sw a) (sw ts) + VGlueElem a ts -> VGlueElem (sw a) (sw ts) + VGlueLine a phi psi -> VGlueLine (sw a) (sw phi) (sw psi) + VGlueLineElem a phi psi -> VGlueLineElem (sw a) (sw phi) (sw psi) + VCompElem a es u us -> VCompElem (sw a) (sw es) (sw u) (sw us) + VElimComp a es u -> VElimComp (sw a) (sw es) (sw u) ----------------------------------------------------------------------- -- The evaluator @@ -161,6 +167,10 @@ eval rho v = case v of Comp a t0 ts -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts) Glue a ts -> glue (eval rho a) (evalSystem rho ts) GlueElem a ts -> glueElem (eval rho a) (evalSystem rho ts) + GlueLine a phi psi -> + glueLine (eval rho a) (evalFormula rho phi) (evalFormula rho psi) + GlueLineElem a phi psi -> + glueLineElem (eval rho a) (evalFormula rho phi) (evalFormula rho psi) CompElem a es u us -> compElem (eval rho a) (evalSystem rho es) (eval rho u) (evalSystem rho us) ElimComp a es u -> elimComp (eval rho a) (evalSystem rho es) (eval rho u) @@ -318,6 +328,7 @@ trans i v0 v1 = case (v0,v1) of _ | isNeutral w -> w where w = VTrans (VPath i v0) v1 (VGlue a ts,_) -> transGlue i a ts v1 + (VGlueLine a phi psi,_) -> transGlueLine i a phi psi v1 (VComp VU a es,_) -> transU i a es v1 (Ter (Sum _ _ nass) env,VComp b w ws) -> comp k v01 (trans i v0 w) ws' where v01 = v0 `face` (i ~> 1) -- b is vi0 and independent of j @@ -368,6 +379,10 @@ genComp i a u ts = comp i ai1 (trans i a u) ts' ts' = mapWithKey (\alpha -> squeeze i (a `face` alpha)) ts genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i) +fillLine :: Val -> Val -> System Val -> Val +fillLine a u ts = VPath i $ fill i a u (Map.map (@@ i) ts) + where i = fresh (a,u,ts) + fill, fillNeg :: Name -> Val -> Val -> System Val -> Val fill i a u ts = comp j a u (ts `conj` (i,j)) where j = fresh (Atom i,a,u,ts) @@ -408,6 +423,7 @@ comp i a u ts = case a of where w = VComp a u (Map.map (VPath i) ts) VComp VU a es -> compU i a es u ts VGlue b hisos -> compGlue i b hisos u ts + VGlueLine b phi psi -> compGlueLine i b phi psi u ts Ter (Sum _ _ nass) env -> case u of VCon n us -> case lookupLabel n nass of Just as -> @@ -544,7 +560,8 @@ pathComp i a u u' us = VPath j $ comp i a (u `face` (i ~> 0)) us' -- outputs u s.t. border u = us and an L-path between v and sigma u -- an theta is a L path if L-border theta is constant gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val) -gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = (u, VPath i theta'') +gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = + (u, VPath i theta'') where i:j:_ = freshs (a,hiso,us,v) us' = mapWithKey (\alpha uAlpha -> app (t `face` alpha) uAlpha @@ i) us @@ -563,6 +580,122 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = (u, VPath i th theta'' = comp j b (app f theta') xs +------------------------------------------------------------------------------- +-- | GlueLine + + +glueLine :: Val -> Formula -> Formula -> Val +glueLine t _ (Dir Zero) = t +glueLine t (Dir _) _ = t +glueLine t phi (Dir One) = glue t isos + where isos = mkSystem (map (\alpha -> (alpha,idIso (t `face` alpha))) + (invFormula phi Zero)) +glueLine t phi psi = VGlueLine t phi psi + +idIso :: Val -> Val +idIso a = VPair a $ VPair idV $ VPair idV $ VPair refl refl + where idV = Ter (Lam "x" (Var "A") (Var "x")) (Upd Empty ("A",a)) + refl = Ter (Lam "x" (Var "A") (Path (Name "i") (Var "x"))) + (Upd Empty ("A",a)) + +glueLineElem :: Val -> Formula -> Formula -> Val +glueLineElem u (Dir _) _ = u +glueLineElem u _ (Dir Zero) = u +glueLineElem u phi (Dir One) = glueElem u ss + where ss = mkSystem (map (\alpha -> (alpha,u `face` alpha)) + (invFormula phi Zero)) +glueLineElem u phi psi = VGlueLineElem u phi psi + +unGlueLine :: Val -> Formula -> Formula -> Val -> Val +unGlueLine b phi psi u = case (phi,psi,u) of + (Dir _,_,_) -> u + (_,Dir Zero,_) -> u + (_,Dir One,_) -> + let isos = mkSystem (map (\alpha -> (alpha,idIso (b `face` alpha))) + (invFormula phi Zero)) + in unGlue isos u + (_,_,VGlueLineElem w _ _ ) -> w + (_,_,_) -> error ("UnGlueLine, should be VGlueLineElem " ++ show u) + +compGlueLine :: Name -> Val -> Formula -> Formula -> Val -> System Val -> Val +compGlueLine i b phi psi u us = glueLineElem vm phi psi + where fs = invFormula psi One + ws = Map.mapWithKey + (\alpha -> unGlueLine (b `face` alpha) + (phi `face` alpha) (psi `face` alpha)) us + w = unGlueLine b phi psi u + v = comp i b w ws + + lss = mkSystem $ map + (\alpha -> + (alpha,(face phi alpha,face b alpha, + face us alpha,face u alpha))) fs + ls = Map.mapWithKey (\alpha vAlpha -> + auxGlueLine i vAlpha (v `face` alpha)) lss + + vm = compLine b v ls + +auxGlueLine :: Name -> (Formula,Val,System Val,Val) -> Val -> Val +auxGlueLine i (Dir _,b,ws,wi0) vi1 = VPath j vi1 where j = fresh vi1 +auxGlueLine i (phi,b,ws,wi0) vi1 = fillLine b vi1 ls' + where hisos = mkSystem (map (\alpha -> + (alpha,idIso (b `face` alpha))) (invFormula phi Zero)) + vs = Map.mapWithKey (\alpha -> unGlue (hisos `face` alpha)) ws + vi0 = unGlue hisos wi0 -- in b + + v = fill i b vi0 vs -- in b + + us' = Map.mapWithKey (\gamma _ -> + fill i (b `face` gamma) (wi0 `face` gamma) + (ws `face` gamma)) + hisos + + ls' = Map.mapWithKey (\gamma _ -> + pathComp i (b `face` gamma) (v `face` gamma) + (us' ! gamma) (vs `face` gamma)) + hisos + +transGlueLine :: Name -> Val -> Formula -> Formula -> Val -> Val +transGlueLine i b phi psi u = glueLineElem vm phii1 psii1 + where fs = filter (i `Map.notMember`) (invFormula psi One) + phii1 = phi `face` (i ~> 1) + psii1 = psi `face` (i ~> 1) + phii0 = phi `face` (i ~> 0) + psii0 = psi `face` (i ~> 0) + bi1 = b `face` (i ~> 1) + bi0 = b `face` (i ~> 0) + lss = mkSystem (map (\ alpha -> + (alpha,(face phi alpha,face b alpha,face u alpha))) fs) + ls = Map.mapWithKey (\alpha vAlpha -> + auxTransGlueLine i vAlpha (v `face` alpha)) lss + v = trans i b w + w = unGlueLine bi0 phii0 psii0 u + vm = compLine bi1 v ls + + + +auxTransGlueLine :: Name -> (Formula,Val,Val) -> Val -> Val +auxTransGlueLine i (Dir _,b,wi0) vi1 = VPath j vi1 where j = fresh vi1 +auxTransGlueLine i (phi,b,wi0) vi1 = fillLine (b `face` (i ~> 1)) vi1 ls' + where hisos = mkSystem (map (\ alpha -> + (alpha,idIso (b `face` alpha))) (invFormula phi Zero)) + vi0 = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0) + + v = transFill i b vi0 -- in b + + -- set of elements in hisos independent of i + hisos' = Map.filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos + + us' = Map.mapWithKey (\gamma _ -> + transFill i (b `face` gamma) (wi0 `face` gamma)) + hisos' + + ls' = Map.mapWithKey (\gamma _ -> + VPath i $ squeeze i (b `face` gamma) (us' ! gamma)) + hisos' + + + ------------------------------------------------------------------------------- -- | Composition in the Universe diff --git a/Exp.cf b/Exp.cf index 0daa71e..8958783 100644 --- a/Exp.cf +++ b/Exp.cf @@ -22,28 +22,30 @@ separator Decl ";" ; Where. ExpWhere ::= Exp "where" "{" [Decl] "}" ; NoWhere. ExpWhere ::= Exp ; -Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ; -Lam. Exp ::= "\\" [PTele] "->" Exp ; -Path. Exp ::= "<" [AIdent] ">" Exp ; -Fun. Exp1 ::= Exp2 "->" Exp1 ; -Pi. Exp1 ::= [PTele] "->" Exp1 ; -Sigma. Exp1 ::= [PTele] "*" Exp1 ; -AppFormula. Exp2 ::= Exp2 "@" Formula ; -App. Exp2 ::= Exp2 Exp3 ; -IdP. Exp3 ::= "IdP" Exp4 Exp4 Exp4 ; -Trans. Exp3 ::= "transport" Exp4 Exp4 ; -Comp. Exp3 ::= "comp" Exp4 Exp4 System ; -Glue. Exp3 ::= "glue" Exp4 System ; -GlueElem. Exp3 ::= "glueElem" Exp4 System ; -CompElem. Exp3 ::= "compElem" Exp4 System Exp4 System ; -ElimComp. Exp3 ::= "elimComp" Exp4 System Exp4 ; -Fst. Exp4 ::= Exp4 ".1" ; -Snd. Exp4 ::= Exp4 ".2" ; -Pair. Exp5 ::= "(" Exp "," [Exp] ")" ; -Var. Exp5 ::= AIdent ; -PCon. Exp5 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi -U. Exp5 ::= "U" ; -Hole. Exp5 ::= HoleIdent ; +Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ; +Lam. Exp ::= "\\" [PTele] "->" Exp ; +Path. Exp ::= "<" [AIdent] ">" Exp ; +Fun. Exp1 ::= Exp2 "->" Exp1 ; +Pi. Exp1 ::= [PTele] "->" Exp1 ; +Sigma. Exp1 ::= [PTele] "*" Exp1 ; +AppFormula. Exp2 ::= Exp2 "@" Formula ; +App. Exp2 ::= Exp2 Exp3 ; +IdP. Exp3 ::= "IdP" Exp4 Exp4 Exp4 ; +Trans. Exp3 ::= "transport" Exp4 Exp4 ; +Comp. Exp3 ::= "comp" Exp4 Exp4 System ; +Glue. Exp3 ::= "glue" Exp4 System ; +GlueElem. Exp3 ::= "glueElem" Exp4 System ; +CompElem. Exp3 ::= "compElem" Exp4 System Exp4 System ; +GlueLine. Exp3 ::= "glueLine" Formula Formula Exp4 ; +GlueLineElem. Exp3 ::= "glueLineElem" Formula Formula Exp4 ; +ElimComp. Exp3 ::= "elimComp" Exp4 System Exp4 ; +Fst. Exp4 ::= Exp4 ".1" ; +Snd. Exp4 ::= Exp4 ".2" ; +Pair. Exp5 ::= "(" Exp "," [Exp] ")" ; +Var. Exp5 ::= AIdent ; +PCon. Exp5 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi +U. Exp5 ::= "U" ; +Hole. Exp5 ::= HoleIdent ; coercions Exp 5 ; separator nonempty Exp "," ; diff --git a/Resolver.hs b/Resolver.hs index bbca155..e8a2d8d 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -213,6 +213,11 @@ resolveExp e = case e of (throwError $ "Not a system of isomorphisms: " ++ show rs) CTT.Glue <$> resolveExp u <*> pure rs GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts + GlueLine phi psi u -> + CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi + GlueLineElem phi psi u -> + CTT.GlueLineElem <$> resolveExp u <*> resolveFormula phi + <*> resolveFormula psi CompElem a es t ts -> CTT.CompElem <$> resolveExp a <*> resolveSystem es <*> resolveExp t <*> resolveSystem ts ElimComp a es t -> CTT.ElimComp <$> resolveExp a <*> resolveSystem es <*> resolveExp t diff --git a/TypeChecker.hs b/TypeChecker.hs index e11c951..3123568 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -208,6 +208,14 @@ check a t = case (a,t) of check va u vu <- evalTyping u checkGlueElem vu ts us + (VU,GlueLine b phi psi) -> do + check VU b + checkFormula phi + checkFormula psi + (VGlueLine vb phi psi,GlueLineElem r phi' psi') -> do + check vb r + unlessM ((phi,psi) === (phi',psi')) $ + throwError $ "GlueLineElem: formulas don't match" _ -> do v <- infer t unlessM (v === a) $ diff --git a/examples/prelude.ctt b/examples/prelude.ctt index f2b8f0c..9c39a43 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -84,6 +84,12 @@ isoId (A B : U) (f : A -> B) (g : B -> A) (t : (x:A) -> Id A (g (f x)) x) : Id U A B = glue B [ (i = 0) -> (A,f,g,s,t) ] +idfun (A : U) (a : A) : A = a + +isoIdRef (A : U) : + Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) = + glueLine j i A + -- u -- a0 -----> a1 -- | | @@ -187,6 +193,4 @@ discrete (A : U) : U = (a b : A) -> dec (Id A a b) injective (A B : U) (f : A -> B) : U = (a0 a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1 -idfun (A : U) (a : A) : A = a - and (A B : U) : U = (_ : A) * B