{- Path Type: Copyright (c) Groupoid Infinity, 2014-2018. HoTT 1.12 Identity types HoTT 1.12.1 Path induction HoTT 2.1 Types are higher groupoids HoTT 2.11 Identity type HoTT 3.11 Contractibility HoTT 6.2 Induction principles and dependent paths. -} module path where import proto_path isConst (A: U) (f: A -> A): U = (x y: A) -> Path A (f x) (f y) exConst (A: U): U = (f: A -> A) * isConst A f mapOnPath (A B: U) (f: A -> B) (a b: A) (p: Path A a b): Path B (f a) (f b) -- = cong A B f a b p = f (p @ i) pullback (A B C:U) (f: A -> C) (g: B -> C): U = (a: A) * (b: B) * ( Path C (f a) (g b)) p_1 (A B C: U) (f: A -> C) (g: B -> C): pullback A B C f g -> A = \(x: pullback A B C f g) -> x.1 p_2 (A B C: U) (f: A -> C) (g: B -> C): pullback A B C f g -> B = \(x: pullback A B C f g) -> x.2.1 p_3 (A B C: U) (f: A -> C) (g: B -> C): (x: pullback A B C f g) -> Path C (f x.1) (g x.2.1) = \(x: pullback A B C f g) -> x.2.2 --subst (A: U) (P: A -> U) (a b: A) (p: Path A a b) (e: P a): P b -- = comp ( P (p @ i)) e [] -- normal form -- = trans (P a) (P b) (mapOnPath A U P a b p) e substInv (A: U) (P: A -> U) (a b: A) (p: Path A a b): P b -> P a = subst A P b a ( p @ -i) transRefl (A: U) (a: A): Path A (transport (<_> A) a) a = comp (<_> A) a [(i=1) -> <_>a] substPathP (A B: U) (p: Path U A B) (x: A) (y: B) (q: Path B (transport p x) y): PathP p x y = transport ( PathP p x (q@i)) ( comp ( p @ (i /\ j)) x [(i=0) -> <_> x]) -- J is formulated in a form of Paulin-Mohring and implemented -- using two facts that singleton are contractible and dependent function transport. JPM (A: U) (a b: A) (P: singl A a -> U) (u: P (eta A a)) (p: Path A a b): P (b,p) = subst (singl A a) T (eta A a) (b,p) (contr A a b p) u where T (z : singl A a) : U = P z data N = Z | S (n: N) -- is-n-Type predicate n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U = split { Z -> Path A a b ; S n -> n_grpd (Path A a b) n } isContr (A: U): U = (x: A) * ((y: A) -> Path A x y) isProp (A: U): U = n_grpd A Z isSet (A: U): U = n_grpd A (S Z) isGroupoid (A: U): U = n_grpd A (S (S Z)) isGrp2 (A: U): U = n_grpd A (S (S (S Z))) isGrp3 (A: U): U = n_grpd A (S (S (S (S Z)))) -- ∞-Groupoid inf_grpd (A: U): U = (carrier: A) * (eq: (a b: A) -> Path A a b) * ((a b: A) -> inf_grpd (Path A a b)) isInfinityGroupoid (A: U): U = inf_grpd A -- n-Types PROP : U = (X:U) * isProp X SET : U = (X:U) * isSet X GROUPOID : U = (X:U) * isGroupoid X INF_GROUPOID : U = (X:U) * isInfinityGroupoid X -- if there's a path from a type then there is a path from every element elemPathP (A B: U) (p: Path U A B) (a: A): (p': Path U A B) * (b: B) * PathP p' a b = comp ( P (p @ i)) (refl U A, a, refl A a) [] where P (X: U): U = (p: Path U A X) * (x: X) * PathP p a x isContrSingl (A:U) (a:A): isContr (singl A a) = ((a,refl A a),\ (z:singl A a) -> contr A a z.1 z.2) singl' (A: U) (a: A): U = (x:A) * Path A x a contr' (A: U) (a b: A) (p: Path A a b): Path (singl' A b) (b,refl A b) (a,p) = (p @ -i, p @ -i\/j) isContrSingl' (A:U) (a:A): isContr (singl' A a) = ((a,refl A a),\ (z:singl' A a) -> contr' A z.1 a z.2) isContrPath (A: U): isContr ((B: U) * Path U A B) = (ctr,ctrpath) where ctr: (B: U) * Path U A B = (A,<_> A) ctrpath (q: (B: U) * Path U A B): Path ((B: U) * Path U A B) ctr q = (q.2 @ i, q.2 @ i/\j) isPathContr (A: U) (cA: isContr A) (x y:A) : isContr (Path A x y) = (p0,q) where a: A = cA.1 f: (x:A) -> Path A a x = cA.2 p0: Path A x y = comp (A) a [(i=0) -> f x,(i=1) -> f y] q (p:Path A x y): Path (Path A x y) p0 p = comp (A) a [(i=0) -> f x, (i=1) -> f y, (j=1) -> f (p@i), (j=0) -> comp (A) a [(k=0) -> a, (i=0) -> f x@k/\l, (i=1) -> f y@k/\l] ] lemFib1 (A:U) (F G : A -> U) (a:A) (fa : F a -> G a) : (x:A) (p : Path A a x) -> (fx : F x -> G x) -> Path U (Path (F a -> G x) (\ (u:F a) -> subst A G a x p (fa u)) (\ (u:F a) -> fx (subst A F a x p u))) (PathP (F (p@i) -> G (p@i)) fa fx) = J A a (\ (x:A) (p : Path A a x) -> (fx : F x -> G x) -> Path U (Path (F a -> G x) (\ (u:F a) -> subst A G a x p (fa u)) (\ (u:F a) -> fx (subst A F a x p u))) (PathP (F (p@i) -> G (p@i)) fa fx)) r where r (ga: F a -> G a) : Path U (Path (F a -> G a) (\ (u:F a) -> transC (G a) (fa u)) (\ (u:F a) -> ga (transC (F a) u))) (Path (F a -> G a) fa ga) = Path (F a -> G a) (\ (u:F a) -> lemTransC (G a) (fa u)@j) (\ (u : F a) -> ga (lemTransC (F a) u@j)) lemFib2 (A:U) (F:A->U) (a b:A) (p:Path A a b) (u:F a) : (c:A) (q:Path A b c) -> Path (F c) (subst A F b c q (subst A F a b p u)) (subst A F a c (composition A a b c p q) u) = J A b (\ (c:A) (q:Path A b c) -> Path (F c) (subst A F b c q (subst A F a b p u)) (subst A F a c (composition A a b c p q) u)) r where x : Path (F b) (subst A F a b p u) (subst A F b b (<_>b) (subst A F a b p u)) = lemTransC (F b) (subst A F a b p u) @ -i y : Path (F b) (subst A F a b p u) (subst A F a b (composition A a b b p (<_>b)) u) = subst A F a b (compPathR A a b p @ i) u r : Path (F b) (subst A F b b (<_>b) (subst A F a b p u)) (subst A F a b (composition A a b b p (<_>b)) u) = comp (Path (F b) (x@i) (y@i)) (<_>subst A F a b p u) [] corFib1 (A: U) (F G: A -> U) (a: A) (fa ga: F a -> G a) (p: Path A a a) (h: (u: F a) -> Path (G a) (subst A G a a p (fa u)) (ga (subst A F a a p u))) : PathP (F (p@i) -> G (p@i)) fa ga = comp (lemFib1 A F G a fa a p ga) (\ (u:F a) -> h u @ i) [] -- not used here lem1 (B:U) (F: B -> U) (y: B) (x: F y) : PathP (U) (PathP (F ((refl B y)@i)) x x) (Path (F y) (transport (F((refl B y)@i)) x) x) = PathP (F ((refl B y)@j\/i)) (comp (F ((refl B y)@j/\i)) x [(j=0)-><_>x]) x