{- Path Type: - Reflexivity, Symmetry, Composition, Kan; - Connections; - Congruence and Respect; - Contractability of Singletons; - Substitution, Transport, J. 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. Copyright (c) Groupoid Infinity, 2014-2018. -} module path where -- Path type and its eliminators Path (A: U) (a b: A): U = PathP ( A) a b HPath (A B: U) (a: A) (b: B) (P: Path U A B) : U = PathP P a b refl (A: U) (a: A): Path A a a = a singl (A: U) (a: A): U = (x: A) * Path A a x eta (A: U) (a: A): singl A a = (a,refl A a) contr (A: U) (a b: A) (p: Path A a b): Path (singl A a) (eta A a) (b,p) = (p @ i, p @ i/\j) sym (A: U) (a b: A) (p: Path A a b): Path A b a = p @ -i cong (A B: U) (f: A->B) (a b: A) (p: Path A a b): Path B (f a) (f b) = f (p @ i) ap (A: U) (a x:A) (B:A->U) (f: A->B a) (b: B a) (p: Path A a x): Path (B a) (f a) (f x) = f (p @ i) trans (A B: U) (p: Path U A B) (a : A): B = transport p a -- comp p a [] subst (A: U) (P: A->U) (a b: A) (p: Path A a b) (e: P a): P b = comp ( P (p @ i)) e [] inv (A: U) (a b: A) (p: Path A a b): Path A b a = p @ -i coerce (A B: U) (p: Path U A B): A -> B = \ (x: A) -> trans A B p x -- Path induction from HoTT J (A: U) (a: A) (C: (x : A) -> Path A a x -> U) (d: C a (refl A a)) (x: A) (p: Path A a x): C x p -- = comp ( C (p @ i) ( p @ i /\ j)) d [] -- normal form = subst (singl A a) T (eta A a) (x, p) (contr A a x p) d where T (z : singl A a) : U = C (z.1) (z.2) -- Computational Rules trans_comp (A : U) (a : A) : Path A a (trans A A (<_> A) a) = fill (<_> A) a [] subst_comp (A : U) (P : A -> U) (a : A) (e : P a): Path (P a) e (subst A P a a (refl A a) e) = trans_comp (P a) e J_comp (A : U) (a : A) (C : (x : A) -> Path A a x -> U) (d : C a (refl A a)) : Path (C a (refl A a)) d (J A a C d a (refl A a)) = subst_comp (singl A a) T (a, refl A a) d where T (z : singl A a) : U = C (z.1) (z.2) symJ (A: U) (a b: A) (p: Path A a b): Path A b a = J A a T (refl A a) b p where T (x: A) (_: Path A a x): U = Path A x a transJ (A: U) (a b c: A) (p: Path A a b) (q: Path A b c): Path A a c = undefined composeUniv (A B C: U) (p: Path U A B) (q: Path U B C): Path U A C = comp ( Path U A (q @ i)) p [] -- composition operation composition (A: U) (a b c: A) (p: Path A a b) (q: Path A b c): Path A a c = comp ( Path A a (q @ i)) p [] -- = subst A (Path A a) b c q p -- = comp (A) (p @ i) [(i=0) -> a, (i=1) -> q ] compositionInv (A: U) (a b c: A) (p: Path A a b) (q: Path A b c): Path A c a = inv A a c (composition A a b c p q) join (A: U) (a b: A) (p: Path A a b) : PathP ( Path A (p @ x) b) p (<_> b) = p @ (x \/ y) meet (A: U) (a b: A) (p: Path A a b) : PathP ( Path A a (p @ x)) (<_> a) p = p @ (x /\ y) app0 (A: U) (a b: A) (p: Path A a b): A = p @ 0 app1 (A: U) (a b: A) (p: Path A a b): A = p @ 1 -- Kan filling operation kan (A: U) (a b c d: A) (p: Path A a b) (q: Path A a c) (r: Path A b d): Path A c d = comp (A) (p @ i) [(i=0) -> q, (i=1) -> r ] kanOp (A: U) (a: A) (p: Path A a a) (b: A) (q: Path A a b) : Path A b b = kan A a a b b p q q kanOpRefl (A: U) (a b: A) (q: Path A a b) : Path (Path A b b) (kanOp A a (refl A a) b q) (refl A b) = comp (refl U A) (q @ j) [ (i = 0) -> q @ j \/ k, (i = 1) -> q @ j \/ k, (j = 1) -> b ] transC (A:U) (a:A) : A = comp (<_>A) a [] lemTransC (A:U) (a:A) : Path A (transC A a) a = comp (<_>A) a [(i=1) -> <_>a] {- compInv' (A:U) (a:A) : (x:A) (p:Path A a x) -> Path (Path A x x) (<_>x) (composition A x a x (p@-i) p) = J A a (\ (x:A) (p:Path A a x) -> Path (Path A x x) (<_>x) (composition A x a x (p@-i) p)) rem where rem : Path (Path A a a) (<_>a) (comp (<_>A) a [(i=0) -> <_>a, (i=1) -> <_>a]) = comp (<_>A) a [(j=0) -> <_>a, (i=0) -> <_>a, (i=1) -> <_>a] -} compInv (A:U) (a b:A) (q:Path A a b) : (x:A) (p:Path A b x) -> Path (Path A a b) q (composition A a x b (composition A a b x q p) (p@-i)) = J A b (\ (x:A) (p: Path A b x) -> Path (Path A a b) q (composition A a x b (composition A a b x q p) (p@-i))) rem where rem : Path (Path A a b) q (comp (<_>A) (comp (<_>A)(q@i) [(i=0) -> <_>a, (i=1)-><_>b]) [(i=0)-><_>a, (i=1)-><_>b]) = comp (<_>A) (comp (<_>A)(q@i) [(j=0)-><_>q@i, (i=0)-><_>a, (i=1)-><_>b]) [(j=0)-><_>q@i, (i=0)-><_>a, (i=1)-><_>b] -- f o f^-1 = 1_a compPathInv (A: U) (a b: A) (p: Path A a b) : Path (Path A a a) (composition A a b a p ( p @ -i)) (<_> a) = comp (<_>A) (p @ j /\ -k) [ (j=0) -> <_> a, (j=1) -> p @ -i /\ -k, (k=1) -> <_> a ] -- f^-1 o f = 1_b compInvPath (A: U) (a b: A) (p: Path A a b) : Path (Path A b b) (composition A b a b ( p @ -i) p) (<_> b) = comp (<_>A) (p @ -i \/ j) [ (i=0) -> <_> b, (j=1) -> <_> b, (i=1) -> p @ j \/ k ] -- Groupoid Interpretation -- id_a o f = f compPathL (A:U) (a b:A) (p: Path A a b) : Path (Path A a b) p (composition A a a b (<_>a) p) = comp (<_>A) a [ (i=0) -> <_> a, (i=1) -> p, (j=0) -> (p@i/\k) ] -- f o id_b = f compPathR (A:U) (a b:A) (p: Path A a b) : Path (Path A a b) p (composition A a b b p (<_>b)) = comp (<_>A) (p@i) [ (i=0) -> <_> a, (i=1) -> <_>b, (j=0) -> <_>(p@i) ] compPathQ (A:U) (a b c d:A) (f: Path A a b) (g: Path A b c) (h: Path A c d) : Path (Path A a d) (composition A a c d (composition A a b c f g) h) (composition A a b d f (composition A b c d g h)) = J A a (\(b : A) (f : Path A a b) -> (c d : A) -> (g : Path A b c) -> (h : Path A c d) -> Path (Path A a d) (composition A a c d (composition A a b c f g) h) (composition A a b d f (composition A b c d g h))) (\(c d : A) (g : Path A a c) (h : Path A c d) -> comp (<_> Path A a d) (composition A a c d g h) [ (i = 0) -> composition A a c d (compPathL A a c g @ j) h, (i = 1) -> compPathL A a d (composition A a c d g h) ]) b f c d g h 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) mapOverComp (A B : U) (f : A -> B) (a b c : A) (p : Path A a b) (q : Path A b c) : Path (Path B (f a) (f c)) (composition B (f a) (f b) (f c) ( f (p @ i)) ( f (q @ i))) ( f (composition A a b c p q @ i)) = J A b (\(z : A) (r : Path A b z) -> Path (Path B (f a) (f z)) (composition B (f a) (f b) (f z) ( f (p @ i)) ( f (r @ i))) ( f (composition A a b z p r @ i))) (J A a (\(z : A) (p : Path A a z) -> Path (Path B (f a) (f z)) (composition B (f a) (f z) (f z) ( f (p @ i)) (<_> f z)) ( f (composition A a z z p (<_> z) @ i))) ( comp (<_> Path B (f a) (f a)) (<_> f a) [ (i = 0) -> kanOpRefl B (f a) (f a) (<_> f a) @ -j, (i = 1) -> mapOnPath A B f a a (kanOpRefl A a a (<_> a) @ -j) ]) b p) c q -- 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]) substToComp (A : U) (a b c : A) (p : Path A b c) (q : Path A a b) : Path (Path A a c) (transport ( Path A a (p @ i)) q) (composition A a b c q p) = <_> composition A a b c q p -- 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