{- Univalence:
   - univ.
   Copyright (c) Groupoid Infinity, 2014-2018. -}

module univ where
import retract
import equiv
import sigma
import path
import iso

{- Univalence theorems are isomorphic at any level of equality:

   univalence (B: U): isContr ((A: U) * equiv B A) = undefined

   1. Path (A = B)  - path
   2. Equiv (A ~ B) - sigma, fibrant
   3. Iso (A == B)  - adjoints

   Path: built-in

   Equiv:

   isContr (A: U): U = (x: A) * ((y: A) -> Path A x y)
   fiber (A B: U) (f: A -> B) (y: B): U = (x: A) * Path B y (f x)
   isEquiv (A B: U) (f: A -> B): U = (y: B) -> isContr (fiber A B f y)

   Iso:

   isIso (A B: U): U
     = (f: A -> B)
     * (g: B -> A)
     * (s: section A B f g)
     * (t: retract A B f g)
     * unit

   Iso(Equiv,Path)                   -- equivToPath, pathToEquiv
   Equiv(swap(Equiv),Iso(Equ,Equiv)) -- univalence, (slow)
   Equiv(Equiv,Iso(Path,Equiv))      -- univalence, (fast)
   Path(Path,Equiv)                  -- pathEqEquiv
   Equiv(Path,Equiv)                 -- pathEquivEquiv -}

-- This is Corollary 10 of the cubical type theory paper
-- (the proof of theorem 9 is inlined) (due to Fabian Ruch).
univalenceAlt (B: U): isContr ((A: U) * equiv A B)
  = ((B,idEquiv B), \(w: (X:U) * equiv X B) ->
       <i> let GlueB: U = Glue B [(i=0) -> (B,idEquiv B), (i=1) -> w]
               unglueB (g: GlueB): B = unglue g [(i=0) -> (B,idEquiv B),(i=1) -> w]
           in (GlueB,unglueB, \(b: B) ->
         ((glue (comp (<j> B) b [(i=0) -> <j> b,(i=1) -> (w.2.2 b).1.2])
                [(i=0) -> b, (i=1) -> (w.2.2 b).1.1] ,
                 fill (<j> B) b [(i=0) -> <j> b, (i=1) -> (w.2.2 b).1.2]),
          \(v: fiber GlueB B unglueB b) -> <j>
          (glue (comp (<j> B) b [(i=0) -> <k> v.2 @ (j /\ k),
                                 (i=1) -> ((w.2.2 b).2 v @ j).2,
                                 (j=0) -> fill (<j> B) b [(i=0) -> <j> b, (i=1) -> (w.2.2 b).1.2],
                                 (j=1) -> v.2])
                [(i=0)-> v.2 @ j,(i=1) -> ((w.2.2 b).2 v @ j).1],
                 fill (<j> B) b [(i=0) -> <l> v.2 @ (j /\ l),
                                 (i=1) -> ((w.2.2 b).2 v @ j).2,
                                 (j=0) -> fill (<j> B) b [(i=0) -> <j> b, (i=1) -> (w.2.2 b).1.2],
                                 (j=1) -> v.2]))))

