module iso_sigma where
import path
import pi
import sigma
import iso

-- used in grothedieck.ctt and below
pathSig (A:U) (B : A -> U) (t u : Sigma A B) :
  Path U (Path (Sigma A B) t u) ((p : Path A t.1 u.1) * PathP (<i> B (p @ i)) t.2 u.2)
  = isoPath T0 T1 f g s t where
  T0 : U = Path (Sigma A B) t u
  T1 : U = (p:Path A t.1 u.1) * PathP (<i> B (p@i)) t.2 u.2
  f (q:T0) : T1 = (<i> (q@i).1,<i> (q@i).2)
  g (z:T1) : T0 = <i>(z.1 @i,z.2 @i)
  s (z:T1) : Path T1 (f (g z)) z = refl T1 z
  t (q:T0) : Path T0 (g (f q)) q = refl T0 q

-- used in algstruct
setSig (A:U) (B: A-> U) (sA: isSet A) (sB : (x:A) -> isSet (B x)): isSet (Sigma A B) = goal where
  goal (t u : Sigma A B) : isProp (Path (Sigma A B) t u)
    = substInv U isProp (Path (Sigma A B) t u) ((p:T) * C p) rem3 rem2 where
    T : U = Path A t.1 u.1
    C (p:T) : U = PathP (<i> B (p@i)) t.2 u.2
    rem (p : T) : isProp (C p) = corSigSet A B sB t u p
    rem1 : isProp T = sA t.1 u.1
    rem2 : isProp ((p:T) * C p) = propSig T C rem1 rem
    rem3 : Path U (Path (Sigma A B) t u) ((p:T) * C p) = pathSig A B t u

pathSig2 (A:U) (P: A -> U) (t u: Sigma A P)
         (p: Path A t.1 u.1)
         (s: PathP (<i> P (p @ i)) t.2 u.2)
       : Path (Sigma A P) t u
       = comp (<i> pathSig A P t u @ -i) (p,s) []

pathSig3 (A:U) (P : A -> U) (t u : Sigma A P) (pp: (p : Path A t.1 u.1) * Path (P u.1) (transport (<i>P (p @ i)) t.2) u.2): Path (Sigma A P) t u
  = pathSig2 A P t u (pp.1, transport foo pp.2) where
  p: Path A t.1 u.1 = pp.1
  P' : Path U (P t.1) (P u.1) = <i>P (p@i)
  T0 : U = PathP P' t.2 u.2
  T1 : U = Path (P u.1) (transport P' t.2) u.2
  foo : Path U T1 T0 = sym U T0 T1 (pathSig0 A P t u p)
  pathSig2 (A:U) (P : A -> U) (t u : Sigma A P) (pp: (p : Path A t.1 u.1) * PathP (<i> P (p @ i)) t.2 u.2): Path (Sigma A P) t u
    = comp (<i> pathSig A P t u @ -i) pp []

pathSigHoTT (A: U) (P: A -> U) (t u: Sigma A P) (p: Path A t.1 u.1)
            (s: Path (P u.1) (transport (<i> P (p @ i)) t.2) u.2)
          : Path (Sigma A P) t u
          = pathSig2 A P t u p (transport f s) where
  P': Path U (P t.1) (P u.1) = <i>P (p@i)
  T0: U = PathP P' t.2 u.2
  T1: U = Path (P u.1) (transport P' t.2) u.2
  f: Path U T1 T0 = sym U T0 T1 (pathSig0 A P t u p)

lemContr (A:U) (pA:isProp A) (a:A) : isContr A = (a,rem)
 where rem (y:A) : Path A a y = pA a y

lem3 (A:U) (B:A-> U) (pB : (x:A) -> isProp (B x)) (t u : Sigma A B) (p:Path A t.1 u.1) :
  isContr (PathP (<i>B (p@i)) t.2 u.2) = lemContr T0 (substInv U isProp T0 T1 rem rem1) rem2
 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
       v2 : B u.1 = transport P t.2
       rem1 : isProp T1 = propSet (B u.1) (pB u.1) v2 u.2
       rem2 : T0 = transport (<i>rem@-i) (pB u.1 v2 u.2)

lem6 (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : Path U ((x:A)*P x) A = isoPath T A f g t s
 where
   T : U = (x:A) * P x
   f (z:T) : A = z.1
   g (x:A) : T = (x,(cA x).1)
   s (z:T) : Path T (g (f z)) z = <i>(z.1,((cA z.1).2 z.2)@ i)
   t (x:A) : Path A (f (g x)) x = refl A x

lemSigProp (A:U) (B:A-> U) (pB : (x:A) -> isProp (B x)) (t u : Sigma A B) : Path U (Path (Sigma A B) t u) (Path A t.1 u.1) =
 composition U (Path (Sigma A B) t u) ((p:Path A t.1 u.1) * PathP (<i> B (p@i)) t.2 u.2) (Path A t.1 u.1) rem2 rem1
 where
   T : U = Path A t.1 u.1
   C (p:T) : U = PathP (<i> B (p@i)) t.2 u.2
   rem (p : T) : isContr (C p) = lem3 A B pB t u p
   rem1 : Path U ((p:T) * C p) T = lem6 T C rem
   rem2 : Path U (Path (Sigma A B) t u) ((p:T) * C p) = pathSig A B t u

flipfunIso (A B C: U): Path U (A -> B -> C) (B -> A -> C)
  = isoPath AB BA from to toK fromK where
    AB:    U = A -> B -> C
    BA:    U = B -> A -> C
    from:  AB -> BA = flip A B C
    to:    BA -> AB = flip B A C
    fromK: (f: AB) -> Path AB (to (from f)) f = refl AB
    toK:   (f: BA) -> Path BA (from (to f)) f = refl BA