{- Sigma Type: Copyright (c) Groupoid Infinity, 2014-2018. HoTT 2.7 Sigma-types HoTT 1.6 Dependent pair types (Sigma-types) -} module sigma where import path Sigma (A:U)(B:A->U): U = (x:A) * B(x) dpair (A:U)(B:A->U)(a: A) (b: B a): Sigma A B = (a,b) pi1 (A:U)(B:A->U)(x: Sigma A B): A = x.1 pi2 (A:U)(B:A->U)(x: Sigma A B): B (pi1 A B x) = x.2 sigRec (A:U)(B:A->U)(C: U) (g:(x:A)->B(x)->C) (p: Sigma A B): C = g p.1 p.2 sigInd (A:U)(B:A->U)(C: Sigma A B->U) (p: Sigma A B) (g:(a:A)(b:B(a))->C(a,b)): C p = g p.1 p.2 -- Axiom of Choice ac (A B: U) (R: A -> B -> U): (p: (x:A)->(y:B)*(R x y)) -> (f:A->B)*((x:A)->R(x)(f x)) = \(g: (x:A)->(y:B)*(R x y)) -> (\(i:A)->(g i).1,\(j:A)->(g j).2) total (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (w:Sigma A B) : Sigma A C = (w.1,f (w.1) (w.2)) sigmaIsContr (A: U) (B: A -> U) (u: isContr A) (q: (x: A) -> isContr (B x)) : isContr (Sigma A B) = ((a,g a),r) where a : A = u.1 p : (x:A) -> Path A a x = u.2 g (x:A) : B x = (q x).1 h (x:A) : (y:B x) -> Path (B x) (g x) y = (q x).2 r (z:Sigma A B): Path (Sigma A B) (a,g a) z = (p z.1@i,h (p z.1@i) (comp (B (p z.1@i\/-j)) z.2 [(i=1)->z.2])@i) funDepTr (A:U) (P: A -> U) (a0 a1: A) (p: Path A a0 a1) (u0: P a0) (u1: P a1) : Path U (PathP ( P (p@i)) u0 u1) (Path (P a1) (transport ( P (p@i)) u0) u1) = PathP (P (p@j\/i)) (comp (P (p@j/\i)) u0 [(j=0)-><_>u0]) u1 pathSig0 (A:U) (B: A -> U) (t u: Sigma A B) (p:Path A t.1 u.1) : Path U (PathP (B (p@i)) t.2 u.2) (Path (B u.1) (transport (B (p@i)) t.2) u.2) = funDepTr A B t.1 u.1 p t.2 u.2 corSigSet (A:U) (B:A-> U) (sB : (x:A) -> isSet (B x)) (t u : Sigma A B) (p:Path A t.1 u.1) : isProp (PathP (B (p@i)) t.2 u.2) = substInv U isProp T0 T1 rem rem1 where P : Path U (B t.1) (B u.1) = B (p@i) T0 : U = PathP P t.2 u.2 T1 : U = Path (B u.1) (transport P t.2) u.2 rem : Path U T0 T1 = pathSig0 A B t u p -- funDepTr (B t.1) (B u.1) P t.2 u.2 v2 : B u.1 = transport P t.2 rem1 : isProp T1 = sB u.1 v2 u.2 sigSecondPath (A: U) (P: A -> U) (t u: Sigma A P) (p: Path A t.1 u.1): U = Path (P u.1) (transport p' t.2) u.2 where p' : Path U (P t.1) (P u.1) = mapOnPath A U P t.1 u.1 p