{- 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
   = <i>(p z.1@i,h (p z.1@i) (comp (<j>B (p z.1@i\/-j)) z.2 [(i=1)-><j>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 (<i> P (p@i)) u0 u1)
                (Path (P a1) (transport (<i> P (p@i)) u0) u1)
       = <j>PathP (<i>P (p@j\/i)) (comp (<i>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 (<i>B (p@i)) t.2 u.2)
                (Path (B u.1) (transport (<i>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 (<i>B (p@i)) t.2 u.2) = substInv U isProp T0 T1 rem rem1
 where P : Path U (B t.1) (B u.1) = <i>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