+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Eval where
import Data.List
(VPi{},_) -> VTrans (VPath i v0) v1
(Ter (Sum _ _ nass) env,VCon n us) -> case lookup n nass of
Just as -> VCon n $ transps i as env us
- Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
+ Nothing -> error $ "comp: missing constructor in labelled sum " ++ n ++ " v0 = " ++ show v0
_ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1
(VGlue a ts,_) -> transGlue i a ts v1
_ | otherwise -> error "trans not implemented"
(u,VTrans p v) | isIndep k j (p @@ j) -> conv k u v
(VTrans p u,VTrans p' u') -> conv k p p' && conv k u u'
(VAppFormula u x,VAppFormula u' x') -> conv k (u,x) (u',x')
- -- VComp
+ (VComp a u ts,v) | isIndep k j (Map.map (@@ j) ts) -> conv k u v
+ (VComp a u ts,v') | not (Map.null indep) -> conv k (VComp a u ts') v'
+ where (ts',indep) = Map.partition (\t -> isIndep k j (t @@ j)) ts
+ (v,VComp a u ts) | isIndep k j (Map.map (@@ j) ts) -> conv k u v
+ (v',VComp a u ts) | not (Map.null indep) -> conv k (VComp a u ts') v'
+ where (ts',indep) = Map.partition (\t -> isIndep k j (t @@ j)) ts
+ (VComp a u ts,VComp a' u' ts') -> conv k (a,u,ts) (a',u',ts')
+ (VGlue v hisos,VGlue v' hisos') -> conv k (v,hisos) (v',hisos')
+ (VGlueElem u us,VGlueElem u' us') -> conv k (u,us) (u',us')
_ -> False
instance Convertible Env where
- conv k e e' =
- conv k (valAndFormulaOfEnv e) (valAndFormulaOfEnv e')
+ conv k e e' = conv k (valAndFormulaOfEnv e) (valAndFormulaOfEnv e')
-instance Convertible () where conv _ _ _ = True
+instance Convertible () where
+ conv _ _ _ = True
instance (Convertible a, Convertible b) => Convertible (a, b) where
conv k (u, v) (u', v') = conv k u u' && conv k v v'
conv k us us' = length us == length us' &&
and [conv k u u' | (u,u') <- zip us us']
+instance Convertible a => Convertible (System a) where
+ conv k ts ts' = Map.keys ts == Map.keys ts' &&
+ and (Map.elems (Map.intersectionWith (conv k) ts ts'))
+
instance Convertible Formula where
conv _ phi psi = sort (invFormula phi 1) == sort (invFormula psi 1)
IdP. Exp3 ::= "IdP" ;
Trans. Exp3 ::= "transport" ;
Comp. Exp3 ::= "comp" ;
+Glue. Exp3 ::= "glue" ;
+GlueElem. Exp3 ::= "glueElem" ;
System. Exp3 ::= "[" [Side] "]" ;
Pair. Exp3 ::= "(" Exp "," Exp ")" ;
coercions Exp 3 ;
import Control.Monad.Trans.Reader
import Control.Monad.Trans.Error hiding (throwError)
import Control.Monad.Error (throwError)
-import Control.Monad (when)
+import Control.Monad
import Data.Functor.Identity
import Data.List (nub)
import Data.Map (Map,(!))
resolveApps Comp (u:v:ts:xs) = do
let c = CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
CTT.mkApps <$> c <*> mapM resolveExp xs
+resolveApps Glue (u:ts:xs) = do
+ rs <- resolveSystem ts
+ let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True
+ isIso _ = False
+ unless (all isIso $ Map.elems rs)
+ (throwError $ "Not a system of isomorphisms: " ++ show rs)
+ let c = CTT.Glue <$> resolveExp u <*> pure rs
+ CTT.mkApps <$> c <*> mapM resolveExp xs
+resolveApps GlueElem (u:ts:xs) = do
+ let c = CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
+ CTT.mkApps <$> c <*> mapM resolveExp xs
resolveApps x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs
resolveExp :: Exp -> Resolver Ter
lams tele (resolveExp t)
Fst t -> CTT.Fst <$> resolveExp t
Snd t -> CTT.Snd <$> resolveExp t
- Pair t0 t1 -> CTT.SPair <$> resolveExp t0 <*> resolveExp t1
+ Pair t0 t1 -> CTT.Pair <$> resolveExp t0 <*> resolveExp t1
Let decls e -> do
(rdecls,names) <- resolveDecls decls
CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e)
let u0 = eval (Sub rho (i,Dir 0)) e\r
u1 = eval (Sub rho (i,Dir 1)) e\r
unless (conv k a0 u0 && conv k a1 u1) $\r
- throwError $ "path endpoints don't match " ++ show e ++ " \nu0 = " ++ show u0 ++ " \nu1 = " ++ show u1 ++ " \na0 = " ++ show a0 ++ " \na1 = " ++ show a1 ++ " \np = " ++ show p\r
+ throwError $ "path endpoints don't match " ++ show e ++\r
+ " \nu0 = " ++ show u0 ++ " \nu1 = " ++ show u1 ++\r
+ " \na0 = " ++ show a0 ++ " \na1 = " ++ show a1 ++\r
+ " \np = " ++ show p\r
+ (VU,Glue a ts) -> do\r
+ check VU a\r
+ rho <- asks env\r
+ checkGlue (eval rho a) ts\r
+ (VGlue va ts,GlueElem u us) -> do\r
+ check va u\r
+ rho <- asks env\r
+ let vu = eval rho u\r
+ checkGlueElem vu ts us\r
_ -> do\r
v <- infer t\r
k <- index <$> ask\r
unless (conv k v a) $\r
throwError $ "check conv: " ++ show v ++ " /= " ++ show a\r
\r
+checkGlueElem :: Val -> System Val -> System Ter -> Typing ()\r
+checkGlueElem vu ts us = do\r
+ unless (Map.keys ts == Map.keys us)\r
+ (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us))\r
+ rho <- asks env\r
+ k <- asks index\r
+ sequence_ $ Map.elems $ Map.intersectionWithKey\r
+ (\alpha vt u -> check (hisoDom vt) u) ts us\r
+ \r
+ let vus = evalSystem rho us\r
+ sequence_ $ Map.elems $ Map.intersectionWithKey\r
+ (\alpha vt vAlpha -> do\r
+ unless (conv k (app (hisoFun vt) vAlpha) (vu `face` alpha))\r
+ (throwError $ "Image of glueElem component " ++ show vAlpha ++\r
+ " doesn't match " ++ show vu)) ts vus\r
+ unless (isCompSystem k vus)\r
+ (throwError $ "Incompatible system " ++ show vus)\r
+\r
+checkGlue :: Val -> System Ter -> Typing ()\r
+checkGlue va ts = do\r
+ sequence_ $ Map.elems $\r
+ Map.mapWithKey (\alpha tAlpha -> checkIso (va `face` alpha) tAlpha) ts\r
+ k <- asks index\r
+ rho <- asks env\r
+ unless (isCompSystem k (evalSystem rho ts))\r
+ (throwError ("Incompatible system " ++ show ts))\r
+\r
+-- An hiso for a type a is a five-tuple: (b,f,g,r,s) where\r
+-- b : U\r
+-- f : b -> a\r
+-- g : a -> b\r
+-- s : forall (y : a), f (g y) = y\r
+-- t : forall (x : b), g (f x) = x\r
+checkIso :: Val -> Ter -> Typing ()\r
+checkIso va (Pair b (Pair f (Pair g (Pair s t)))) = do\r
+ check VU b\r
+ rho <- asks env\r
+ let vb = eval rho b\r
+ check (mkFun vb va) f\r
+ check (mkFun va vb) g\r
+ let vf = eval rho f\r
+ vg = eval rho g\r
+ check (mkSection va vb vf vg) s\r
+ check (mkSection vb va vg vf) t\r
+\r
+mkFun :: Val -> Val -> Val\r
+mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b")))\r
+ where rho = Upd (Upd Empty ("a",va)) ("b",vb)\r
+\r
+mkSection :: Val -> Val -> Val -> Val -> Val\r
+mkSection va _ vf vg =\r
+ VPi va (eval rho (Lam "y" a (IdP (Path (Name "_") a) (App f (App g y)) y)))\r
+ where [a,y,f,g] = map Var ["a","y","f","g"]\r
+ rho = Upd (Upd (Upd Empty ("a",va)) ("f",vf)) ("g",vg)\r
+ \r
checkBranch :: (Tele,Env) -> Val -> Branch -> Typing ()\r
checkBranch (xas,nu) f (c,(xs,e)) = do\r
k <- asks index\r
;; create regex strings
(setq cubical-keywords-regexp (regexp-opt cubical-keywords 'words))
-(setq cubical-operators-regexp (regexp-opt '(":" "->" "=" "\\" "|" "\\" "*" "_") t))
+(setq cubical-operators-regexp (regexp-opt '(":" "->" "=" "\\" "|" "\\" "*" "_" "<" ">") t))
(setq cubical-special-regexp (regexp-opt cubical-special 'words))
(setq cubical-def-regexp "^[[:word:]]+")
--- /dev/null
+module bool where
+
+import prelude
+
+data bool = true | false
+
+neg : bool -> bool = split
+ true -> false
+ false -> true
+
+negK : (b : bool) -> Id bool (neg (neg b)) b = split
+ true -> refl bool true
+ false -> refl bool false
+
+negEq : Id U bool bool =
+ <i> glue bool [ (i = 0) -> (bool,(neg,(neg,(negK,negK)))) ]
+
+test : bool = transport negEq true
+
+data F2 = zero | one
+
+f2ToBool : F2 -> bool = split
+ zero -> false
+ one -> true
+
+boolToF2 : bool -> F2 = split
+ false -> zero
+ true -> one
+
+f2ToBoolK : (x : F2) -> Id F2 (boolToF2 (f2ToBool x)) x = split
+ zero -> refl F2 zero
+ one -> refl F2 one
+
+boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split
+ false -> refl bool false
+ true -> refl bool true
+
+boolEqF2 : Id U bool F2 =
+ -- <i> glue F2 [ (i = 0) -> (bool,(boolToF2,(f2ToBool,(f2ToBoolK,boolToF2K))))]
+ isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
+
+negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg
+
+test : IdP boolEqF2 true one = <i> glueElem one [ (i = 0) -> true ]
+test1 : IdP boolEqF2 true one = lemTest bool F2 boolEqF2 true
+
+F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2
+
+negBool : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2
+
nil -> nil
cons x xs -> append A (reverse A xs) (cons x nil)
-Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
-
-refl (A : U) (a : A) : Id A a a = <i> a
-
-mapOnPath (A B : U) (f : A -> B) (a b : A)
- (p : Id A a b) : Id B (f a) (f b) = <i> f (p @ i)
-
-funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
- (p : (x : A) -> Id (B x) (f x) (g x)) :
- Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i
-
idnat : nat -> nat = split
zero -> zero
suc n -> suc (idnat n)
zero -> refl nat zero
suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n)
-subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
- transport (mapOnPath A U P a b p) e
-
-substRefl (A : U) (P : A -> U) (a : A) (e : P a) : Id (P a) (subst A P a a (refl A a) e) e =
- refl (P a) e
-
-singl (A : U) (a : A) : U = (x : A) * Id A a x
-
-contrSingl (A : U) (a b : A) (p : Id A a b) :
- Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i /\ j)
-
-J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
- (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p =
- subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d
- where T (z : singl A a) : U = C (z.1) (z.2)
-
-defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
- Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d
-
test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
(r : Id A b d) : Id A c d =
<i> comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
-inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
-- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
-- (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
--- /dev/null
+module prelude where
+
+Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
+
+refl (A : U) (a : A) : Id A a a = <i> a
+
+mapOnPath (A B : U) (f : A -> B) (a b : A)
+ (p : Id A a b) : Id B (f a) (f b) = <i> f (p @ i)
+
+funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
+ (p : (x : A) -> Id (B x) (f x) (g x)) :
+ Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i
+
+
+subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
+ transport (mapOnPath A U P a b p) e
+
+substRefl (A : U) (P : A -> U) (a : A) (e : P a) :
+ Id (P a) (subst A P a a (refl A a) e) e = refl (P a) e
+
+singl (A : U) (a : A) : U = (x : A) * Id A a x
+
+contrSingl (A : U) (a b : A) (p : Id A a b) :
+ Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i /\ j)
+
+J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
+ (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p =
+ subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d
+ where T (z : singl A a) : U = C (z.1) (z.2)
+
+defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
+ Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d
+
+inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
+
+isoId (A B : U) (f : A -> B) (g : B -> A)
+ (s : (y:B) -> Id B (f (g y)) y)
+ (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
+ <i> glue B [ (i = 0) -> (A,(f,(g,(s,t)))) ]
+
+lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) =
+ J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) rem
+ where rem (a : A) : Id A a a = refl A a
\ No newline at end of file
projects / cubicaltt.git / commitdiff