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
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 ]
data Ter = App Ter Ter
| Pi Ter
| Lam Ident Ter Ter
- | Where Ter [Decl]
+ | Where Ter Decls
| Var Ident
| U
-- Sigma types:
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
-- Neutral values:
| VVar Ident Val
+ | VOpaque Ident Val
| VFst Val
| VSnd Val
| VSplit Val Val
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
-- 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
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
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
-- 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
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
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
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]
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 () _ = ()
-- 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
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)
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)
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)
-- 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)
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
(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))
instance Convertible Formula where
conv _ phi psi = dnf phi == dnf psi
+instance Convertible (Nameless a) where
+ conv _ _ _ = True
-------------------------------------------------------------------------------
-- | Normalization
VAppFormula u phi -> VAppFormula (normal ns u) (normal ns phi)
_ -> v
+instance Normal (Nameless a) where
+ normal _ = id
+
instance Normal Ctxt where
normal _ = id
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 ;
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."
# 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
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
-- 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
runTyping :: TEnv -> Typing a -> IO (Either String a)\r
runTyping env t = runExceptT $ runReaderT t env\r
\r
-runDecls :: TEnv -> [Decl] -> IO (Either String TEnv)\r
+runDecls :: TEnv -> Decls -> IO (Either String TEnv)\r
runDecls tenv d = runTyping tenv $ do\r
checkDecls d\r
return $ addDecls d tenv\r
\r
-runDeclss :: TEnv -> [[Decl]] -> IO (Maybe String,TEnv)\r
+runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv)\r
runDeclss tenv [] = return (Nothing, tenv)\r
runDeclss tenv (d:ds) = do\r
x <- runDecls tenv d\r
addBranch nvs env (TEnv ns ind rho v) =\r
TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds nvs rho) v\r
\r
-addDecls :: [Decl] -> TEnv -> TEnv\r
+addDecls :: Decls -> TEnv -> TEnv\r
addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v\r
\r
addTele :: Tele -> TEnv -> TEnv\r
++ "\ndomain of Pi: " ++ show a\r
++ "\nnormal form of type: " ++ show (normal ns a)\r
let var = mkVarNice ns x a\r
+\r
local (addTypeVal (x,a)) $ check (app f var) t\r
(VSigma a f, Pair t1 t2) -> do\r
check a t1\r
throwError $ "check conv:\n" ++ show v ++ "\n/=\n" ++ show a\r
\r
-- Check a list of declarations\r
-checkDecls :: [Decl] -> Typing ()\r
-checkDecls d = do\r
+checkDecls :: Decls -> Typing ()\r
+checkDecls (MutualDecls []) = return ()\r
+checkDecls (MutualDecls d) = do\r
+ a <- asks env\r
let (idents,tele,ters) = (declIdents d,declTele d,declTers d)\r
ind <- asks indent\r
trace (replicate ind ' ' ++ "Checking: " ++ unwords idents)\r
checkTele tele\r
- local (addDecls d) $ do\r
+ local (addDecls (MutualDecls d)) $ do\r
rho <- asks env\r
checks (tele,rho) ters\r
+checkDecls (OpaqueDecl _) = return ()\r
+checkDecls (VisibleDecl _) = return ()\r
\r
-- Check a telescope\r
checkTele :: Tele -> Typing ()\r
-- infer the type of e\r
infer :: Ter -> Typing Val\r
infer e = case e of\r
- U -> return VU -- U : U\r
- Var n -> lookType n <$> asks env\r
+ U -> return VU -- U : U\r
+ Var n -> lookType n <$> asks env\r
App t u -> do\r
c <- infer t\r
case c of\r
;; 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
import helix\r
import univalence\r
\r
--- Only ZBZ.ZEquiv is not proven\r
--- Some proofs are replaced by undefined to speed up typechecking\r
-\r
--\r
\r
isEquivComp (A B C : U) (F : A -> B) (G : B -> C) (ef : isEquiv A B F) (eg : isEquiv B C G)\r
(\(x : A) -> compId A ((ef (eg (G (F x))).1.1).1.1) (ef (F x)).1.1 x\r
(<i> (ef (secEq B C (G, eg) (F x) @ i)).1.1) (secEq A B (F, ef) x))\r
\r
+isEquivComp' (A B C : U) (F : A -> B) (G : C -> B) (ef : isEquiv A B F) (eg : isEquiv C B G)\r
+ : isEquiv A C (\(x : A) -> (eg (F x)).1.1)\r
+ = gradLemma A C (\(x : A) -> (eg (F x)).1.1) (\(x : C) -> (ef (G x)).1.1)\r
+ (\(x : C) -> compId C (eg (F (ef (G x)).1.1)).1.1 (eg (G x)).1.1 x\r
+ (<i> (eg (retEq A B (F, ef) (G x) @ i)).1.1) (secEq C B (G, eg) x))\r
+ (\(x : A) -> compId A ((ef (G (eg (F x)).1.1)).1.1) (ef (F x)).1.1 x\r
+ (<i> (ef (retEq C B (G, eg) (F x) @ i)).1.1) (secEq A B (F, ef) x))\r
+\r
+\r
lemHcomp (x : loopS1) : Id loopS1 (<i> comp (<_>S1) (x@i) [(i=0)-><_>base,(i=1)-><_>base]) x\r
= <j i> comp (<_>S1) (x@i) [(i=0)-><_>base,(j=1)-><_>x@i,(i=1)-><_>base]\r
+opaque lemHcomp\r
\r
lemHcomp3 (x : loopS1)\r
: Id loopS1\r
x\r
(<j i> comp (<_>S1) (lemHcomp x@j@i) [(i=0)-><_>base,(i=1)-><_>base])\r
(lemHcomp x))\r
+opaque lemHcomp3\r
\r
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\r
= <i> \(x : A) -> transport (<i> 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\r
)\r
(mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p)\r
\r
-\r
lem11 (A : U) : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) = hole\r
where\r
hole0 : Id (equiv A A)\r
= lem10' (Id U A A) (equiv A A) (corrUniv' A A)\r
(univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A)\r
(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)\r
+opaque lem11\r
\r
substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y\r
= transport (<i> IdP p x (q@i)) hole\r
hole3\r
\r
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)\r
+opaque E12\r
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)\r
+opaque E23\r
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)\r
+opaque E13\r
\r
-- torsor\r
\r
inl n -> hole n\r
where hole : (n : nat) -> isEquiv A A (\(x : A) -> action A shift x (inl n)) = split\r
zero -> hole0\r
- where hole0 : isEquiv A A (\(x : A) -> action A shift x (inl zero)) = undefined\r
- suc n -> hole0\r
- where hole0 : isEquiv A A (\(x : A) -> (shift.2 (action A shift x (inl n))).1.1) = undefined\r
+ 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\r
+ suc n -> isEquivComp' A A A (\(x : A) -> action A shift x (inl n)) shift.1 (hole n) shift.2\r
inr n -> hole n\r
where hole : (n : nat) -> isEquiv A A (\(x : A) -> action A shift x (inr n)) = split\r
zero -> isEquivId A\r
suc n -> isEquivComp A A A (\(x : A) -> action A shift x (inr n)) shift.1 (hole n) shift.2\r
\r
-plop : nat = U\r
-\r
BZ : U = (A : U) * (ASet : set A) * (a : ishinh_UU A)\r
* (AShift : equiv A A)\r
* ((x : A) -> isEquiv Z A (action A AShift x))\r
pS : IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = w.2\r
pASet : IdP (<i> set (p@i)) ASet BSet\r
= lemIdPProp (set A) (set B) (setIsProp A) (<i> set (p@i)) ASet BSet\r
+ opaque pASet\r
pNE : IdP (<i> ishinh_UU (p@i)) a b\r
= lemIdPProp (ishinh_UU A) (ishinh_UU B) (propishinh A) (<i> ishinh_UU (p@i)) a b\r
+ opaque pNE\r
pShift : IdP (<i> equiv (p@i) (p@i)) AShift BShift =\r
<i> ( pS @ i\r
, (lemIdPProp\r
(\(x : A) -> propIsEquiv Z A (action A AShift x)))\r
(<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x))\r
AEquiv BEquiv\r
+ opaque pEquiv\r
hole : Id BZ BA BB = <i> (p@i, (pASet@i, (pNE@i, (pShift@i, pEquiv@i))))\r
G (q : Id BZ BA BB) : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = (<i> BZSet (q @ i), <i> (BZShift (q@i)).1)\r
GF (w : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB))\r
q2 : Id BZ BA BB = F (p, p2)\r
pASet : Id (IdP (<i> set (p@i)) ASet BSet) (<i> BZASet (q2@i)) (<i> BZASet (q@i))\r
= lemIdPSet (set A) (set B) (propSet (set A) (setIsProp A)) (<i> set (p@i)) ASet BSet (<i> BZASet (q2@i)) (<i> BZASet (q@i))\r
+ opaque pASet\r
pNE : Id (IdP (<i> ishinh_UU (p@i)) a b) (<i> BZNE (q2@i)) (<i> BZNE (q@i))\r
= lemIdPSet (ishinh_UU A) (ishinh_UU B) (propSet (ishinh_UU A) (propishinh A)) (<i> ishinh_UU (p@i)) a b (<i> BZNE (q2@i)) (<i> BZNE (q@i))\r
+ opaque pNE\r
pShift : Id (IdP (<i> equiv (p@i) (p@i)) AShift BShift) (<i> BZShift (q2@i)) (<i> BZShift (q@i)) =\r
<j i> ( p2 @ i\r
, (lemIdPSet\r
AShift.2 BShift.2\r
(<i> (BZShift (q2@i)).2) (<i> (BZShift (q@i)).2)) @ j @ i\r
)\r
+ opaque pShift\r
pEquiv : IdP (<j> IdP (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x)) AEquiv BEquiv) (<i> BZEquiv (q2@i)) (<i> BZEquiv (q@i))\r
= lemIdPSet2\r
((x : A) -> isEquiv Z A (action A AShift x))\r
(<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@1@i) x))\r
(<j i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x))\r
AEquiv BEquiv (<i> BZEquiv (q2@i)) (<i> BZEquiv (q@i))\r
+ opaque pEquiv\r
hole : Id (Id BZ BA BB) q2 q = <j i> (p@i, (pASet@j@i, (pNE@j@i, (pShift@j@i, pEquiv@j@i))))\r
hole : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB)\r
= (F, gradLemma ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) F G FG GF)\r
zero -> <_> action A shift a (inl zero)\r
suc n -> secEq A A shift (action A shift a (inr n))\r
\r
--- negZ : Z -> Z = split\r
--- inl u -> inr (suc u)\r
--- inr u -> hole u\r
--- where\r
--- hole : nat -> Z = split\r
--- zero -> inr zero\r
--- suc n -> inl n\r
-\r
--- negNegZ : (x : Z) -> Id Z (negZ (negZ x)) x = split\r
--- inl u -> <_> inl u\r
--- inr u -> hole u\r
--- where\r
--- hole : (n : nat) -> Id Z (negZ (negZ (inr n))) (inr n) = split\r
--- zero -> <_> inr zero\r
--- suc n -> <_> inr (suc n)\r
-\r
ZBZ : BZ = (Z, (ZSet, (hinhpr Z zeroZ, (ZShift, ZEquiv))))\r
where\r
ZShift : equiv Z Z = (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ)\r
plus : Z -> Z -> Z = action Z ZShift\r
- -- plusCommZero : (y : Z) -> Id Z (plus zeroZ y) (plus y zeroZ) = undefined\r
- -- plusComm : (x y : Z) -> Id Z (plus x y) (plus y x) = undefined\r
- -- plusNeg : (x : Z) -> Id Z (plus (negZ x) x) zeroZ = split\r
- -- inl u -> hole u\r
- -- where\r
- -- hole : (n : nat) -> Id Z (plus (inr (suc n)) (inl n)) zeroZ = split\r
- -- zero -> <_> zeroZ\r
- -- suc n -> compId Z (predZ (plus (inr (suc (suc n))) (inl n))) (predZ (sucZ (plus (inl n) (inr (suc n))))) zeroZ\r
- -- (<i> predZ (plusComm (inr (suc (suc n))) (inl n) @ i))\r
- -- (compId Z (predZ (sucZ (plus (inl n) (inr (suc n))))) (predZ (sucZ (plus (inr (suc n)) (inl n)))) zeroZ\r
- -- (<i> predZ (sucZ (plusComm (inr (suc n)) (inl n) @ -i)))\r
- -- (<i> predZ (sucZ (hole n @ i))))\r
- -- inr u -> hole u\r
- -- where\r
- -- hole : (n : nat) -> Id Z (plus (negZ (inr n)) (inr n)) zeroZ = split\r
- -- zero -> <_> zeroZ\r
- -- suc n -> hole2\r
- -- where\r
- -- hole2 : Id Z (plus (inl n) (inr (suc n))) zeroZ = undefined\r
- -- plusAssoc (x y : Z) : (z : Z) -> Id Z (plus (plus x y) z) (plus x (plus y z)) = split\r
- -- inl u -> hole u\r
- -- where\r
- -- hole : (n : nat) -> Id Z (plus (plus x y) (inl n)) (plus x (plus y (inl n))) = split\r
- -- zero -> lem2' Z ZShift x y\r
- -- 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))))\r
- -- (<i> predZ (plusAssoc x y (inl n) @ i)) (lem2' Z ZShift x (plus y (inl n)))\r
- -- inr u -> hole u\r
- -- where\r
- -- hole : (n : nat) -> Id Z (plus (plus x y) (inr n)) (plus x (plus y (inr n))) = split\r
- -- zero -> <_> plus x y\r
- -- suc n -> hole3\r
- -- where hole3 : Id Z (sucZ (plus (plus x y) (inr n))) (plus x (sucZ (plus y (inr n))))\r
- -- = compId Z (sucZ (plus (plus x y) (inr n))) (sucZ (plus x (plus y (inr n)))) (plus x (sucZ (plus y (inr n))))\r
- -- (<i> sucZ (plusAssoc x y (inr n) @ i)) (lem2 Z ZShift x (plus y (inr n)))\r
- ZEquiv (x : Z) : isEquiv Z Z (plus x) = undefined\r
- -- where\r
- -- G : Z -> Z = plus (negZ x)\r
- -- FG (a : Z) : Id Z (plus x (plus (negZ x) a)) a = undefined\r
- -- GF (a : Z) : Id Z (plus (negZ x) (plus x a)) a = undefined\r
- -- hole : isEquiv Z Z (plus x) = undefined\r
+ plusCommZero : (y : Z) -> Id Z (plus zeroZ y) (plus y zeroZ) = split\r
+ inl u -> hole u\r
+ where hole : (n : nat) -> Id Z (plus zeroZ (inl n)) (inl n) = split\r
+ zero -> <_> inl zero\r
+ suc n -> <i> predZ (hole n @ i)\r
+ inr u -> hole u\r
+ where hole : (n : nat) -> Id Z (plus zeroZ (inr n)) (inr n) = split\r
+ zero -> <_> inr zero\r
+ suc n -> <i> sucZ (plusCommZero (inr n) @ i)\r
+ plusCommSuc (x : Z) : (y : Z) -> Id Z (plus (sucZ x) y) (plus x (sucZ y)) = split\r
+ inl u -> hole u\r
+ where hole : (n : nat) -> Id Z (plus (sucZ x) (inl n)) (plus x (sucZ (inl n))) = split\r
+ zero -> predsucZ x\r
+ suc n -> hole0 n\r
+ where hole0 : (n : nat) -> Id Z (predZ (plus (sucZ x) (inl n))) (plus x (sucZ (predZ (inl n)))) = split\r
+ zero -> <i> predZ (predsucZ x @ i)\r
+ suc n -> compId Z (predZ (predZ (plus (sucZ x) (inl n))))\r
+ (predZ (plus x (inl n))) (predZ (plus x (sucZ (predZ (inl n)))))\r
+ (<i> predZ (hole0 n @ i)) (<i> predZ (plus x (sucpredZ (inl n) @ -i)))\r
+ inr u -> hole u\r
+ where hole : (n : nat) -> Id Z (plus (sucZ x) (inr n)) (plus x (inr (suc n))) = split\r
+ zero -> <_> sucZ x\r
+ suc n -> <i> sucZ (hole n @ i)\r
+ plusCommPred (x y : Z) : Id Z (plus (predZ x) y) (plus x (predZ y))\r
+ = transport (<i> Id Z (plus (predZ x) (sucpredZ y @ i)) (plus (sucpredZ x @ i) (predZ y)))\r
+ (<i> plusCommSuc (predZ x) (predZ y) @ -i)\r
+ plusComm (x : Z) : (y : Z) -> Id Z (plus y x) (plus x y) = split\r
+ inl u -> hole u\r
+ where hole : (n : nat) -> Id Z (plus (inl n) x) (plus x (inl n)) = split\r
+ zero -> compId Z (plus (inl zero) x) (plus (inr zero) (predZ x)) (predZ x)\r
+ (plusCommPred (inr zero) x) (plusCommZero (predZ x))\r
+ suc n -> compId Z (plus (inl (suc n)) x) (plus (inl n) (predZ x)) (predZ (plus x (inl n)))\r
+ (plusCommPred (inl n) x)\r
+ (compId Z (plus (inl n) (predZ x)) (predZ (plus (inl n) x)) (predZ (plus x (inl n)))\r
+ (<i> lem2' Z ZShift (inl n) x @ -i)\r
+ (<i> predZ (hole n @ i)))\r
+ inr u -> hole u\r
+ where hole : (n : nat) -> Id Z (plus (inr n) x) (plus x (inr n)) = split\r
+ zero -> plusCommZero x\r
+ suc n -> compId Z (plus (inr (suc n)) x) (plus (inr n) (sucZ x)) (sucZ (plus x (inr n)))\r
+ (plusCommSuc (inr n) x)\r
+ (compId Z (plus (inr n) (sucZ x)) (sucZ (plus (inr n) x)) (sucZ (plus x (inr n)))\r
+ (<i> lem2 Z ZShift (inr n) x @ -i)\r
+ (<i> sucZ (hole n @ i)))\r
+ ZEquiv (x : Z) : isEquiv Z Z (plus x)\r
+ = transport (<i> isEquiv Z Z (\(y : Z) -> plusComm x y @ i)) (actionEquiv Z ZShift x)\r
\r
loopBZ : U = Id BZ ZBZ ZBZ\r
compBZ : loopBZ -> loopBZ -> loopBZ = compId BZ ZBZ ZBZ ZBZ\r
\r
encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport (<i> BZSet (p@i)) zeroZ\r
\r
-decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> p @ -i, <i> q @ -i)\r
+decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> p @ -i, q)\r
where\r
p1 : isEquiv Z (BZSet A) (BZAction A a) = BZEquiv A a\r
p : Id U (BZSet A) Z = <i> (univalence (BZSet A) Z (BZAction A a, p1)).1.1 @ -i\r
- -- hole1 (x : Z) : Id Z (transport p (BZS A (transport (<i> p @ -i) x)))\r
- -- (p1 (BZS A (BZAction A a x))).1.1\r
- -- = compId Z (transport p (BZS A (transport (<i> p @ -i) x)))\r
- -- (transport p (BZS A (BZAction A a x)))\r
- -- (p1 (BZS A (BZAction A a x))).1.1\r
- -- (<i> transport p (BZS A (lem0 Z (BZSet A) (BZAction A a) p1 x @ i)))\r
- -- (lem1 Z (BZSet A) (BZAction A a) p1 (BZS A (BZAction A a x)))\r
- -- hole2 (x : Z) : Id Z (p1 (BZS A (BZAction A a x))).1.1 (sucZ x)\r
- -- = compId Z (p1 (BZS A (BZAction A a x))).1.1 (p1 (BZAction A a (sucZ x))).1.1 (sucZ x)\r
- -- (<i> (p1 (lem2 (BZSet A) (BZShift A) a x @ i)).1.1)\r
- -- (secEq Z (BZSet A) (BZAction A a, p1) (sucZ x))\r
- -- hole : Id (Z->Z) (\(x : Z) -> transport p (BZS A (transport (<i> p @ -i) x))) sucZ\r
- -- = <i> \(x : Z) -> compId Z (transport p (BZS A (transport (<i> p @ -i) x))) (p1 (BZS A (BZAction A a x))).1.1 (sucZ x)\r
- -- (hole1 x) (hole2 x) @ i\r
- q : IdP (<i> (p@i) -> (p@i)) (BZS A) sucZ\r
- = undefined\r
- -- = substIdP (BZSet A -> BZSet A) (Z -> Z) (<i> (p@i) -> (p@i)) (BZS A) sucZ hole\r
-\r
-prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = undefined\r
--- hole\r
--- where\r
--- hole0 : (x : Z) -> Id Z (BZAction ZBZ zeroZ x) x = split\r
--- inl n -> hole1 n\r
--- where\r
--- hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inl n)) (inl n) = split\r
--- zero -> <_> inl zero\r
--- suc n -> mapOnPath Z Z predZ (BZAction ZBZ zeroZ (inl n)) (inl n) (hole1 n)\r
--- inr n -> hole1 n\r
--- where\r
--- hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inr n)) (inr n) = split\r
--- zero -> <_> inr zero\r
--- suc n -> mapOnPath Z Z sucZ (BZAction ZBZ zeroZ (inr n)) (inr n) (hole1 n)\r
--- hole : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z)\r
--- = <i> (\(x : Z) -> hole0 x @ i,\r
--- lemIdPProp\r
--- (isEquiv Z Z (BZAction ZBZ zeroZ)) (isEquiv Z Z (\(x : Z) -> x))\r
--- (propIsEquiv Z Z (BZAction ZBZ zeroZ))\r
--- (<j> isEquiv Z Z (\(x : Z) -> hole0 x @ j))\r
--- (BZEquiv ZBZ zeroZ) (isEquivId Z) @ i\r
--- )\r
+ hole1 (x : Z) : Id Z (transport p (BZS A (transport (<i> p @ -i) x)))\r
+ (p1 (BZS A (BZAction A a x))).1.1\r
+ = compId Z (transport p (BZS A (transport (<i> p @ -i) x)))\r
+ (transport p (BZS A (BZAction A a x)))\r
+ (p1 (BZS A (BZAction A a x))).1.1\r
+ (<i> transport p (BZS A (lem0 Z (BZSet A) (BZAction A a) p1 x @ i)))\r
+ (lem1 Z (BZSet A) (BZAction A a) p1 (BZS A (BZAction A a x)))\r
+ opaque hole1\r
+ hole2 (x : Z) : Id Z (p1 (BZS A (BZAction A a x))).1.1 (sucZ x)\r
+ = compId Z (p1 (BZS A (BZAction A a x))).1.1 (p1 (BZAction A a (sucZ x))).1.1 (sucZ x)\r
+ (<i> (p1 (lem2 (BZSet A) (BZShift A) a x @ i)).1.1)\r
+ (secEq Z (BZSet A) (BZAction A a, p1) (sucZ x))\r
+ opaque hole2\r
+ hole : Id (Z->Z) (\(x : Z) -> transport p (BZS A (transport (<i> p @ -i) x))) sucZ\r
+ = <i> \(x : Z) -> compId Z (transport p (BZS A (transport (<i> p @ -i) x))) (p1 (BZS A (BZAction A a x))).1.1 (sucZ x) (hole1 x) (hole2 x) @ i\r
+ opaque hole\r
+ q : IdP (<i> (p@-i) -> (p@-i)) sucZ (BZS A)\r
+ = <i> substIdP (BZSet A -> BZSet A) (Z -> Z) (<i> (p@i) -> (p@i)) (BZS A) sucZ hole @ -i\r
+ opaque q\r
+\r
+prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = hole\r
+ where\r
+ hole0 : (x : Z) -> Id Z (BZAction ZBZ zeroZ x) x = split\r
+ inl n -> hole1 n\r
+ where\r
+ hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inl n)) (inl n) = split\r
+ zero -> <_> inl zero\r
+ suc n -> mapOnPath Z Z predZ (BZAction ZBZ zeroZ (inl n)) (inl n) (hole1 n)\r
+ inr n -> hole1 n\r
+ where\r
+ hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inr n)) (inr n) = split\r
+ zero -> <_> inr zero\r
+ suc n -> mapOnPath Z Z sucZ (BZAction ZBZ zeroZ (inr n)) (inr n) (hole1 n)\r
+ hole : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z)\r
+ = <i> (\(x : Z) -> hole0 x @ i,\r
+ lemIdPProp\r
+ (isEquiv Z Z (BZAction ZBZ zeroZ)) (isEquiv Z Z (\(x : Z) -> x))\r
+ (propIsEquiv Z Z (BZAction ZBZ zeroZ))\r
+ (<j> isEquiv Z Z (\(x : Z) -> hole0 x @ j))\r
+ (BZEquiv ZBZ zeroZ) (isEquivId Z) @ i\r
+ )\r
+opaque prf\r
\r
decodeEncodeZRefl0\r
: Id (Id U Z Z) (univalence Z Z (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ)).1.1 (<_> Z)\r
= transport (<i> Id (Id U Z Z) (univalence Z Z (prf @ -i)).1.1 (<_> Z)) (lem11 Z)\r
+opaque decodeEncodeZRefl0\r
\r
decodeEncodeZRefl1\r
: IdP (<j> (IdP (<i> decodeEncodeZRefl0@j@i -> decodeEncodeZRefl0@j@i) sucZ sucZ))\r
(<j> decodeEncodeZRefl0@1@j -> decodeEncodeZRefl0@1@j)\r
(<i j> decodeEncodeZRefl0@i@j -> decodeEncodeZRefl0@i@j)\r
sucZ sucZ (<i> (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ)\r
+opaque decodeEncodeZRefl1\r
+\r
decodeEncodeZRefl2 : Id ((p : Id U Z Z) * IdP (<i> p@i -> p@i) sucZ sucZ) ((lemBZ ZBZ ZBZ).2 (decodeZ ZBZ zeroZ)).1.1 ((lemBZ ZBZ ZBZ).2 (<_> ZBZ)).1.1\r
= <i> (decodeEncodeZRefl0 @ i, decodeEncodeZRefl1 @ i)\r
+opaque decodeEncodeZRefl2\r
+\r
+\r
+decodeEncodeZRefl : Id loopBZ (decodeZ ZBZ zeroZ) (<_> ZBZ)\r
+ = lem10 ((p : Id U Z Z) * IdP (<i> p@i -> p@i) sucZ sucZ) loopBZ (lemBZ ZBZ ZBZ) (decodeZ ZBZ zeroZ) (<_> ZBZ) decodeEncodeZRefl2\r
+opaque decodeEncodeZRefl\r
+\r
+decodeEncodeZ : (A : BZ) -> (p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p\r
+ = J BZ ZBZ (\(A : BZ) -> \(p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p) decodeEncodeZRefl\r
+opaque decodeEncodeZ\r
\r
+encodeDecodeZ (A : BZ) (p : BZSet A) : Id (BZSet A) (transport (univalence (BZSet A) Z (BZAction A p, BZEquiv A p)).1.1 zeroZ) p\r
+ = lem0 Z (BZSet A) (BZAction A p) (BZEquiv A p) zeroZ\r
+opaque encodeDecodeZ\r
\r
--- decodeEncodeZRefl : Id loopBZ (decodeZ ZBZ zeroZ) (<_> ZBZ)\r
--- = lem10 ((p : Id U Z Z) * IdP (<i> p@i -> p@i) sucZ sucZ) loopBZ (lemBZ ZBZ ZBZ) (decodeZ ZBZ zeroZ) (<_> ZBZ) decodeEncodeZRefl2\r
-\r
--- decodeEncodeZ : (A : BZ) -> (p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p\r
--- = J BZ ZBZ (\(A : BZ) -> \(p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p) decodeEncodeZRefl\r
--- encodeDecodeZ (A : BZ) (p : BZSet A) : Id (BZSet A) (transport (univalence (BZSet A) Z (BZAction A p, BZEquiv A p)).1.1 zeroZ) p\r
--- = lem0 Z (BZSet A) (BZAction A p) (BZEquiv A p) zeroZ\r
-\r
--- loopBZequalsZ : Id U loopBZ Z = isoId loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ)\r
-\r
--- loopS1equalsLoopBZ : Id U loopS1 loopBZ = compId U loopS1 Z loopBZ loopS1equalsZ (<i> loopBZequalsZ @ -i)\r
--- loopS1equalsLoopBZ' : equiv loopS1 loopBZ = transEquiv' loopBZ loopS1 loopS1equalsLoopBZ\r
-\r
--- -- BZ = S1\r
-\r
--- F : S1 -> BZ = split\r
--- base -> ZBZ\r
--- loop @ i -> loopZ @ i\r
-\r
--- -- mapOnPath S1 BZ F base base = loopS1equalsLoopBZ'.1 : same left inverse and loopS1equalsLoopBZ'.1 is an equivalence\r
-\r
--- G : (y : S1) -> Id BZ ZBZ (F y) -> Id S1 base y = split\r
--- base -> \(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1\r
--- loop @ i -> hole @ i\r
--- where\r
--- hole4 (x : Z) : Id loopS1 (loopIt (predZ x)) (compS1 (loopIt x) invLoop)\r
--- = lem2It x\r
--- hole5 (x : loopBZ) : Id Z (encodeZ ZBZ (compBZ x invLoopZ)) (predZ (encodeZ ZBZ x))\r
--- = J BZ ZBZ (\(A : BZ) -> \(x : Id BZ ZBZ A) -> Id (BZSet A) (encodeZ A (compId BZ ZBZ A A x (<i> loopA A @ -i))) (BZP A (encodeZ A x)))\r
--- (<_> inl zero) ZBZ x\r
--- hole3 (x : loopBZ)\r
--- : Id loopS1\r
--- (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1)\r
--- (decode base (encodeZ ZBZ x))\r
--- = compId loopS1\r
--- (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1)\r
--- (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1)\r
--- (decode base (encodeZ ZBZ x))\r
--- (<i> compS1 (decode base (hole5 x @ i)) loop1)\r
--- (compId loopS1\r
--- (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1)\r
--- (compS1 (compS1 (decode base (encodeZ ZBZ x)) invLoop) loop1)\r
--- (decode base (encodeZ ZBZ x))\r
--- (<i> compS1 (hole4 (encodeZ ZBZ x) @ i) loop1)\r
--- (<i> compInv S1 base base (decode base (encodeZ ZBZ x)) base invLoop @ -i))\r
--- hole6 (x : loopBZ) : Id loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (decode base (encodeZ ZBZ x))\r
--- = compId loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))))) (decode base (encodeZ ZBZ x))\r
--- (lemHcomp3 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))))))\r
--- (<i> decode base (transConstNRefl Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))) @ i))\r
--- hole1 : Id (loopBZ -> loopS1)\r
--- (\(x : loopBZ) -> compS1 ((loopS1equalsLoopBZ'.2 (compBZ x invLoopZ)).1.1) loop1)\r
--- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
--- = <j> \(x : loopBZ) ->\r
--- transport (<i> Id loopS1 (compS1 (hole6 (compBZ x invLoopZ) @ -i) loop1) (loopS1equalsLoopBZ'.2 x).1.1)\r
--- (transport (<i> Id loopS1 (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) (hole6 x @ -i))\r
--- (hole3 x)) @ j\r
--- hole : IdP (<i> Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i))\r
--- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
--- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
--- = substIdP (loopBZ -> loopS1) (loopBZ -> loopS1)\r
--- (<i> Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i))\r
--- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
--- (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
--- hole1\r
-\r
--- GF : (y : S1) -> (x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F base y x)) x\r
--- = 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)\r
--- (lemHcomp3 (<_> base))\r
-\r
--- -- When F_fullyFaithful.hole0 is uncommented, typechecking F_fullyFaithful.hole is slow (doesn't terminate ?)\r
-\r
--- F_fullyFaithful : (x y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)\r
--- = lemPropFib (\(x : S1) -> (y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))\r
--- (\(x : S1) -> propPi S1 (\(y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))\r
--- (\(y : S1) -> propIsEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)))\r
--- (lemPropFib (\(y : S1) -> isEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y))\r
--- (\(y : S1) -> propIsEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y))\r
--- hole)\r
--- where\r
--- hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1\r
--- = undefined\r
--- -- = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base)\r
--- hole : isEquiv loopS1 loopBZ (mapOnPath S1 BZ F base base)\r
--- = transport (<i> isEquiv loopS1 loopBZ (hole0 @ -i)) loopS1equalsLoopBZ'.2\r
-\r
--- F_essentiallySurjective (y : BZ) : (x : S1) * Id BZ y (F x) = hole\r
--- where\r
--- hInh (y : BZ) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hole\r
--- where\r
--- hole2 (a : BZSet y) : (x : S1) * Id BZ y (F x) = (base, <i> decodeZ y a @ -i)\r
--- hole1 (a : BZSet y) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hinhpr ((x : S1) * Id BZ y (F x)) (hole2 a)\r
--- 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\r
--- hProp : prop ((x : S1) * Id BZ y (F x)) = transport (E13 S1 BZ F) (F_fullyFaithful) y\r
--- hContr : isContr ((x : S1) * Id BZ y (F x)) = inhPropContr ((x : S1) * Id BZ y (F x)) hProp (hInh y)\r
--- hole : (x : S1) * Id BZ y (F x) = hContr.1\r
-\r
--- -- Typechecking S1equalsBZ.hole is slow\r
-\r
--- S1equalsBZ : Id U S1 BZ = hole\r
--- where\r
--- G (y : BZ) : S1 = (F_essentiallySurjective y).1\r
--- FG (y : BZ) : Id BZ (F (G y)) y = <i> (F_essentiallySurjective y).2 @ -i\r
--- GF (x : S1) : Id S1 (G (F x)) x = (F_fullyFaithful (G (F x)) x (FG (F x))).1.1\r
--- hole : Id U S1 BZ = isoId S1 BZ F G FG GF\r
+loopBZequalsZ : Id U loopBZ Z = isoId loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ)\r
+\r
+loopS1equalsLoopBZ : Id U loopS1 loopBZ = compId U loopS1 Z loopBZ loopS1equalsZ (<i> loopBZequalsZ @ -i)\r
+loopS1equalsLoopBZ' : equiv loopS1 loopBZ = transEquiv' loopBZ loopS1 loopS1equalsLoopBZ\r
+\r
+-- BZ = S1\r
+\r
+F : S1 -> BZ = split\r
+ base -> ZBZ\r
+ loop @ i -> loopZ @ i\r
+\r
+-- mapOnPath S1 BZ F base base = loopS1equalsLoopBZ'.1 : same left inverse and loopS1equalsLoopBZ'.1 is an equivalence\r
+\r
+G : (y : S1) -> Id BZ ZBZ (F y) -> Id S1 base y = split\r
+ base -> \(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1\r
+ loop @ i -> hole @ i\r
+ where\r
+ hole4 (x : Z) : Id loopS1 (loopIt (predZ x)) (compS1 (loopIt x) invLoop)\r
+ = lem2It x\r
+ hole5 (x : loopBZ) : Id Z (encodeZ ZBZ (compBZ x invLoopZ)) (predZ (encodeZ ZBZ x))\r
+ = J BZ ZBZ (\(A : BZ) -> \(x : Id BZ ZBZ A) -> Id (BZSet A) (encodeZ A (compId BZ ZBZ A A x (<i> loopA A @ -i))) (BZP A (encodeZ A x)))\r
+ (<_> inl zero) ZBZ x\r
+ hole3 (x : loopBZ)\r
+ : Id loopS1\r
+ (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1)\r
+ (decode base (encodeZ ZBZ x))\r
+ = compId loopS1\r
+ (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1)\r
+ (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1)\r
+ (decode base (encodeZ ZBZ x))\r
+ (<i> compS1 (decode base (hole5 x @ i)) loop1)\r
+ (compId loopS1\r
+ (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1)\r
+ (compS1 (compS1 (decode base (encodeZ ZBZ x)) invLoop) loop1)\r
+ (decode base (encodeZ ZBZ x))\r
+ (<i> compS1 (hole4 (encodeZ ZBZ x) @ i) loop1)\r
+ (<i> compInv S1 base base (decode base (encodeZ ZBZ x)) base invLoop @ -i))\r
+ hole6 (x : loopBZ) : Id loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (decode base (encodeZ ZBZ x))\r
+ = compId loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))))) (decode base (encodeZ ZBZ x))\r
+ (lemHcomp3 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))))))\r
+ (<i> decode base (transConstNRefl Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))) @ i))\r
+ hole1 : Id (loopBZ -> loopS1)\r
+ (\(x : loopBZ) -> compS1 ((loopS1equalsLoopBZ'.2 (compBZ x invLoopZ)).1.1) loop1)\r
+ (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ = <j> \(x : loopBZ) ->\r
+ transport (<i> Id loopS1 (compS1 (hole6 (compBZ x invLoopZ) @ -i) loop1) (loopS1equalsLoopBZ'.2 x).1.1)\r
+ (transport (<i> Id loopS1 (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) (hole6 x @ -i))\r
+ (hole3 x)) @ j\r
+ hole : IdP (<i> Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i))\r
+ (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ = substIdP (loopBZ -> loopS1) (loopBZ -> loopS1)\r
+ (<i> Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i))\r
+ (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ hole1\r
+\r
+GF : (y : S1) -> (x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F base y x)) x\r
+ = 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)\r
+ (lemHcomp3 (<_> base))\r
+opaque GF\r
+\r
+F_fullyFaithful : (x y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)\r
+ = lemPropFib (\(x : S1) -> (y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))\r
+ (\(x : S1) -> propPi S1 (\(y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))\r
+ (\(y : S1) -> propIsEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)))\r
+ (lemPropFib (\(y : S1) -> isEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y))\r
+ (\(y : S1) -> propIsEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y))\r
+ hole)\r
+ where\r
+ hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1\r
+ = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base)\r
+ opaque hole0\r
+ hole : isEquiv loopS1 loopBZ (mapOnPath S1 BZ F base base)\r
+ = transport (<i> isEquiv loopS1 loopBZ (hole0 @ -i)) loopS1equalsLoopBZ'.2\r
+ opaque hole\r
+opaque F_fullyFaithful\r
+\r
+F_essentiallySurjective (y : BZ) : (x : S1) * Id BZ y (F x) = hole\r
+ where\r
+ hInh (y : BZ) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hole\r
+ where\r
+ hole2 (a : BZSet y) : (x : S1) * Id BZ y (F x) = (base, <i> decodeZ y a @ -i)\r
+ hole1 (a : BZSet y) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hinhpr ((x : S1) * Id BZ y (F x)) (hole2 a)\r
+ 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\r
+ hProp : prop ((x : S1) * Id BZ y (F x)) = transport (E13 S1 BZ F) (F_fullyFaithful) y\r
+ hContr : isContr ((x : S1) * Id BZ y (F x)) = inhPropContr ((x : S1) * Id BZ y (F x)) hProp (hInh y)\r
+ hole : (x : S1) * Id BZ y (F x) = hContr.1\r
+\r
+S1equalsBZ : Id U S1 BZ = hole\r
+ where\r
+ G (y : BZ) : S1 = (F_essentiallySurjective y).1\r
+ FG (y : BZ) : Id BZ (F (G y)) y = <i> (F_essentiallySurjective y).2 @ -i\r
+ opaque FG\r
+ GF (x : S1) : Id S1 (G (F x)) x = (F_fullyFaithful (G (F x)) x (FG (F x))).1.1\r
+ opaque GF\r
+ hole : Id U S1 BZ = isoId S1 BZ F G FG GF
\ No newline at end of file
+++ /dev/null
-module torsor0 where\r
-import prelude\r
-import int\r
-import circle\r
-import helix\r
-import univalence\r
-\r
-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\r
- = <i> \(x : A) -> transport (<i> 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\r
-\r
-transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = <i> comp (<_> A) a [(i=1) -> <_>a]\r
-lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p =\r
- <j i> comp (<k> A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <k> p @ k \/ j ]\r
-lemReflComp' (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a b b p (<_> b)) p =\r
- <j i> comp (<k> A) (p @ i) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <_> b ]\r
-\r
-lem2ItPos : (n:nat) -> Id loopS1 (loopIt (predZ (inr n))) (backTurn (loopIt (inr n))) = split\r
- zero -> transport (<i> Id loopS1 invLoop (lemReflComp S1 base base invLoop @ -i)) (<_> invLoop)\r
- suc p -> compInv S1 base base (loopIt (inr p)) base loop1\r
-\r
-lem2It : (n:Z) -> Id loopS1 (loopIt (predZ n)) (backTurn (loopIt n)) = split\r
- inl n -> <_> loopIt (inl (suc n))\r
- inr n -> lem2ItPos n\r
-\r
-transportCompId (a b c : U) (p1 : Id U a b) (p2 : Id U b c) (x : a)\r
- : Id c (transport (compId U a b c p1 p2) x) (transport p2 (transport p1 x))\r
- = 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) []))\r
- hole c p2\r
- where\r
- hole : Id b (comp (compId U a b b p1 (<_> b)) x []) (comp (<_> b) (transport p1 x) []) =\r
- compId b (comp (compId U a b b p1 (<_> b)) x []) (transport p1 x) (comp (<_> b) (transport p1 x) [])\r
- (<i> comp (lemReflComp' U a b p1 @ i) x [])\r
- (<i> transRefl b (transport p1 x) @ -i)\r
-\r
-lemRevCompId (A : U) (a b c : A) (p1 : Id A a b) (p2 : Id A b c)\r
- : Id (Id A c a) (<i> compId A a b c p1 p2 @ -i) (compId A c b a (<i> p2@-i) (<i> p1@-i))\r
- = <j i> comp (<k> A) (hole1 @ i @ j) [(i=0) -> <k> p2 @ k \/ j, (i=1) -> <k> p1 @ -k /\ j]\r
- where\r
- hole1 : Square A b a c b (<i> p1@-i) (<i> p2@-i) p2 p1\r
- = <i j> comp (<k> A) (p1 @ -i \/ j) [(i=0) -> <k> p2 @ j /\ k, (i=1) -> <_> p1@j, (j=0) -> <_> p1@-i, (j=1) -> <k> p2 @ k /\ -i ]\r
-\r
-setPi (A : U) (B : A -> U) (h : (x : A) -> set (B x))\r
- (f0 f1 : (x : A) -> B x)\r
- (p1 p2 : Id ((x : A) -> B x) f0 f1)\r
- : Id (Id ((x : A) -> B x) f0 f1) p1 p2\r
- = <i j> \(x : A) -> (h x (f0 x) (f1 x) (<i> (p1@i) x) (<i> (p2@i) x)) @ i @ j\r
-\r
-lemIdPProp (A B : U) (AProp : prop A) (p : Id U A B) : (x : A) -> (y : B) -> IdP p x y\r
- = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) -> (y : B) -> IdP p x y) AProp B p\r
-\r
-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\r
- = 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\r
-\r
-lemIdPSet2 (A B : U) (ASet : set A) (p1 : Id U A B)\r
- : (p2 : Id U A B) -> (p : Id (Id U A B) p1 p2) ->\r
- (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP (<i> (IdP (p @ i) x y)) s t\r
- = 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 (<i> (IdP (p @ i) x y)) s t)\r
- (lemIdPSet A B ASet p1)\r
-\r
-\r
-isEquivId (A : U) : isEquiv A A (\(x : A) -> x) = gradLemma A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x)\r
-\r
-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\r
- = transport\r
- (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)\r
- (<i> Id B (retEq A B e x @ i) (e.1 (e.2 y).1.1)) (<i> Id B x (retEq A B e y @ i)))\r
- (mapOnPath A B e.1 (e.2 x).1.1 (e.2 y).1.1 p)\r
-\r
-lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y\r
- = transport\r
- (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)\r
- (<i> Id A (secEq A B e x @ i) (e.2 (e.1 y)).1.1) (<i> Id A x (secEq A B e y @ i))\r
- )\r
- (mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p)\r
-\r
-\r
-lem11 (A : U) : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) = hole\r
- where\r
- hole0 : Id (equiv A A)\r
- (\(x : A) -> x, isEquivId A)\r
- (transEquiv' A A (<_> A))\r
- = <i> ( (transRefl (A->A) (\(x : A) -> x) @ -i)\r
- , lemIdPProp (isEquiv A A (\(x : A) -> x)) (isEquiv A A (transEquiv' A A (<_> A)).1)\r
- (propIsEquiv A A (\(x : A) -> x)) (<j> isEquiv A A (transRefl (A->A) (\(x : A) -> x) @ -j))\r
- (isEquivId A) (transEquiv' A A (<_> A)).2 @ i\r
- )\r
- hole1 : Id (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A)\r
- = retEq (Id U A A) (equiv A A) (corrUniv' A A) (\(x : A) -> x, isEquivId A)\r
- hole : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A)\r
- = lem10' (Id U A A) (equiv A A) (corrUniv' A A)\r
- (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A)\r
- (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)\r
-\r
-substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y\r
- = transport (<i> IdP p x (q@i)) hole\r
- where\r
- hole : IdP p x (transport p x) = <i> comp (<j> p @ (i /\ j)) x [(i=0) -> <_> x]\r
-\r
-lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) :\r
- Id U (Id (Sigma A B) t u) ((p : Id A t.1 u.1) * IdP (<i> B (p @ i)) t.2 u.2) =\r
- isoId T0 T1 f g s t where\r
- T0 : U = Id (Sigma A B) t u\r
- T1 : U = (p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2\r
- f (q:T0) : T1 = (<i> (q@i).1,<i> (q@i).2)\r
- g (z:T1) : T0 = <i>(z.1 @i,z.2 @i)\r
- s (z:T1) : Id T1 (f (g z)) z = refl T1 z\r
- t (q:T0) : Id T0 (g (f q)) q = refl T0 q\r
-\r
-transConstN (A : U) (a : A) : (n : nat) -> A = split\r
- zero -> a\r
- suc n -> transport (<_> A) (transConstN A a n)\r
-\r
-transConstNRefl (A : U) (a : A) : (n : nat) -> Id A (transConstN A a n) a = split\r
- zero -> <_> a\r
- suc n -> compId A (transport (<_> A) (transConstN A a n)) (transConstN A a n) a\r
- (transRefl A (transConstN A a n)) (transConstNRefl A a n)\r
-\r
-lem0 (A B : U) (f : A -> B) (e : isEquiv A B f) (x : A)\r
- : Id B (transport (univalence B A (f, e)).1.1 x) (f x)\r
- = transConstNRefl B (f x) (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))\r
-\r
-lem1 (A B : U) (f : A -> B) (e : isEquiv A B f) (x : B)\r
- : Id A (transport (<i> (univalence B A (f, e)).1.1 @ -i) x) (e x).1.1\r
- = compId A\r
- (transConstN A (e (transConstN B x (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))).1.1 (suc (suc (suc zero))))\r
- (transConstN A (e x).1.1 (suc (suc (suc zero))))\r
- (e x).1.1\r
- (<i> transConstN A (e (transConstNRefl B x (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) @ i)).1.1 (suc (suc (suc zero))))\r
- (transConstNRefl A (e x).1.1 (suc (suc (suc zero))))\r
-\r
--- truncation\r
-\r
-hProp : U = (X : U) * prop X\r
-\r
-ishinh_UU (X : U) : U = (P : hProp) -> ((X -> P.1) -> P.1)\r
-\r
-propishinh (X : U) : prop (ishinh_UU X) =\r
- propPi hProp (\(P : hProp) -> ((X -> P.1) -> P.1)) rem1\r
- where\r
- rem1 (P : hProp) : prop ((X -> P.1) -> P.1) =\r
- propPi (X -> P.1) (\(_ : X -> P.1) -> P.1) (\(f : X -> P.1) -> P.2)\r
-\r
-ishinh (X : U) : hProp = (ishinh_UU X,propishinh X)\r
-\r
-hinhpr (X : U) : X -> (ishinh X).1 =\r
- \(x : X) (P : hProp) (f : X -> P.1) -> f x\r
-\r
-inhPropContr (A : U) (x : prop A) (y : ishinh_UU A) : isContr A = y (isContr A, propIsContr A) (\(z : A) -> (z, x z))\r
-\r
-action (A : U) (shift : equiv A A) (x : A) : Z -> A = split\r
- inl n -> invEq A A shift (actionAux n)\r
- where actionAux : nat -> A = split\r
- zero -> x\r
- suc n -> action A shift x (inl n)\r
- inr n -> actionAux n\r
- where actionAux : nat -> A = split\r
- zero -> x\r
- suc n -> shift.1 (action A shift x (inr n))\r
-\r
-BZ : U = (A : U) * (ASet : set A) * (a : ishinh_UU A)\r
- * (AShift : equiv A A)\r
- * ((x : A) -> isEquiv Z A (action A AShift x))\r
-\r
-BZSet (x : BZ) : U = x.1\r
-BZASet (A : BZ) : set (BZSet A) = A.2.1\r
-BZNE (A : BZ) : ishinh_UU (BZSet A) = A.2.2.1\r
-BZShift (A : BZ) : equiv (BZSet A) (BZSet A) = A.2.2.2.1\r
-BZAction (A : BZ) : BZSet A -> Z -> BZSet A = action (BZSet A) (BZShift A)\r
-BZS (A : BZ) : BZSet A -> BZSet A = (BZShift A).1\r
-BZP (A : BZ) (a : BZSet A) : BZSet A = ((BZShift A).2 a).1.1\r
-BZEquiv (A : BZ) : (x : BZSet A) -> isEquiv Z (BZSet A) (BZAction A x) = A.2.2.2.2\r
-\r
--- Two Z-torsors are equal if their underlying sets are equal in a way compatible with the actions\r
-lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) = hole\r
- where\r
- A : U = BA.1\r
- ASet : set A = BA.2.1\r
- a : ishinh_UU A = BA.2.2.1\r
- AShift : equiv A A = BA.2.2.2.1\r
- AEquiv : (x : A) -> isEquiv Z A (BZAction BA x) = BA.2.2.2.2\r
- B : U = BB.1\r
- BSet : set B = BB.2.1\r
- b : ishinh_UU B = BB.2.2.1\r
- BShift : equiv B B = BB.2.2.2.1\r
- BEquiv : (x : B) -> isEquiv Z B (BZAction BB x) = BB.2.2.2.2\r
- F (w : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) : Id BZ BA BB = hole\r
- where\r
- p : Id U A B = w.1\r
- pS : IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = w.2\r
- pASet : IdP (<i> set (p@i)) ASet BSet = undefined\r
- pNE : IdP (<i> ishinh_UU (p@i)) a b = undefined\r
- pShift : IdP (<i> equiv (p@i) (p@i)) AShift BShift =\r
- <i> ( pS @ i\r
- , (lemIdPProp\r
- (isEquiv A A AShift.1)\r
- (isEquiv B B BShift.1)\r
- (propIsEquiv A A AShift.1)\r
- (<j> isEquiv (p@j) (p@j) (pS@j))\r
- AShift.2 BShift.2) @ i\r
- )\r
- pEquiv : IdP (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x)) AEquiv BEquiv = undefined\r
- hole : Id BZ BA BB = <i> (p@i, (pASet@i, (pNE@i, (pShift@i, pEquiv@i))))\r
- G (q : Id BZ BA BB) : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = (<i> BZSet (q @ i), <i> (BZShift (q@i)).1)\r
- GF (w : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB))\r
- : Id ((p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (<i> BZSet (F w @ i), <i> (BZShift (F w @ i)).1) w\r
- = <_> w\r
- FG (q : Id BZ BA BB) : Id (Id BZ BA BB) (F (<i> BZSet (q@i), <i> (BZShift (q@i)).1)) q = undefined\r
- hole : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB)\r
- = (F, gradLemma ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) F G FG GF)\r
-\r
-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\r
- inl n -> lem2Aux n\r
- where\r
- lem2Aux : (n : nat) -> Id A (shift.1 (action A shift a (inl n))) (action A shift a (sucZ (inl n))) = split\r
- zero -> retEq A A shift a\r
- suc n -> retEq A A shift (action A shift a (inl n))\r
- inr n -> lem2Aux n\r
- where\r
- lem2Aux : (n : nat) -> Id A (shift.1 (action A shift a (inr n))) (action A shift a (sucZ (inr n))) = split\r
- zero -> <_> shift.1 a\r
- suc n -> <_> shift.1 (action A shift a (inr (suc n)))\r
-\r
-ZBZ : BZ = (Z, (ZSet, (hinhpr Z zeroZ, (ZShift, ZEquiv))))\r
- where\r
- ZShift : equiv Z Z = (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ)\r
- plus : Z -> Z -> Z = action Z ZShift\r
- ZEquiv (x : Z) : isEquiv Z Z (plus x) = undefined\r
-\r
-loopBZ : U = Id BZ ZBZ ZBZ\r
-compBZ : loopBZ -> loopBZ -> loopBZ = compId BZ ZBZ ZBZ ZBZ\r
-\r
--- loopBZ = Z = loopS1\r
-\r
-encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport (<i> BZSet (p@i)) zeroZ\r
-\r
-decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> p @ -i, <i> q @ -i)\r
- where\r
- p1 : isEquiv Z (BZSet A) (BZAction A a) = BZEquiv A a\r
- p : Id U (BZSet A) Z = <i> (univalence (BZSet A) Z (BZAction A a, p1)).1.1 @ -i\r
- q : IdP (<i> (p@i) -> (p@i)) (BZS A) sucZ = undefined\r
-\r
-prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = undefined\r
-\r
-decodeEncodeZRefl0\r
- : Id (Id U Z Z) (univalence Z Z (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ)).1.1 (<_> Z)\r
- = transport (<i> Id (Id U Z Z) (univalence Z Z (prf @ -i)).1.1 (<_> Z)) (lem11 Z)\r
-\r
-decodeEncodeZRefl1\r
- : IdP (<j> (IdP (<i> decodeEncodeZRefl0@j@i -> decodeEncodeZRefl0@j@i) sucZ sucZ))\r
- (<i> (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ)\r
- = lemIdPSet2 (Z->Z) (Z->Z) (setPi Z (\(_ : Z) -> Z) (\(_ : Z) -> ZSet))\r
- (<j> decodeEncodeZRefl0@0@j -> decodeEncodeZRefl0@0@j)\r
- (<j> decodeEncodeZRefl0@1@j -> decodeEncodeZRefl0@1@j)\r
- (<i j> decodeEncodeZRefl0@i@j -> decodeEncodeZRefl0@i@j)\r
- sucZ sucZ (<i> (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ)\r
-\r
-decodeEncodeZRefl2 : Id ((p : Id U Z Z) * IdP (<i> p@i -> p@i) sucZ sucZ) ((lemBZ ZBZ ZBZ).2 (decodeZ ZBZ zeroZ)).1.1 ((lemBZ ZBZ ZBZ).2 (<_> ZBZ)).1.1\r
- = <i> (decodeEncodeZRefl0 @ i, decodeEncodeZRefl1 @ i)\r
projects / cubicaltt.git / commitdiff