-- A version univalence. This is Corollary 11 of the cubical type theory paper.
thmUniv (t: (A X: U) -> Path U X A -> equiv X A) (A: U)
      : (X: U) -> isEquiv (Path U X A) (equiv X A) (t A X)
      = equivFunFib U (\(X : U) -> Path U X A) (\(X: U) -> equiv X A)
                      (t A) (isContrSingl' U A) (univalenceAlt A)

univalence (A X: U) : isEquiv (Path U X A) (equiv X A) (transEquiv' A X)
  = thmUniv transEquiv' A X

-- Univalence Intro
ua (A B: U) (e: equiv A B): Path U A B
  = <i> Glue B [ (i = 0) -> (A,e), (i = 1) -> (B,idEquiv B) ]

uabeta (A B: U) (e: equiv A B): Path (A -> B) (trans A B (ua A B e)) e.1
  = <i> \(a: A) -> fill (<_> B) (fill (<_> B) (e.1 a) [] @ -i) [] @ -i

uabetaTransEquiv (A B: U) (e: equiv A B) : Path (A -> B) (transEquiv A B (ua A B e)).1 e.1
  = <i> \(a: A) -> (uabeta A B e @ i) (fill (<_> A) a [] @ -i)

uaret (A B: U): retract (equiv A B) (Path U A B) (ua A B) (transEquiv A B)
  = \(e: equiv A B) -> equivLemma A B (transEquiv A B (ua A B e)) e (uabetaTransEquiv A B e)

f1 (A: U) (p: (B: U) * equiv A B): singl U A
  = (p.1,ua A p.1 p.2)

f2 (A: U) (p: singl U A): ((B: U) * equiv A B)
  = (p.1,transEquiv A p.1 p.2)
corrUniv (A B: U) : Path U (Path U A B) (equiv A B)
  = equivPath (Path U A B) (equiv A B) (transEquiv' B A) (univalence B A)

corrUniv' (A B: U): equiv (Path U A B) (equiv A B)
  = (transEquiv' B A,univalence B A)

-- Elimination principle for equivalences
contrSinglEquiv (A B: U) (f: equiv A B): Path ((X: U) * equiv X B) (B,idEquiv B) (A,f)
  = isContrProp ((X: U) * equiv X B) (univalenceAlt B) (B,idEquiv B) (A,f)

elimEquiv (B: U) (P: (A: U) -> (A -> B) -> U) (d: P B (idfun B))
          (A: U) (f: equiv A B): P A f.1
  = subst((X: U) * equiv X B) T (B,idEquiv B) (A,f) (contrSinglEquiv A B f) d where
     T (z:(X: U) * equiv X B): U = P z.1 z.2.1

-- Elimination principle for iso
elimIso (B: U) (Q: (A: U) -> (A -> B) -> (B -> A) -> U)
        (h1: Q B (idfun B) (idfun B)) (A: U) (f: A -> B): (g: B -> A) ->
        section A B f g -> retract A B f g -> Q A f g = rem1 A f where
  P (A: U) (f: A -> B): U
    = (g: B -> A) -> section A B f g -> retract A B f g -> Q A f g
  rem: P B (idfun B) = \ (g: B -> B) (sg: section B B (idfun B) g) (rg: retract B B (idfun B) g) ->
    substInv (B -> B) (Q B (idfun B)) g (idfun B) (<i> \(b: B) -> (sg b) @ i) h1
  rem1 (A: U) (f: A -> B): P A f = \(g: B -> A) (sg: section A B f g) (rg: retract A B f g) ->
    elimEquiv B P rem A (f,isoToEquiv A B f g sg rg) g sg rg

elimIsIso (A : U) (Q : (B : U) -> (A -> B) -> (B -> A) -> U)
         (d : Q A (idfun A) (idfun A)) (B : U) (f : A -> B) (g : B -> A)
         (sg : section A B f g) (rg : retract A B f g) : Q B f g =
  elimIso A (\(B : U) (f : B -> A) (g : A -> B) -> Q B g f) d B g f rg sg

------------------------------------------ VERY SLOW
{-
uaretsig (A: U): retract ((B: U) * equiv A B) (singl U A) (f1 A) (f2 A)
  = \(p: (B: U) * equiv A B) -> <i> (p.1,uaret A p.1 p.2 @ i)

univalenceAlt' (B: U) : isContr ((A: U) * equiv B A)
  = retIsContr ((A:U) * equiv B A) (singl U B) (f1 B) (f2 B) (uaretsig B) (isContrPath B)

thmUniv' (t: (A X: U) -> Path U A X -> equiv A X) (A: U)
       : (X: U) -> isEquiv (Path U A X) (equiv A X) (t A X)
       = equivFunFib U (\(X: U) -> Path U A X) (\(X: U) -> equiv A X)
                       (t A) (isContrSingl U A) (univalenceAlt' A)

univalence' (A X: U): isEquiv (Path U A X) (equiv A X) (transEquiv A X)
  = thmUniv' transEquiv A X
-}
-----------------