From: Rafaël Bocquet Date: Tue, 12 Apr 2016 13:02:26 +0000 (+0200) Subject: Opaque/Visible definitions X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=23dfbddfa9a0df75945fca8a5c626f4486d843ad;p=cubicaltt.git Opaque/Visible definitions --- diff --git a/CTT.hs b/CTT.hs index e3d42f9..c92fff2 100644 --- a/CTT.hs +++ b/CTT.hs @@ -7,6 +7,8 @@ import Data.Maybe import Data.Map (Map,(!),filterWithKey,elems) import qualified Data.Map as Map import Text.PrettyPrint as PP +import Data.Set (Set) +import qualified Data.Set as Set import Connections @@ -34,7 +36,11 @@ data Branch = OBranch LIdent [Ident] Ter deriving (Eq,Show) -- Declarations: x : A = e -type Decl = (Ident,(Ter,Ter)) +type Decl = (Ident,(Ter,Ter)) +data Decls = MutualDecls [Decl] + | OpaqueDecl Ident + | VisibleDecl Ident + deriving Eq declIdents :: [Decl] -> [Ident] declIdents decls = [ x | (x,_) <- decls ] @@ -80,7 +86,7 @@ lookupBranch x (b:brs) = case b of data Ter = App Ter Ter | Pi Ter | Lam Ident Ter Ter - | Where Ter [Decl] + | Where Ter Decls | Var Ident | U -- Sigma types: @@ -123,7 +129,7 @@ mkApps :: Ter -> [Ter] -> Ter mkApps (Con l us) vs = Con l (us ++ vs) mkApps t ts = foldl App t ts -mkWheres :: [[Decl]] -> Ter -> Ter +mkWheres :: [Decls] -> Ter -> Ter mkWheres [] e = e mkWheres (d:ds) e = Where (mkWheres ds e) d @@ -156,6 +162,7 @@ data Val = VU -- Neutral values: | VVar Ident Val + | VOpaque Ident Val | VFst Val | VSnd Val | VSplit Val Val @@ -167,18 +174,19 @@ data Val = VU isNeutral :: Val -> Bool isNeutral v = case v of - Ter Undef{} _ -> True - Ter Hole{} _ -> True - VVar{} -> True - VComp{} -> True - VFst{} -> True - VSnd{} -> True - VSplit{} -> True - VApp{} -> True - VAppFormula{} -> True - VUnGlueElemU{} -> True - VUnGlueElem{} -> True - _ -> False + Ter Undef{} _ -> True + Ter Hole{} _ -> True + VVar{} -> True + VOpaque{} -> True + VComp{} -> True + VFst{} -> True + VSnd{} -> True + VSplit{} -> True + VApp{} -> True + VAppFormula{} -> True + VUnGlueElemU{} -> True + VUnGlueElem{} -> True + _ -> False isNeutralSystem :: System Val -> Bool isNeutralSystem = any isNeutral . elems @@ -219,19 +227,22 @@ data Ctxt = Empty -- The Idents and Names in the Ctxt refer to the elements in the two -- lists. This is more efficient because acting on an environment now -- only need to affect the lists and not the whole context. -type Env = (Ctxt,[Val],[Formula]) +-- The last list is the list of opaque names +type Env = (Ctxt,[Val],[Formula],Nameless (Set Ident)) emptyEnv :: Env -emptyEnv = (Empty,[],[]) +emptyEnv = (Empty,[],[],Nameless Set.empty) -def :: [Decl] -> Env -> Env -def ds (rho,vs,fs) = (Def ds rho,vs,fs) +def :: Decls -> Env -> Env +def (MutualDecls ds) (rho,vs,fs,Nameless os) = (Def ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds))) +def (OpaqueDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.insert n os)) +def (VisibleDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.delete n os)) sub :: (Name,Formula) -> Env -> Env -sub (i,phi) (rho,vs,fs) = (Sub i rho,vs,phi:fs) +sub (i,phi) (rho,vs,fs,os) = (Sub i rho,vs,phi:fs,os) upd :: (Ident,Val) -> Env -> Env -upd (x,v) (rho,vs,fs) = (Upd x rho,v:vs,fs) +upd (x,v) (rho,vs,fs,Nameless os) = (Upd x rho,v:vs,fs,Nameless (Set.delete x os)) upds :: [(Ident,Val)] -> Env -> Env upds xus rho = foldl (flip upd) rho xus @@ -243,10 +254,10 @@ subs :: [(Name,Formula)] -> Env -> Env subs iphis rho = foldl (flip sub) rho iphis mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env -mapEnv f g (rho,vs,fs) = (rho,map f vs,map g fs) +mapEnv f g (rho,vs,fs,os) = (rho,map f vs,map g fs,os) valAndFormulaOfEnv :: Env -> ([Val],[Formula]) -valAndFormulaOfEnv (_,vs,fs) = (vs,fs) +valAndFormulaOfEnv (_,vs,fs,_) = (vs,fs) valOfEnv :: Env -> [Val] valOfEnv = fst . valAndFormulaOfEnv @@ -255,7 +266,7 @@ formulaOfEnv :: Env -> [Formula] formulaOfEnv = snd . valAndFormulaOfEnv domainEnv :: Env -> [Name] -domainEnv (rho,_,_) = domCtxt rho +domainEnv (rho,_,_,_) = domCtxt rho where domCtxt rho = case rho of Empty -> [] Upd _ e -> domCtxt e @@ -265,11 +276,11 @@ domainEnv (rho,_,_) = domCtxt rho -- Extract the context from the environment, used when printing holes contextOfEnv :: Env -> [String] contextOfEnv rho = case rho of - (Empty,_,_) -> [] - (Upd x e,VVar n t:vs,fs) -> (n ++ " : " ++ show t) : contextOfEnv (e,vs,fs) - (Upd x e,v:vs,fs) -> (x ++ " = " ++ show v) : contextOfEnv (e,vs,fs) - (Def _ e,vs,fs) -> contextOfEnv (e,vs,fs) - (Sub i e,vs,phi:fs) -> (show i ++ " = " ++ show phi) : contextOfEnv (e,vs,fs) + (Empty,_,_,_) -> [] + (Upd x e,VVar n t:vs,fs,os) -> (n ++ " : " ++ show t) : contextOfEnv (e,vs,fs,os) + (Upd x e,v:vs,fs,os) -> (x ++ " = " ++ show v) : contextOfEnv (e,vs,fs,os) + (Def _ e,vs,fs,os) -> contextOfEnv (e,vs,fs,os) + (Sub i e,vs,phi:fs,os) -> (show i ++ " = " ++ show phi) : contextOfEnv (e,vs,fs,os) -------------------------------------------------------------------------------- -- | Pretty printing @@ -284,19 +295,19 @@ showEnv b e = par x = if b then parens x else x com = if b then comma else PP.empty showEnv1 e = case e of - (Upd x env,u:us,fs) -> - showEnv1 (env,us,fs) <+> names x <+> showVal1 u <> com - (Sub i env,us,phi:fs) -> - showEnv1 (env,us,fs) <+> names (show i) <+> text (show phi) <> com - (Def _ env,vs,fs) -> showEnv1 (env,vs,fs) - _ -> showEnv b e + (Upd x env,u:us,fs,os) -> + showEnv1 (env,us,fs,os) <+> names x <+> showVal1 u <> com + (Sub i env,us,phi:fs,os) -> + showEnv1 (env,us,fs,os) <+> names (show i) <+> text (show phi) <> com + (Def _ env,vs,fs,os) -> showEnv1 (env,vs,fs,os) + _ -> showEnv b e in case e of - (Empty,_,_) -> PP.empty - (Def _ env,vs,fs) -> showEnv b (env,vs,fs) - (Upd x env,u:us,fs) -> - par $ showEnv1 (env,us,fs) <+> names x <+> showVal u - (Sub i env,us,phi:fs) -> - par $ showEnv1 (env,us,fs) <+> names (show i) <+> text (show phi) + (Empty,_,_,_) -> PP.empty + (Def _ env,vs,fs,os) -> showEnv b (env,vs,fs,os) + (Upd x env,u:us,fs,os) -> + par $ showEnv1 (env,us,fs,os) <+> names x <+> showVal u + (Sub i env,us,phi:fs,os) -> + par $ showEnv1 (env,us,fs,os) <+> names (show i) <+> text (show phi) instance Show Loc where show = render . showLoc @@ -360,9 +371,12 @@ showTer1 t = case t of Snd{} -> showTer t _ -> parens (showTer t) -showDecls :: [Decl] -> Doc -showDecls defs = hsep $ punctuate comma - [ text x <+> equals <+> showTer d | (x,(_,d)) <- defs ] +showDecls :: Decls -> Doc +showDecls (MutualDecls defs) = + hsep $ punctuate comma + [ text x <+> equals <+> showTer d | (x,(_,d)) <- defs ] +showDecls (OpaqueDecl i) = text "opaque" <+> text i +showDecls (VisibleDecl i) = text "visible" <+> text i instance Show Val where show = render . showVal @@ -389,6 +403,7 @@ showVal v = case v of VPath{} -> char '<' <> showPath v VSplit u v -> showVal u <+> showVal1 v VVar x _ -> text x + VOpaque x _ -> text ('#':x) VFst u -> showVal1 u <> text ".1" VSnd u -> showVal1 u <> text ".2" VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] diff --git a/Connections.hs b/Connections.hs index c1031ea..077d575 100644 --- a/Connections.hs +++ b/Connections.hs @@ -292,6 +292,14 @@ unions = foldr union [] unionsMap :: Eq b => (a -> [b]) -> [a] -> [b] unionsMap f = unions . map f +newtype Nameless a = Nameless { unNameless :: a } + deriving (Eq, Ord) + +instance Nominal (Nameless a) where + support _ = [] + act x _ = x + swap x _ = x + instance Nominal () where support () = [] act () _ = () diff --git a/Eval.hs b/Eval.hs index 15d268f..148ea46 100644 --- a/Eval.hs +++ b/Eval.hs @@ -15,33 +15,34 @@ import CTT -- Lookup functions look :: String -> Env -> Val -look x (Upd y rho,v:vs,fs) | x == y = v - | otherwise = look x (rho,vs,fs) -look x r@(Def decls rho,vs,fs) = case lookup x decls of +look x (Upd y rho,v:vs,fs,os) | x == y = v + | otherwise = look x (rho,vs,fs,os) +look x r@(Def decls rho,vs,fs,Nameless os) = case lookup x decls of Just (_,t) -> eval r t - Nothing -> look x (rho,vs,fs) -look x (Sub _ rho,vs,_:fs) = look x (rho,vs,fs) -look x _ = error $ "look: not found " ++ show x + Nothing -> look x (rho,vs,fs,Nameless os) +look x (Sub _ rho,vs,_:fs,os) = look x (rho,vs,fs,os) +look x (Empty,_,_,_) = error $ "look: not found " ++ show x lookType :: String -> Env -> Val -lookType x (Upd y rho,VVar _ a:vs,fs) - | x == y = a - | otherwise = lookType x (rho,vs,fs) -lookType x r@(Def decls rho,vs,fs) = case lookup x decls of +lookType x (Upd y rho,v:vs,fs,os) + | x /= y = lookType x (rho,vs,fs,os) + | VVar _ a <- v = a + | otherwise = error "" +lookType x r@(Def decls rho,vs,fs,os) = case lookup x decls of Just (a,_) -> eval r a - Nothing -> lookType x (rho,vs,fs) -lookType x (Sub _ rho,vs,_:fs) = lookType x (rho,vs,fs) -lookType x _ = error $ "lookType: not found " ++ show x + Nothing -> lookType x (rho,vs,fs,os) +lookType x (Sub _ rho,vs,_:fs,os) = lookType x (rho,vs,fs,os) +lookType x (Empty,_,_,_) = error $ "lookType: not found " ++ show x lookName :: Name -> Env -> Formula -lookName i (Upd _ rho,v:vs,fs) = lookName i (rho,vs,fs) -lookName i (Def _ rho,vs,fs) = lookName i (rho,vs,fs) -lookName i (Sub j rho,vs,phi:fs) | i == j = phi - | otherwise = lookName i (rho,vs,fs) +lookName i (Upd _ rho,v:vs,fs,os) = lookName i (rho,vs,fs,os) +lookName i (Def _ rho,vs,fs,os) = lookName i (rho,vs,fs,os) +lookName i (Sub j rho,vs,phi:fs,os) | i == j = phi + | otherwise = lookName i (rho,vs,fs,os) lookName i _ = error $ "lookName: not found " ++ show i ------------------------------------------------------------------------ + ----------------------------------------------------------------------- -- Nominal instances instance Nominal Ctxt where @@ -65,6 +66,7 @@ instance Nominal Val where VPCon _ a vs phis -> support (a,vs,phis) VHComp a u ts -> support (a,u,ts) VVar _ v -> support v + VOpaque _ v -> support v VApp u v -> support (u,v) VLam _ u v -> support (u,v) VAppFormula u phi -> support (u,phi) @@ -98,6 +100,7 @@ instance Nominal Val where VPCon c a vs phis -> pcon c (acti a) (acti vs) (acti phis) VHComp a u us -> hComp (acti a) (acti u) (acti us) VVar x v -> VVar x (acti v) + VOpaque x v -> VOpaque 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) @@ -127,6 +130,7 @@ instance Nominal Val where VPCon c a vs phis -> VPCon c (sw a) (sw vs) (sw phis) VHComp a u us -> VHComp (sw a) (sw u) (sw us) VVar x v -> VVar x (sw v) + VOpaque x v -> VOpaque 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) @@ -142,10 +146,12 @@ instance Nominal Val where -- The evaluator eval :: Env -> Ter -> Val -eval rho v = case v of +eval rho@(_,_,_,Nameless os) v = case v of U -> VU App r s -> app (eval rho r) (eval rho s) - Var i -> look i rho + Var i + | i `elem` os -> VOpaque i t + | otherwise -> look i rho Pi t@(Lam _ a _) -> VPi (eval rho a) (eval rho t) Sigma t@(Lam _ a _) -> VSigma (eval rho a) (eval rho t) Pair a b -> VPair (eval rho a) (eval rho b) @@ -234,6 +240,7 @@ sndVal u = error $ "sndVal: " ++ show u ++ " is not neutral." inferType :: Val -> Val inferType v = case v of VVar _ t -> t + VOpaque _ t -> t Ter (Undef _ t) rho -> eval rho t VFst t -> case inferType t of VSigma a _ -> a @@ -820,6 +827,7 @@ instance Convertible Val where (VSnd u,VSnd u') -> conv ns u u' (VApp u v,VApp u' v') -> conv ns u u' && conv ns v v' (VSplit u v,VSplit u' v') -> conv ns u u' && conv ns v v' + (VOpaque x _, VOpaque x' _) -> x == x' (VVar x _, VVar x' _) -> x == x' (VIdP a b c,VIdP a' b' c') -> conv ns a a' && conv ns b b' && conv ns c c' (VPath i a,VPath i' a') -> conv ns (a `swap` (i,j)) (a' `swap` (i',j)) @@ -863,6 +871,8 @@ instance Convertible a => Convertible (System a) where instance Convertible Formula where conv _ phi psi = dnf phi == dnf psi +instance Convertible (Nameless a) where + conv _ _ _ = True ------------------------------------------------------------------------------- -- | Normalization @@ -900,6 +910,9 @@ instance Normal Val where VAppFormula u phi -> VAppFormula (normal ns u) (normal ns phi) _ -> v +instance Normal (Nameless a) where + normal _ = id + instance Normal Ctxt where normal _ = id diff --git a/Exp.cf b/Exp.cf index d0fbe72..d4a8784 100644 --- a/Exp.cf +++ b/Exp.cf @@ -12,13 +12,15 @@ Module. Module ::= "module" AIdent "where" "{" [Imp] [Decl] "}" ; Import. Imp ::= "import" AIdent ; separator Imp ";" ; -DeclDef. Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ; -DeclData. Decl ::= "data" AIdent [Tele] "=" [Label] ; -DeclHData. Decl ::= "hdata" AIdent [Tele] "=" [Label] ; -DeclSplit. Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ; -DeclUndef. Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ; -DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; -separator Decl ";" ; +DeclDef. Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ; +DeclData. Decl ::= "data" AIdent [Tele] "=" [Label] ; +DeclHData. Decl ::= "hdata" AIdent [Tele] "=" [Label] ; +DeclSplit. Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ; +DeclUndef. Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ; +DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; +DeclOpaque. Decl ::= "opaque" AIdent ; +DeclVisible. Decl ::= "visible" AIdent ; +separator Decl ";" ; Where. ExpWhere ::= Exp "where" "{" [Decl] "}" ; NoWhere. ExpWhere ::= Exp ; diff --git a/Main.hs b/Main.hs index 56536cc..77d5aac 100644 --- a/Main.hs +++ b/Main.hs @@ -97,8 +97,7 @@ initLoop flags f hist = do putStrLn $ "Resolver failed: " ++ err runInputT (settings []) (putHistory hist >> loop flags f [] TC.verboseEnv) Right (adefs,names) -> do - (merr,tenv) <- - TC.runDeclss TC.verboseEnv (takeWhile (\x -> fst (head x) /= "stop") adefs) + (merr,tenv) <- TC.runDeclss TC.verboseEnv adefs case merr of Just err -> putStrLn $ "Type checking failed: " ++ shrink err Nothing -> putStrLn "File loaded." diff --git a/Makefile b/Makefile index a81220b..23767e5 100644 --- a/Makefile +++ b/Makefile @@ -1,86 +1,51 @@ # DO NOT DELETE: Beginning of Haskell dependencies -Exp/ErrM.o Exp/ErrM._o : Exp/ErrM.hs -Exp/Abs.o Exp/Abs._o : Exp/Abs.hs -Exp/Skel.o Exp/Skel._o : Exp/Skel.hs +Exp/ErrM.o : Exp/ErrM.hs +Exp/Abs.o : Exp/Abs.hs +Exp/Skel.o : Exp/Skel.hs Exp/Skel.o : Exp/ErrM.hi -Exp/Skel._o : Exp/ErrM._hi Exp/Skel.o : Exp/Abs.hi -Exp/Skel._o : Exp/Abs._hi -Exp/Print.o Exp/Print._o : Exp/Print.hs +Exp/Print.o : Exp/Print.hs Exp/Print.o : Exp/Abs.hi -Exp/Print._o : Exp/Abs._hi -Exp/Lex.o Exp/Lex._o : Exp/Lex.hs -Exp/Par.o Exp/Par._o : Exp/Par.hs +Exp/Lex.o : Exp/Lex.hs +Exp/Par.o : Exp/Par.hs Exp/Par.o : Exp/ErrM.hi -Exp/Par._o : Exp/ErrM._hi Exp/Par.o : Exp/Lex.hi -Exp/Par._o : Exp/Lex._hi Exp/Par.o : Exp/Abs.hi -Exp/Par._o : Exp/Abs._hi -Exp/Layout.o Exp/Layout._o : Exp/Layout.hs +Exp/Layout.o : Exp/Layout.hs Exp/Layout.o : Exp/Lex.hi -Exp/Layout._o : Exp/Lex._hi -Exp/Test.o Exp/Test._o : Exp/Test.hs +Exp/Test.o : Exp/Test.hs Exp/Test.o : Exp/ErrM.hi -Exp/Test._o : Exp/ErrM._hi Exp/Test.o : Exp/Layout.hi -Exp/Test._o : Exp/Layout._hi Exp/Test.o : Exp/Abs.hi -Exp/Test._o : Exp/Abs._hi Exp/Test.o : Exp/Print.hi -Exp/Test._o : Exp/Print._hi Exp/Test.o : Exp/Skel.hi -Exp/Test._o : Exp/Skel._hi Exp/Test.o : Exp/Par.hi -Exp/Test._o : Exp/Par._hi Exp/Test.o : Exp/Lex.hi -Exp/Test._o : Exp/Lex._hi -Connections.o Connections._o : Connections.hs -CTT.o CTT._o : CTT.hs +Connections.o : Connections.hs +CTT.o : CTT.hs CTT.o : Connections.hi -CTT._o : Connections._hi -Eval.o Eval._o : Eval.hs +Eval.o : Eval.hs Eval.o : CTT.hi -Eval._o : CTT._hi Eval.o : Connections.hi -Eval._o : Connections._hi -Resolver.o Resolver._o : Resolver.hs +Resolver.o : Resolver.hs Resolver.o : Connections.hi -Resolver._o : Connections._hi Resolver.o : Connections.hi -Resolver._o : Connections._hi Resolver.o : CTT.hi -Resolver._o : CTT._hi Resolver.o : CTT.hi -Resolver._o : CTT._hi Resolver.o : Exp/Abs.hi -Resolver._o : Exp/Abs._hi -TypeChecker.o TypeChecker._o : TypeChecker.hs +TypeChecker.o : TypeChecker.hs TypeChecker.o : Eval.hi -TypeChecker._o : Eval._hi TypeChecker.o : CTT.hi -TypeChecker._o : CTT._hi TypeChecker.o : Connections.hi -TypeChecker._o : Connections._hi -Main.o Main._o : Main.hs +Main.o : Main.hs Main.o : Eval.hi -Main._o : Eval._hi Main.o : TypeChecker.hi -Main._o : TypeChecker._hi Main.o : Resolver.hi -Main._o : Resolver._hi Main.o : CTT.hi -Main._o : CTT._hi Main.o : Exp/ErrM.hi -Main._o : Exp/ErrM._hi Main.o : Exp/Layout.hi -Main._o : Exp/Layout._hi Main.o : Exp/Abs.hi -Main._o : Exp/Abs._hi Main.o : Exp/Print.hi -Main._o : Exp/Print._hi Main.o : Exp/Par.hi -Main._o : Exp/Par._hi Main.o : Exp/Lex.hi -Main._o : Exp/Lex._hi # DO NOT DELETE: End of Haskell dependencies diff --git a/Resolver.hs b/Resolver.hs index 3dfd8ef..f5414ec 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -325,7 +325,7 @@ resolveRTele (i:is) (t:ts) = do return ((i,a):as) -- Resolve a declaration -resolveDecl :: Decl -> Resolver ([CTT.Decl],[(Ident,SymKind)]) +resolveDecl :: Decl -> Resolver (CTT.Decls,[(Ident,SymKind)]) resolveDecl d = case d of DeclMutual decls -> do let (fs,ts,bs,nss) = unzip4 $ map resolveNonMutualDecl decls @@ -337,24 +337,30 @@ resolveDecl d = case d of -- mutual block ds <- sequence $ map (local (insertIdents ns)) bs let ads = zipWith (\ (x,y) z -> (x,(y,z))) as ds - return (ads,ns) + return (CTT.MutualDecls ads,ns) + DeclOpaque i -> do + resolveVar i + return (CTT.OpaqueDecl (unAIdent i), []) + DeclVisible i -> do + resolveVar i + return (CTT.VisibleDecl (unAIdent i), []) _ -> do let (f,typ,body,ns) = resolveNonMutualDecl d a <- typ d <- body - return ([(f,(a,d))],ns) + return (CTT.MutualDecls [(f,(a,d))],ns) -resolveDecls :: [Decl] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) +resolveDecls :: [Decl] -> Resolver ([CTT.Decls],[(Ident,SymKind)]) resolveDecls [] = return ([],[]) resolveDecls (d:ds) = do (rtd,names) <- resolveDecl d (rds,names') <- local (insertIdents names) $ resolveDecls ds return (rtd : rds, names' ++ names) -resolveModule :: Module -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) +resolveModule :: Module -> Resolver ([CTT.Decls],[(Ident,SymKind)]) resolveModule (Module (AIdent (_,n)) _ decls) = local (updateModule n) $ resolveDecls decls -resolveModules :: [Module] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) +resolveModules :: [Module] -> Resolver ([CTT.Decls],[(Ident,SymKind)]) resolveModules [] = return ([],[]) resolveModules (mod:mods) = do (rmod, names) <- resolveModule mod diff --git a/TypeChecker.hs b/TypeChecker.hs index 3b22d2c..918e443 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -42,12 +42,12 @@ trace s = do runTyping :: TEnv -> Typing a -> IO (Either String a) runTyping env t = runExceptT $ runReaderT t env -runDecls :: TEnv -> [Decl] -> IO (Either String TEnv) +runDecls :: TEnv -> Decls -> IO (Either String TEnv) runDecls tenv d = runTyping tenv $ do checkDecls d return $ addDecls d tenv -runDeclss :: TEnv -> [[Decl]] -> IO (Maybe String,TEnv) +runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv) runDeclss tenv [] = return (Nothing, tenv) runDeclss tenv (d:ds) = do x <- runDecls tenv d @@ -79,7 +79,7 @@ addBranch :: [(Ident,Val)] -> Env -> TEnv -> TEnv addBranch nvs env (TEnv ns ind rho v) = TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds nvs rho) v -addDecls :: [Decl] -> TEnv -> TEnv +addDecls :: Decls -> TEnv -> TEnv addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v addTele :: Tele -> TEnv -> TEnv @@ -184,6 +184,7 @@ check a t = case (a,t) of ++ "\ndomain of Pi: " ++ show a ++ "\nnormal form of type: " ++ show (normal ns a) let var = mkVarNice ns x a + local (addTypeVal (x,a)) $ check (app f var) t (VSigma a f, Pair t1 t2) -> do check a t1 @@ -220,15 +221,19 @@ check a t = case (a,t) of throwError $ "check conv:\n" ++ show v ++ "\n/=\n" ++ show a -- Check a list of declarations -checkDecls :: [Decl] -> Typing () -checkDecls d = do +checkDecls :: Decls -> Typing () +checkDecls (MutualDecls []) = return () +checkDecls (MutualDecls d) = do + a <- asks env let (idents,tele,ters) = (declIdents d,declTele d,declTers d) ind <- asks indent trace (replicate ind ' ' ++ "Checking: " ++ unwords idents) checkTele tele - local (addDecls d) $ do + local (addDecls (MutualDecls d)) $ do rho <- asks env checks (tele,rho) ters +checkDecls (OpaqueDecl _) = return () +checkDecls (VisibleDecl _) = return () -- Check a telescope checkTele :: Tele -> Typing () @@ -416,8 +421,8 @@ checks _ _ = -- infer the type of e infer :: Ter -> Typing Val infer e = case e of - U -> return VU -- U : U - Var n -> lookType n <$> asks env + U -> return VU -- U : U + Var n -> lookType n <$> asks env App t u -> do c <- infer t case c of diff --git a/cubicaltt.el b/cubicaltt.el index 2b9bab3..c45a39f 100644 --- a/cubicaltt.el +++ b/cubicaltt.el @@ -1,6 +1,6 @@ ;; define several class of keywords (setq ctt-keywords '("hdata" "data" "import" "mutual" "let" "in" "split" - "module" "where" "U") ) + "module" "where" "U" "opaque" "visible") ) (setq ctt-special '("undefined" "primitive")) ;; create regex strings diff --git a/examples/torsor.ctt b/examples/torsor.ctt index f552523..24a5c53 100644 --- a/examples/torsor.ctt +++ b/examples/torsor.ctt @@ -5,9 +5,6 @@ import circle import helix import univalence --- Only ZBZ.ZEquiv is not proven --- Some proofs are replaced by undefined to speed up typechecking - -- isEquivComp (A B C : U) (F : A -> B) (G : B -> C) (ef : isEquiv A B F) (eg : isEquiv B C G) @@ -18,8 +15,18 @@ isEquivComp (A B C : U) (F : A -> B) (G : B -> C) (ef : isEquiv A B F) (eg : isE (\(x : A) -> compId A ((ef (eg (G (F x))).1.1).1.1) (ef (F x)).1.1 x ( (ef (secEq B C (G, eg) (F x) @ i)).1.1) (secEq A B (F, ef) x)) +isEquivComp' (A B C : U) (F : A -> B) (G : C -> B) (ef : isEquiv A B F) (eg : isEquiv C B G) + : isEquiv A C (\(x : A) -> (eg (F x)).1.1) + = gradLemma A C (\(x : A) -> (eg (F x)).1.1) (\(x : C) -> (ef (G x)).1.1) + (\(x : C) -> compId C (eg (F (ef (G x)).1.1)).1.1 (eg (G x)).1.1 x + ( (eg (retEq A B (F, ef) (G x) @ i)).1.1) (secEq C B (G, eg) x)) + (\(x : A) -> compId A ((ef (G (eg (F x)).1.1)).1.1) (ef (F x)).1.1 x + ( (ef (retEq C B (G, eg) (F x) @ i)).1.1) (secEq A B (F, ef) x)) + + lemHcomp (x : loopS1) : Id loopS1 ( comp (<_>S1) (x@i) [(i=0)-><_>base,(i=1)-><_>base]) x = comp (<_>S1) (x@i) [(i=0)-><_>base,(j=1)-><_>x@i,(i=1)-><_>base] +opaque lemHcomp lemHcomp3 (x : loopS1) : Id loopS1 @@ -35,6 +42,7 @@ lemHcomp3 (x : loopS1) x ( comp (<_>S1) (lemHcomp x@j@i) [(i=0)-><_>base,(i=1)-><_>base]) (lemHcomp x)) +opaque lemHcomp3 lemEquiv1 (A B : U) (F : A -> B) (G : A -> B) (e : isEquiv A B G) (p : (x : A) -> Id A (e (F x)).1.1 x) : Id (A -> B) F G = \(x : A) -> transport ( Id B (retEq A B (G, e) (F x) @ i) (G x)) (mapOnPath A B G (e (F x)).1.1 x (p x)) @ i @@ -104,7 +112,6 @@ lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y ) (mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p) - lem11 (A : U) : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) = hole where hole0 : Id (equiv A A) @@ -121,6 +128,7 @@ lem11 (A : U) : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 = lem10' (Id U A A) (equiv A A) (corrUniv' A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) (compId (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A) (transEquiv' A A (<_> A)) hole1 hole0) +opaque lem11 substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y = transport ( IdP p x (q@i)) hole @@ -323,8 +331,11 @@ F23 (A B : U) (F : A -> B) (p2 : P2 A B F) (x : B) (a b : (y : A) * Id B x (F y) hole3 E12 (A B : U) (F : A -> B) : Id U (P1 A B F) (P2 A B F) = isoIdProp (P1 A B F) (P2 A B F) (propP1 A B F) (propP2 A B F) (F12 A B F) (F21 A B F) +opaque E12 E23 (A B : U) (F : A -> B) : Id U (P2 A B F) (P3 A B F) = isoIdProp (P2 A B F) (P3 A B F) (propP2 A B F) (propP3 A B F) (F23 A B F) (F32 A B F) +opaque E23 E13 (A B : U) (F : A -> B) : Id U (P1 A B F) (P3 A B F) = compId U (P1 A B F) (P2 A B F) (P3 A B F) (E12 A B F) (E23 A B F) +opaque E13 -- torsor @@ -342,16 +353,13 @@ actionEquiv (A : U) (shift : equiv A A) : (y : Z) -> isEquiv A A (\(x : A) -> ac inl n -> hole n where hole : (n : nat) -> isEquiv A A (\(x : A) -> action A shift x (inl n)) = split zero -> hole0 - where hole0 : isEquiv A A (\(x : A) -> action A shift x (inl zero)) = undefined - suc n -> hole0 - where hole0 : isEquiv A A (\(x : A) -> (shift.2 (action A shift x (inl n))).1.1) = undefined + where hole0 : isEquiv A A (\(x : A) -> (shift.2 x).1.1) = isEquivComp' A A A (\(x : A) -> x) shift.1 (isEquivId A) shift.2 + suc n -> isEquivComp' A A A (\(x : A) -> action A shift x (inl n)) shift.1 (hole n) shift.2 inr n -> hole n where hole : (n : nat) -> isEquiv A A (\(x : A) -> action A shift x (inr n)) = split zero -> isEquivId A suc n -> isEquivComp A A A (\(x : A) -> action A shift x (inr n)) shift.1 (hole n) shift.2 -plop : nat = U - BZ : U = (A : U) * (ASet : set A) * (a : ishinh_UU A) * (AShift : equiv A A) * ((x : A) -> isEquiv Z A (action A AShift x)) @@ -384,8 +392,10 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p pS : IdP ( p@i -> p@i) (BZS BA) (BZS BB) = w.2 pASet : IdP ( set (p@i)) ASet BSet = lemIdPProp (set A) (set B) (setIsProp A) ( set (p@i)) ASet BSet + opaque pASet pNE : IdP ( ishinh_UU (p@i)) a b = lemIdPProp (ishinh_UU A) (ishinh_UU B) (propishinh A) ( ishinh_UU (p@i)) a b + opaque pNE pShift : IdP ( equiv (p@i) (p@i)) AShift BShift = ( pS @ i , (lemIdPProp @@ -403,6 +413,7 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p (\(x : A) -> propIsEquiv Z A (action A AShift x))) ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x)) AEquiv BEquiv + opaque pEquiv hole : Id BZ BA BB = (p@i, (pASet@i, (pNE@i, (pShift@i, pEquiv@i)))) G (q : Id BZ BA BB) : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB) = ( BZSet (q @ i), (BZShift (q@i)).1) GF (w : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) @@ -415,8 +426,10 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p q2 : Id BZ BA BB = F (p, p2) pASet : Id (IdP ( set (p@i)) ASet BSet) ( BZASet (q2@i)) ( BZASet (q@i)) = lemIdPSet (set A) (set B) (propSet (set A) (setIsProp A)) ( set (p@i)) ASet BSet ( BZASet (q2@i)) ( BZASet (q@i)) + opaque pASet pNE : Id (IdP ( ishinh_UU (p@i)) a b) ( BZNE (q2@i)) ( BZNE (q@i)) = lemIdPSet (ishinh_UU A) (ishinh_UU B) (propSet (ishinh_UU A) (propishinh A)) ( ishinh_UU (p@i)) a b ( BZNE (q2@i)) ( BZNE (q@i)) + opaque pNE pShift : Id (IdP ( equiv (p@i) (p@i)) AShift BShift) ( BZShift (q2@i)) ( BZShift (q@i)) = ( p2 @ i , (lemIdPSet @@ -427,6 +440,7 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p AShift.2 BShift.2 ( (BZShift (q2@i)).2) ( (BZShift (q@i)).2)) @ j @ i ) + opaque pShift pEquiv : IdP ( IdP ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x)) AEquiv BEquiv) ( BZEquiv (q2@i)) ( BZEquiv (q@i)) = lemIdPSet2 ((x : A) -> isEquiv Z A (action A AShift x)) @@ -438,6 +452,7 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@1@i) x)) ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x)) AEquiv BEquiv ( BZEquiv (q2@i)) ( BZEquiv (q@i)) + opaque pEquiv hole : Id (Id BZ BA BB) q2 q = (p@i, (pASet@j@i, (pNE@j@i, (pShift@j@i, pEquiv@j@i)))) hole : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) = (F, gradLemma ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) F G FG GF) @@ -466,66 +481,56 @@ lem2' (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Id A (shift.2 (action A s zero -> <_> action A shift a (inl zero) suc n -> secEq A A shift (action A shift a (inr n)) --- negZ : Z -> Z = split --- inl u -> inr (suc u) --- inr u -> hole u --- where --- hole : nat -> Z = split --- zero -> inr zero --- suc n -> inl n - --- negNegZ : (x : Z) -> Id Z (negZ (negZ x)) x = split --- inl u -> <_> inl u --- inr u -> hole u --- where --- hole : (n : nat) -> Id Z (negZ (negZ (inr n))) (inr n) = split --- zero -> <_> inr zero --- suc n -> <_> inr (suc n) - ZBZ : BZ = (Z, (ZSet, (hinhpr Z zeroZ, (ZShift, ZEquiv)))) where ZShift : equiv Z Z = (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) plus : Z -> Z -> Z = action Z ZShift - -- plusCommZero : (y : Z) -> Id Z (plus zeroZ y) (plus y zeroZ) = undefined - -- plusComm : (x y : Z) -> Id Z (plus x y) (plus y x) = undefined - -- plusNeg : (x : Z) -> Id Z (plus (negZ x) x) zeroZ = split - -- inl u -> hole u - -- where - -- hole : (n : nat) -> Id Z (plus (inr (suc n)) (inl n)) zeroZ = split - -- zero -> <_> zeroZ - -- suc n -> compId Z (predZ (plus (inr (suc (suc n))) (inl n))) (predZ (sucZ (plus (inl n) (inr (suc n))))) zeroZ - -- ( predZ (plusComm (inr (suc (suc n))) (inl n) @ i)) - -- (compId Z (predZ (sucZ (plus (inl n) (inr (suc n))))) (predZ (sucZ (plus (inr (suc n)) (inl n)))) zeroZ - -- ( predZ (sucZ (plusComm (inr (suc n)) (inl n) @ -i))) - -- ( predZ (sucZ (hole n @ i)))) - -- inr u -> hole u - -- where - -- hole : (n : nat) -> Id Z (plus (negZ (inr n)) (inr n)) zeroZ = split - -- zero -> <_> zeroZ - -- suc n -> hole2 - -- where - -- hole2 : Id Z (plus (inl n) (inr (suc n))) zeroZ = undefined - -- plusAssoc (x y : Z) : (z : Z) -> Id Z (plus (plus x y) z) (plus x (plus y z)) = split - -- inl u -> hole u - -- where - -- hole : (n : nat) -> Id Z (plus (plus x y) (inl n)) (plus x (plus y (inl n))) = split - -- zero -> lem2' Z ZShift x y - -- suc n -> compId Z (predZ (plus (plus x y) (inl n))) (predZ (plus x (plus y (inl n)))) (plus x (predZ (plus y (inl n)))) - -- ( predZ (plusAssoc x y (inl n) @ i)) (lem2' Z ZShift x (plus y (inl n))) - -- inr u -> hole u - -- where - -- hole : (n : nat) -> Id Z (plus (plus x y) (inr n)) (plus x (plus y (inr n))) = split - -- zero -> <_> plus x y - -- suc n -> hole3 - -- where hole3 : Id Z (sucZ (plus (plus x y) (inr n))) (plus x (sucZ (plus y (inr n)))) - -- = compId Z (sucZ (plus (plus x y) (inr n))) (sucZ (plus x (plus y (inr n)))) (plus x (sucZ (plus y (inr n)))) - -- ( sucZ (plusAssoc x y (inr n) @ i)) (lem2 Z ZShift x (plus y (inr n))) - ZEquiv (x : Z) : isEquiv Z Z (plus x) = undefined - -- where - -- G : Z -> Z = plus (negZ x) - -- FG (a : Z) : Id Z (plus x (plus (negZ x) a)) a = undefined - -- GF (a : Z) : Id Z (plus (negZ x) (plus x a)) a = undefined - -- hole : isEquiv Z Z (plus x) = undefined + plusCommZero : (y : Z) -> Id Z (plus zeroZ y) (plus y zeroZ) = split + inl u -> hole u + where hole : (n : nat) -> Id Z (plus zeroZ (inl n)) (inl n) = split + zero -> <_> inl zero + suc n -> predZ (hole n @ i) + inr u -> hole u + where hole : (n : nat) -> Id Z (plus zeroZ (inr n)) (inr n) = split + zero -> <_> inr zero + suc n -> sucZ (plusCommZero (inr n) @ i) + plusCommSuc (x : Z) : (y : Z) -> Id Z (plus (sucZ x) y) (plus x (sucZ y)) = split + inl u -> hole u + where hole : (n : nat) -> Id Z (plus (sucZ x) (inl n)) (plus x (sucZ (inl n))) = split + zero -> predsucZ x + suc n -> hole0 n + where hole0 : (n : nat) -> Id Z (predZ (plus (sucZ x) (inl n))) (plus x (sucZ (predZ (inl n)))) = split + zero -> predZ (predsucZ x @ i) + suc n -> compId Z (predZ (predZ (plus (sucZ x) (inl n)))) + (predZ (plus x (inl n))) (predZ (plus x (sucZ (predZ (inl n))))) + ( predZ (hole0 n @ i)) ( predZ (plus x (sucpredZ (inl n) @ -i))) + inr u -> hole u + where hole : (n : nat) -> Id Z (plus (sucZ x) (inr n)) (plus x (inr (suc n))) = split + zero -> <_> sucZ x + suc n -> sucZ (hole n @ i) + plusCommPred (x y : Z) : Id Z (plus (predZ x) y) (plus x (predZ y)) + = transport ( Id Z (plus (predZ x) (sucpredZ y @ i)) (plus (sucpredZ x @ i) (predZ y))) + ( plusCommSuc (predZ x) (predZ y) @ -i) + plusComm (x : Z) : (y : Z) -> Id Z (plus y x) (plus x y) = split + inl u -> hole u + where hole : (n : nat) -> Id Z (plus (inl n) x) (plus x (inl n)) = split + zero -> compId Z (plus (inl zero) x) (plus (inr zero) (predZ x)) (predZ x) + (plusCommPred (inr zero) x) (plusCommZero (predZ x)) + suc n -> compId Z (plus (inl (suc n)) x) (plus (inl n) (predZ x)) (predZ (plus x (inl n))) + (plusCommPred (inl n) x) + (compId Z (plus (inl n) (predZ x)) (predZ (plus (inl n) x)) (predZ (plus x (inl n))) + ( lem2' Z ZShift (inl n) x @ -i) + ( predZ (hole n @ i))) + inr u -> hole u + where hole : (n : nat) -> Id Z (plus (inr n) x) (plus x (inr n)) = split + zero -> plusCommZero x + suc n -> compId Z (plus (inr (suc n)) x) (plus (inr n) (sucZ x)) (sucZ (plus x (inr n))) + (plusCommSuc (inr n) x) + (compId Z (plus (inr n) (sucZ x)) (sucZ (plus (inr n) x)) (sucZ (plus x (inr n))) + ( lem2 Z ZShift (inr n) x @ -i) + ( sucZ (hole n @ i))) + ZEquiv (x : Z) : isEquiv Z Z (plus x) + = transport ( isEquiv Z Z (\(y : Z) -> plusComm x y @ i)) (actionEquiv Z ZShift x) loopBZ : U = Id BZ ZBZ ZBZ compBZ : loopBZ -> loopBZ -> loopBZ = compId BZ ZBZ ZBZ ZBZ @@ -575,54 +580,57 @@ invLoopZ : loopBZ = loopZ @ -i encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport ( BZSet (p@i)) zeroZ -decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 ( p @ -i, q @ -i) +decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 ( p @ -i, q) where p1 : isEquiv Z (BZSet A) (BZAction A a) = BZEquiv A a p : Id U (BZSet A) Z = (univalence (BZSet A) Z (BZAction A a, p1)).1.1 @ -i - -- hole1 (x : Z) : Id Z (transport p (BZS A (transport ( p @ -i) x))) - -- (p1 (BZS A (BZAction A a x))).1.1 - -- = compId Z (transport p (BZS A (transport ( p @ -i) x))) - -- (transport p (BZS A (BZAction A a x))) - -- (p1 (BZS A (BZAction A a x))).1.1 - -- ( transport p (BZS A (lem0 Z (BZSet A) (BZAction A a) p1 x @ i))) - -- (lem1 Z (BZSet A) (BZAction A a) p1 (BZS A (BZAction A a x))) - -- hole2 (x : Z) : Id Z (p1 (BZS A (BZAction A a x))).1.1 (sucZ x) - -- = compId Z (p1 (BZS A (BZAction A a x))).1.1 (p1 (BZAction A a (sucZ x))).1.1 (sucZ x) - -- ( (p1 (lem2 (BZSet A) (BZShift A) a x @ i)).1.1) - -- (secEq Z (BZSet A) (BZAction A a, p1) (sucZ x)) - -- hole : Id (Z->Z) (\(x : Z) -> transport p (BZS A (transport ( p @ -i) x))) sucZ - -- = \(x : Z) -> compId Z (transport p (BZS A (transport ( p @ -i) x))) (p1 (BZS A (BZAction A a x))).1.1 (sucZ x) - -- (hole1 x) (hole2 x) @ i - q : IdP ( (p@i) -> (p@i)) (BZS A) sucZ - = undefined - -- = substIdP (BZSet A -> BZSet A) (Z -> Z) ( (p@i) -> (p@i)) (BZS A) sucZ hole - -prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = undefined --- hole --- where --- hole0 : (x : Z) -> Id Z (BZAction ZBZ zeroZ x) x = split --- inl n -> hole1 n --- where --- hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inl n)) (inl n) = split --- zero -> <_> inl zero --- suc n -> mapOnPath Z Z predZ (BZAction ZBZ zeroZ (inl n)) (inl n) (hole1 n) --- inr n -> hole1 n --- where --- hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inr n)) (inr n) = split --- zero -> <_> inr zero --- suc n -> mapOnPath Z Z sucZ (BZAction ZBZ zeroZ (inr n)) (inr n) (hole1 n) --- hole : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) --- = (\(x : Z) -> hole0 x @ i, --- lemIdPProp --- (isEquiv Z Z (BZAction ZBZ zeroZ)) (isEquiv Z Z (\(x : Z) -> x)) --- (propIsEquiv Z Z (BZAction ZBZ zeroZ)) --- ( isEquiv Z Z (\(x : Z) -> hole0 x @ j)) --- (BZEquiv ZBZ zeroZ) (isEquivId Z) @ i --- ) + hole1 (x : Z) : Id Z (transport p (BZS A (transport ( p @ -i) x))) + (p1 (BZS A (BZAction A a x))).1.1 + = compId Z (transport p (BZS A (transport ( p @ -i) x))) + (transport p (BZS A (BZAction A a x))) + (p1 (BZS A (BZAction A a x))).1.1 + ( transport p (BZS A (lem0 Z (BZSet A) (BZAction A a) p1 x @ i))) + (lem1 Z (BZSet A) (BZAction A a) p1 (BZS A (BZAction A a x))) + opaque hole1 + hole2 (x : Z) : Id Z (p1 (BZS A (BZAction A a x))).1.1 (sucZ x) + = compId Z (p1 (BZS A (BZAction A a x))).1.1 (p1 (BZAction A a (sucZ x))).1.1 (sucZ x) + ( (p1 (lem2 (BZSet A) (BZShift A) a x @ i)).1.1) + (secEq Z (BZSet A) (BZAction A a, p1) (sucZ x)) + opaque hole2 + hole : Id (Z->Z) (\(x : Z) -> transport p (BZS A (transport ( p @ -i) x))) sucZ + = \(x : Z) -> compId Z (transport p (BZS A (transport ( p @ -i) x))) (p1 (BZS A (BZAction A a x))).1.1 (sucZ x) (hole1 x) (hole2 x) @ i + opaque hole + q : IdP ( (p@-i) -> (p@-i)) sucZ (BZS A) + = substIdP (BZSet A -> BZSet A) (Z -> Z) ( (p@i) -> (p@i)) (BZS A) sucZ hole @ -i + opaque q + +prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = hole + where + hole0 : (x : Z) -> Id Z (BZAction ZBZ zeroZ x) x = split + inl n -> hole1 n + where + hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inl n)) (inl n) = split + zero -> <_> inl zero + suc n -> mapOnPath Z Z predZ (BZAction ZBZ zeroZ (inl n)) (inl n) (hole1 n) + inr n -> hole1 n + where + hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inr n)) (inr n) = split + zero -> <_> inr zero + suc n -> mapOnPath Z Z sucZ (BZAction ZBZ zeroZ (inr n)) (inr n) (hole1 n) + hole : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) + = (\(x : Z) -> hole0 x @ i, + lemIdPProp + (isEquiv Z Z (BZAction ZBZ zeroZ)) (isEquiv Z Z (\(x : Z) -> x)) + (propIsEquiv Z Z (BZAction ZBZ zeroZ)) + ( isEquiv Z Z (\(x : Z) -> hole0 x @ j)) + (BZEquiv ZBZ zeroZ) (isEquivId Z) @ i + ) +opaque prf decodeEncodeZRefl0 : Id (Id U Z Z) (univalence Z Z (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ)).1.1 (<_> Z) = transport ( Id (Id U Z Z) (univalence Z Z (prf @ -i)).1.1 (<_> Z)) (lem11 Z) +opaque decodeEncodeZRefl0 decodeEncodeZRefl1 : IdP ( (IdP ( decodeEncodeZRefl0@j@i -> decodeEncodeZRefl0@j@i) sucZ sucZ)) @@ -632,111 +640,119 @@ decodeEncodeZRefl1 ( decodeEncodeZRefl0@1@j -> decodeEncodeZRefl0@1@j) ( decodeEncodeZRefl0@i@j -> decodeEncodeZRefl0@i@j) sucZ sucZ ( (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ) +opaque decodeEncodeZRefl1 + decodeEncodeZRefl2 : Id ((p : Id U Z Z) * IdP ( p@i -> p@i) sucZ sucZ) ((lemBZ ZBZ ZBZ).2 (decodeZ ZBZ zeroZ)).1.1 ((lemBZ ZBZ ZBZ).2 (<_> ZBZ)).1.1 = (decodeEncodeZRefl0 @ i, decodeEncodeZRefl1 @ i) +opaque decodeEncodeZRefl2 + + +decodeEncodeZRefl : Id loopBZ (decodeZ ZBZ zeroZ) (<_> ZBZ) + = lem10 ((p : Id U Z Z) * IdP ( p@i -> p@i) sucZ sucZ) loopBZ (lemBZ ZBZ ZBZ) (decodeZ ZBZ zeroZ) (<_> ZBZ) decodeEncodeZRefl2 +opaque decodeEncodeZRefl + +decodeEncodeZ : (A : BZ) -> (p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p + = J BZ ZBZ (\(A : BZ) -> \(p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p) decodeEncodeZRefl +opaque decodeEncodeZ +encodeDecodeZ (A : BZ) (p : BZSet A) : Id (BZSet A) (transport (univalence (BZSet A) Z (BZAction A p, BZEquiv A p)).1.1 zeroZ) p + = lem0 Z (BZSet A) (BZAction A p) (BZEquiv A p) zeroZ +opaque encodeDecodeZ --- decodeEncodeZRefl : Id loopBZ (decodeZ ZBZ zeroZ) (<_> ZBZ) --- = lem10 ((p : Id U Z Z) * IdP ( p@i -> p@i) sucZ sucZ) loopBZ (lemBZ ZBZ ZBZ) (decodeZ ZBZ zeroZ) (<_> ZBZ) decodeEncodeZRefl2 - --- decodeEncodeZ : (A : BZ) -> (p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p --- = J BZ ZBZ (\(A : BZ) -> \(p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p) decodeEncodeZRefl --- encodeDecodeZ (A : BZ) (p : BZSet A) : Id (BZSet A) (transport (univalence (BZSet A) Z (BZAction A p, BZEquiv A p)).1.1 zeroZ) p --- = lem0 Z (BZSet A) (BZAction A p) (BZEquiv A p) zeroZ - --- loopBZequalsZ : Id U loopBZ Z = isoId loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ) - --- loopS1equalsLoopBZ : Id U loopS1 loopBZ = compId U loopS1 Z loopBZ loopS1equalsZ ( loopBZequalsZ @ -i) --- loopS1equalsLoopBZ' : equiv loopS1 loopBZ = transEquiv' loopBZ loopS1 loopS1equalsLoopBZ - --- -- BZ = S1 - --- F : S1 -> BZ = split --- base -> ZBZ --- loop @ i -> loopZ @ i - --- -- mapOnPath S1 BZ F base base = loopS1equalsLoopBZ'.1 : same left inverse and loopS1equalsLoopBZ'.1 is an equivalence - --- G : (y : S1) -> Id BZ ZBZ (F y) -> Id S1 base y = split --- base -> \(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1 --- loop @ i -> hole @ i --- where --- hole4 (x : Z) : Id loopS1 (loopIt (predZ x)) (compS1 (loopIt x) invLoop) --- = lem2It x --- hole5 (x : loopBZ) : Id Z (encodeZ ZBZ (compBZ x invLoopZ)) (predZ (encodeZ ZBZ x)) --- = J BZ ZBZ (\(A : BZ) -> \(x : Id BZ ZBZ A) -> Id (BZSet A) (encodeZ A (compId BZ ZBZ A A x ( loopA A @ -i))) (BZP A (encodeZ A x))) --- (<_> inl zero) ZBZ x --- hole3 (x : loopBZ) --- : Id loopS1 --- (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) --- (decode base (encodeZ ZBZ x)) --- = compId loopS1 --- (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) --- (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1) --- (decode base (encodeZ ZBZ x)) --- ( compS1 (decode base (hole5 x @ i)) loop1) --- (compId loopS1 --- (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1) --- (compS1 (compS1 (decode base (encodeZ ZBZ x)) invLoop) loop1) --- (decode base (encodeZ ZBZ x)) --- ( compS1 (hole4 (encodeZ ZBZ x) @ i) loop1) --- ( compInv S1 base base (decode base (encodeZ ZBZ x)) base invLoop @ -i)) --- hole6 (x : loopBZ) : Id loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (decode base (encodeZ ZBZ x)) --- = compId loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))))) (decode base (encodeZ ZBZ x)) --- (lemHcomp3 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero)))))))) --- ( decode base (transConstNRefl Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))) @ i)) --- hole1 : Id (loopBZ -> loopS1) --- (\(x : loopBZ) -> compS1 ((loopS1equalsLoopBZ'.2 (compBZ x invLoopZ)).1.1) loop1) --- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) --- = \(x : loopBZ) -> --- transport ( Id loopS1 (compS1 (hole6 (compBZ x invLoopZ) @ -i) loop1) (loopS1equalsLoopBZ'.2 x).1.1) --- (transport ( Id loopS1 (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) (hole6 x @ -i)) --- (hole3 x)) @ j --- hole : IdP ( Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i)) --- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) --- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) --- = substIdP (loopBZ -> loopS1) (loopBZ -> loopS1) --- ( Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i)) --- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) --- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) --- hole1 - --- GF : (y : S1) -> (x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F base y x)) x --- = J S1 base (\(y : S1) -> \(x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F base y x)) x) --- (lemHcomp3 (<_> base)) - --- -- When F_fullyFaithful.hole0 is uncommented, typechecking F_fullyFaithful.hole is slow (doesn't terminate ?) - --- F_fullyFaithful : (x y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y) --- = lemPropFib (\(x : S1) -> (y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)) --- (\(x : S1) -> propPi S1 (\(y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)) --- (\(y : S1) -> propIsEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))) --- (lemPropFib (\(y : S1) -> isEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y)) --- (\(y : S1) -> propIsEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y)) --- hole) --- where --- hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 --- = undefined --- -- = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base) --- hole : isEquiv loopS1 loopBZ (mapOnPath S1 BZ F base base) --- = transport ( isEquiv loopS1 loopBZ (hole0 @ -i)) loopS1equalsLoopBZ'.2 - --- F_essentiallySurjective (y : BZ) : (x : S1) * Id BZ y (F x) = hole --- where --- hInh (y : BZ) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hole --- where --- hole2 (a : BZSet y) : (x : S1) * Id BZ y (F x) = (base, decodeZ y a @ -i) --- hole1 (a : BZSet y) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hinhpr ((x : S1) * Id BZ y (F x)) (hole2 a) --- hole : ishinh_UU ((x : S1) * Id BZ y (F x)) = BZNE y (ishinh_UU ((x : S1) * Id BZ y (F x)), propishinh ((x : S1) * Id BZ y (F x))) hole1 --- hProp : prop ((x : S1) * Id BZ y (F x)) = transport (E13 S1 BZ F) (F_fullyFaithful) y --- hContr : isContr ((x : S1) * Id BZ y (F x)) = inhPropContr ((x : S1) * Id BZ y (F x)) hProp (hInh y) --- hole : (x : S1) * Id BZ y (F x) = hContr.1 - --- -- Typechecking S1equalsBZ.hole is slow - --- S1equalsBZ : Id U S1 BZ = hole --- where --- G (y : BZ) : S1 = (F_essentiallySurjective y).1 --- FG (y : BZ) : Id BZ (F (G y)) y = (F_essentiallySurjective y).2 @ -i --- GF (x : S1) : Id S1 (G (F x)) x = (F_fullyFaithful (G (F x)) x (FG (F x))).1.1 --- hole : Id U S1 BZ = isoId S1 BZ F G FG GF +loopBZequalsZ : Id U loopBZ Z = isoId loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ) + +loopS1equalsLoopBZ : Id U loopS1 loopBZ = compId U loopS1 Z loopBZ loopS1equalsZ ( loopBZequalsZ @ -i) +loopS1equalsLoopBZ' : equiv loopS1 loopBZ = transEquiv' loopBZ loopS1 loopS1equalsLoopBZ + +-- BZ = S1 + +F : S1 -> BZ = split + base -> ZBZ + loop @ i -> loopZ @ i + +-- mapOnPath S1 BZ F base base = loopS1equalsLoopBZ'.1 : same left inverse and loopS1equalsLoopBZ'.1 is an equivalence + +G : (y : S1) -> Id BZ ZBZ (F y) -> Id S1 base y = split + base -> \(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1 + loop @ i -> hole @ i + where + hole4 (x : Z) : Id loopS1 (loopIt (predZ x)) (compS1 (loopIt x) invLoop) + = lem2It x + hole5 (x : loopBZ) : Id Z (encodeZ ZBZ (compBZ x invLoopZ)) (predZ (encodeZ ZBZ x)) + = J BZ ZBZ (\(A : BZ) -> \(x : Id BZ ZBZ A) -> Id (BZSet A) (encodeZ A (compId BZ ZBZ A A x ( loopA A @ -i))) (BZP A (encodeZ A x))) + (<_> inl zero) ZBZ x + hole3 (x : loopBZ) + : Id loopS1 + (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) + (decode base (encodeZ ZBZ x)) + = compId loopS1 + (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) + (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1) + (decode base (encodeZ ZBZ x)) + ( compS1 (decode base (hole5 x @ i)) loop1) + (compId loopS1 + (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1) + (compS1 (compS1 (decode base (encodeZ ZBZ x)) invLoop) loop1) + (decode base (encodeZ ZBZ x)) + ( compS1 (hole4 (encodeZ ZBZ x) @ i) loop1) + ( compInv S1 base base (decode base (encodeZ ZBZ x)) base invLoop @ -i)) + hole6 (x : loopBZ) : Id loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (decode base (encodeZ ZBZ x)) + = compId loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))))) (decode base (encodeZ ZBZ x)) + (lemHcomp3 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero)))))))) + ( decode base (transConstNRefl Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))) @ i)) + hole1 : Id (loopBZ -> loopS1) + (\(x : loopBZ) -> compS1 ((loopS1equalsLoopBZ'.2 (compBZ x invLoopZ)).1.1) loop1) + (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) + = \(x : loopBZ) -> + transport ( Id loopS1 (compS1 (hole6 (compBZ x invLoopZ) @ -i) loop1) (loopS1equalsLoopBZ'.2 x).1.1) + (transport ( Id loopS1 (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) (hole6 x @ -i)) + (hole3 x)) @ j + hole : IdP ( Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i)) + (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) + (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) + = substIdP (loopBZ -> loopS1) (loopBZ -> loopS1) + ( Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i)) + (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) + (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1) + hole1 + +GF : (y : S1) -> (x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F base y x)) x + = J S1 base (\(y : S1) -> \(x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F base y x)) x) + (lemHcomp3 (<_> base)) +opaque GF + +F_fullyFaithful : (x y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y) + = lemPropFib (\(x : S1) -> (y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)) + (\(x : S1) -> propPi S1 (\(y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)) + (\(y : S1) -> propIsEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))) + (lemPropFib (\(y : S1) -> isEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y)) + (\(y : S1) -> propIsEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y)) + hole) + where + hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 + = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base) + opaque hole0 + hole : isEquiv loopS1 loopBZ (mapOnPath S1 BZ F base base) + = transport ( isEquiv loopS1 loopBZ (hole0 @ -i)) loopS1equalsLoopBZ'.2 + opaque hole +opaque F_fullyFaithful + +F_essentiallySurjective (y : BZ) : (x : S1) * Id BZ y (F x) = hole + where + hInh (y : BZ) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hole + where + hole2 (a : BZSet y) : (x : S1) * Id BZ y (F x) = (base, decodeZ y a @ -i) + hole1 (a : BZSet y) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hinhpr ((x : S1) * Id BZ y (F x)) (hole2 a) + hole : ishinh_UU ((x : S1) * Id BZ y (F x)) = BZNE y (ishinh_UU ((x : S1) * Id BZ y (F x)), propishinh ((x : S1) * Id BZ y (F x))) hole1 + hProp : prop ((x : S1) * Id BZ y (F x)) = transport (E13 S1 BZ F) (F_fullyFaithful) y + hContr : isContr ((x : S1) * Id BZ y (F x)) = inhPropContr ((x : S1) * Id BZ y (F x)) hProp (hInh y) + hole : (x : S1) * Id BZ y (F x) = hContr.1 + +S1equalsBZ : Id U S1 BZ = hole + where + G (y : BZ) : S1 = (F_essentiallySurjective y).1 + FG (y : BZ) : Id BZ (F (G y)) y = (F_essentiallySurjective y).2 @ -i + opaque FG + GF (x : S1) : Id S1 (G (F x)) x = (F_fullyFaithful (G (F x)) x (FG (F x))).1.1 + opaque GF + hole : Id U S1 BZ = isoId S1 BZ F G FG GF \ No newline at end of file diff --git a/examples/torsor0.ctt b/examples/torsor0.ctt deleted file mode 100644 index 0825628..0000000 --- a/examples/torsor0.ctt +++ /dev/null @@ -1,258 +0,0 @@ -module torsor0 where -import prelude -import int -import circle -import helix -import univalence - -lemEquiv1 (A B : U) (F : A -> B) (G : A -> B) (e : isEquiv A B G) (p : (x : A) -> Id A (e (F x)).1.1 x) : Id (A -> B) F G - = \(x : A) -> transport ( Id B (retEq A B (G, e) (F x) @ i) (G x)) (mapOnPath A B G (e (F x)).1.1 x (p x)) @ i - -transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = comp (<_> A) a [(i=1) -> <_>a] -lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p = - comp ( A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> p @ k \/ j ] -lemReflComp' (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a b b p (<_> b)) p = - comp ( A) (p @ i) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <_> b ] - -lem2ItPos : (n:nat) -> Id loopS1 (loopIt (predZ (inr n))) (backTurn (loopIt (inr n))) = split - zero -> transport ( Id loopS1 invLoop (lemReflComp S1 base base invLoop @ -i)) (<_> invLoop) - suc p -> compInv S1 base base (loopIt (inr p)) base loop1 - -lem2It : (n:Z) -> Id loopS1 (loopIt (predZ n)) (backTurn (loopIt n)) = split - inl n -> <_> loopIt (inl (suc n)) - inr n -> lem2ItPos n - -transportCompId (a b c : U) (p1 : Id U a b) (p2 : Id U b c) (x : a) - : Id c (transport (compId U a b c p1 p2) x) (transport p2 (transport p1 x)) - = J U b (\(c : U) -> \(p2 : Id U b c) -> Id c (comp (compId U a b c p1 p2) x []) (comp p2 (transport p1 x) [])) - hole c p2 - where - hole : Id b (comp (compId U a b b p1 (<_> b)) x []) (comp (<_> b) (transport p1 x) []) = - compId b (comp (compId U a b b p1 (<_> b)) x []) (transport p1 x) (comp (<_> b) (transport p1 x) []) - ( comp (lemReflComp' U a b p1 @ i) x []) - ( transRefl b (transport p1 x) @ -i) - -lemRevCompId (A : U) (a b c : A) (p1 : Id A a b) (p2 : Id A b c) - : Id (Id A c a) ( compId A a b c p1 p2 @ -i) (compId A c b a ( p2@-i) ( p1@-i)) - = comp ( A) (hole1 @ i @ j) [(i=0) -> p2 @ k \/ j, (i=1) -> p1 @ -k /\ j] - where - hole1 : Square A b a c b ( p1@-i) ( p2@-i) p2 p1 - = comp ( A) (p1 @ -i \/ j) [(i=0) -> p2 @ j /\ k, (i=1) -> <_> p1@j, (j=0) -> <_> p1@-i, (j=1) -> p2 @ k /\ -i ] - -setPi (A : U) (B : A -> U) (h : (x : A) -> set (B x)) - (f0 f1 : (x : A) -> B x) - (p1 p2 : Id ((x : A) -> B x) f0 f1) - : Id (Id ((x : A) -> B x) f0 f1) p1 p2 - = \(x : A) -> (h x (f0 x) (f1 x) ( (p1@i) x) ( (p2@i) x)) @ i @ j - -lemIdPProp (A B : U) (AProp : prop A) (p : Id U A B) : (x : A) -> (y : B) -> IdP p x y - = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) -> (y : B) -> IdP p x y) AProp B p - -lemIdPSet (A B : U) (ASet : set A) (p : Id U A B) : (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t - = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t) ASet B p - -lemIdPSet2 (A B : U) (ASet : set A) (p1 : Id U A B) - : (p2 : Id U A B) -> (p : Id (Id U A B) p1 p2) -> - (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP ( (IdP (p @ i) x y)) s t - = J (Id U A B) p1 (\(p2 : Id U A B) -> \(p : Id (Id U A B) p1 p2) -> (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP ( (IdP (p @ i) x y)) s t) - (lemIdPSet A B ASet p1) - - -isEquivId (A : U) : isEquiv A A (\(x : A) -> x) = gradLemma A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x) - -lem10 (A B : U) (e : equiv A B) (x y : B) (p : Id A (e.2 x).1.1 (e.2 y).1.1) : Id B x y - = transport - (compId U (Id B (e.1 (e.2 x).1.1) (e.1 (e.2 y).1.1)) (Id B x (e.1 (e.2 y).1.1)) (Id B x y) - ( Id B (retEq A B e x @ i) (e.1 (e.2 y).1.1)) ( Id B x (retEq A B e y @ i))) - (mapOnPath A B e.1 (e.2 x).1.1 (e.2 y).1.1 p) - -lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y - = transport - (compId U (Id A (e.2 (e.1 x)).1.1 (e.2 (e.1 y)).1.1) (Id A x (e.2 (e.1 y)).1.1) (Id A x y) - ( Id A (secEq A B e x @ i) (e.2 (e.1 y)).1.1) ( Id A x (secEq A B e y @ i)) - ) - (mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p) - - -lem11 (A : U) : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) = hole - where - hole0 : Id (equiv A A) - (\(x : A) -> x, isEquivId A) - (transEquiv' A A (<_> A)) - = ( (transRefl (A->A) (\(x : A) -> x) @ -i) - , lemIdPProp (isEquiv A A (\(x : A) -> x)) (isEquiv A A (transEquiv' A A (<_> A)).1) - (propIsEquiv A A (\(x : A) -> x)) ( isEquiv A A (transRefl (A->A) (\(x : A) -> x) @ -j)) - (isEquivId A) (transEquiv' A A (<_> A)).2 @ i - ) - hole1 : Id (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A) - = retEq (Id U A A) (equiv A A) (corrUniv' A A) (\(x : A) -> x, isEquivId A) - hole : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) - = lem10' (Id U A A) (equiv A A) (corrUniv' A A) - (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) - (compId (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A) (transEquiv' A A (<_> A)) hole1 hole0) - -substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y - = transport ( IdP p x (q@i)) hole - where - hole : IdP p x (transport p x) = comp ( p @ (i /\ j)) x [(i=0) -> <_> x] - -lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) : - Id U (Id (Sigma A B) t u) ((p : Id A t.1 u.1) * IdP ( B (p @ i)) t.2 u.2) = - isoId T0 T1 f g s t where - T0 : U = Id (Sigma A B) t u - T1 : U = (p:Id A t.1 u.1) * IdP ( B (p@i)) t.2 u.2 - f (q:T0) : T1 = ( (q@i).1, (q@i).2) - g (z:T1) : T0 = (z.1 @i,z.2 @i) - s (z:T1) : Id T1 (f (g z)) z = refl T1 z - t (q:T0) : Id T0 (g (f q)) q = refl T0 q - -transConstN (A : U) (a : A) : (n : nat) -> A = split - zero -> a - suc n -> transport (<_> A) (transConstN A a n) - -transConstNRefl (A : U) (a : A) : (n : nat) -> Id A (transConstN A a n) a = split - zero -> <_> a - suc n -> compId A (transport (<_> A) (transConstN A a n)) (transConstN A a n) a - (transRefl A (transConstN A a n)) (transConstNRefl A a n) - -lem0 (A B : U) (f : A -> B) (e : isEquiv A B f) (x : A) - : Id B (transport (univalence B A (f, e)).1.1 x) (f x) - = transConstNRefl B (f x) (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))))) - -lem1 (A B : U) (f : A -> B) (e : isEquiv A B f) (x : B) - : Id A (transport ( (univalence B A (f, e)).1.1 @ -i) x) (e x).1.1 - = compId A - (transConstN A (e (transConstN B x (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))).1.1 (suc (suc (suc zero)))) - (transConstN A (e x).1.1 (suc (suc (suc zero)))) - (e x).1.1 - ( transConstN A (e (transConstNRefl B x (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) @ i)).1.1 (suc (suc (suc zero)))) - (transConstNRefl A (e x).1.1 (suc (suc (suc zero)))) - --- truncation - -hProp : U = (X : U) * prop X - -ishinh_UU (X : U) : U = (P : hProp) -> ((X -> P.1) -> P.1) - -propishinh (X : U) : prop (ishinh_UU X) = - propPi hProp (\(P : hProp) -> ((X -> P.1) -> P.1)) rem1 - where - rem1 (P : hProp) : prop ((X -> P.1) -> P.1) = - propPi (X -> P.1) (\(_ : X -> P.1) -> P.1) (\(f : X -> P.1) -> P.2) - -ishinh (X : U) : hProp = (ishinh_UU X,propishinh X) - -hinhpr (X : U) : X -> (ishinh X).1 = - \(x : X) (P : hProp) (f : X -> P.1) -> f x - -inhPropContr (A : U) (x : prop A) (y : ishinh_UU A) : isContr A = y (isContr A, propIsContr A) (\(z : A) -> (z, x z)) - -action (A : U) (shift : equiv A A) (x : A) : Z -> A = split - inl n -> invEq A A shift (actionAux n) - where actionAux : nat -> A = split - zero -> x - suc n -> action A shift x (inl n) - inr n -> actionAux n - where actionAux : nat -> A = split - zero -> x - suc n -> shift.1 (action A shift x (inr n)) - -BZ : U = (A : U) * (ASet : set A) * (a : ishinh_UU A) - * (AShift : equiv A A) - * ((x : A) -> isEquiv Z A (action A AShift x)) - -BZSet (x : BZ) : U = x.1 -BZASet (A : BZ) : set (BZSet A) = A.2.1 -BZNE (A : BZ) : ishinh_UU (BZSet A) = A.2.2.1 -BZShift (A : BZ) : equiv (BZSet A) (BZSet A) = A.2.2.2.1 -BZAction (A : BZ) : BZSet A -> Z -> BZSet A = action (BZSet A) (BZShift A) -BZS (A : BZ) : BZSet A -> BZSet A = (BZShift A).1 -BZP (A : BZ) (a : BZSet A) : BZSet A = ((BZShift A).2 a).1.1 -BZEquiv (A : BZ) : (x : BZSet A) -> isEquiv Z (BZSet A) (BZAction A x) = A.2.2.2.2 - --- Two Z-torsors are equal if their underlying sets are equal in a way compatible with the actions -lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) = hole - where - A : U = BA.1 - ASet : set A = BA.2.1 - a : ishinh_UU A = BA.2.2.1 - AShift : equiv A A = BA.2.2.2.1 - AEquiv : (x : A) -> isEquiv Z A (BZAction BA x) = BA.2.2.2.2 - B : U = BB.1 - BSet : set B = BB.2.1 - b : ishinh_UU B = BB.2.2.1 - BShift : equiv B B = BB.2.2.2.1 - BEquiv : (x : B) -> isEquiv Z B (BZAction BB x) = BB.2.2.2.2 - F (w : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) : Id BZ BA BB = hole - where - p : Id U A B = w.1 - pS : IdP ( p@i -> p@i) (BZS BA) (BZS BB) = w.2 - pASet : IdP ( set (p@i)) ASet BSet = undefined - pNE : IdP ( ishinh_UU (p@i)) a b = undefined - pShift : IdP ( equiv (p@i) (p@i)) AShift BShift = - ( pS @ i - , (lemIdPProp - (isEquiv A A AShift.1) - (isEquiv B B BShift.1) - (propIsEquiv A A AShift.1) - ( isEquiv (p@j) (p@j) (pS@j)) - AShift.2 BShift.2) @ i - ) - pEquiv : IdP ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x)) AEquiv BEquiv = undefined - hole : Id BZ BA BB = (p@i, (pASet@i, (pNE@i, (pShift@i, pEquiv@i)))) - G (q : Id BZ BA BB) : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB) = ( BZSet (q @ i), (BZShift (q@i)).1) - GF (w : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) - : Id ((p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) ( BZSet (F w @ i), (BZShift (F w @ i)).1) w - = <_> w - FG (q : Id BZ BA BB) : Id (Id BZ BA BB) (F ( BZSet (q@i), (BZShift (q@i)).1)) q = undefined - hole : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) - = (F, gradLemma ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) F G FG GF) - -lem2 (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Id A (shift.1 (action A shift a x)) (action A shift a (sucZ x)) = split - inl n -> lem2Aux n - where - lem2Aux : (n : nat) -> Id A (shift.1 (action A shift a (inl n))) (action A shift a (sucZ (inl n))) = split - zero -> retEq A A shift a - suc n -> retEq A A shift (action A shift a (inl n)) - inr n -> lem2Aux n - where - lem2Aux : (n : nat) -> Id A (shift.1 (action A shift a (inr n))) (action A shift a (sucZ (inr n))) = split - zero -> <_> shift.1 a - suc n -> <_> shift.1 (action A shift a (inr (suc n))) - -ZBZ : BZ = (Z, (ZSet, (hinhpr Z zeroZ, (ZShift, ZEquiv)))) - where - ZShift : equiv Z Z = (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) - plus : Z -> Z -> Z = action Z ZShift - ZEquiv (x : Z) : isEquiv Z Z (plus x) = undefined - -loopBZ : U = Id BZ ZBZ ZBZ -compBZ : loopBZ -> loopBZ -> loopBZ = compId BZ ZBZ ZBZ ZBZ - --- loopBZ = Z = loopS1 - -encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport ( BZSet (p@i)) zeroZ - -decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 ( p @ -i, q @ -i) - where - p1 : isEquiv Z (BZSet A) (BZAction A a) = BZEquiv A a - p : Id U (BZSet A) Z = (univalence (BZSet A) Z (BZAction A a, p1)).1.1 @ -i - q : IdP ( (p@i) -> (p@i)) (BZS A) sucZ = undefined - -prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = undefined - -decodeEncodeZRefl0 - : Id (Id U Z Z) (univalence Z Z (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ)).1.1 (<_> Z) - = transport ( Id (Id U Z Z) (univalence Z Z (prf @ -i)).1.1 (<_> Z)) (lem11 Z) - -decodeEncodeZRefl1 - : IdP ( (IdP ( decodeEncodeZRefl0@j@i -> decodeEncodeZRefl0@j@i) sucZ sucZ)) - ( (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ) - = lemIdPSet2 (Z->Z) (Z->Z) (setPi Z (\(_ : Z) -> Z) (\(_ : Z) -> ZSet)) - ( decodeEncodeZRefl0@0@j -> decodeEncodeZRefl0@0@j) - ( decodeEncodeZRefl0@1@j -> decodeEncodeZRefl0@1@j) - ( decodeEncodeZRefl0@i@j -> decodeEncodeZRefl0@i@j) - sucZ sucZ ( (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ) - -decodeEncodeZRefl2 : Id ((p : Id U Z Z) * IdP ( p@i -> p@i) sucZ sucZ) ((lemBZ ZBZ ZBZ).2 (decodeZ ZBZ zeroZ)).1.1 ((lemBZ ZBZ ZBZ).2 (<_> ZBZ)).1.1 - = (decodeEncodeZRefl0 @ i, decodeEncodeZRefl1 @ i)