----------------------------------------------------------------------
-- This Agda code is designed to accompany the paper "Axioms for
-- Modelling Cubical Type Theory in a Topos". It is currently a work
-- in progress and still includes postulates/holes in certain places.
-- It also needs some tidying up and possibily reorganisation.
--
-- The idea for getting an impredicative universe of propositions Ω
-- comes from Martin Escardo, more details can be found at:
--
--          http://www.cs.bham.ac.uk/~mhe/impredicativity/          
----------------------------------------------------------------------

{-# OPTIONS --rewriting #-}
module equivs where 

open import prelude
open import impredicative
open import interval
open import cof
open import fibrations
open import Data.products
open import Data.paths
open import Data.id

----------------------------------------------------------------------
-- Contr and Ext
----------------------------------------------------------------------
Contr : Set  Set
Contr A = Σ a₀  A , ((a : A)  a₀ ~ a)

Ext : Set  Set
Ext A = (φ : Cof)(f : [ φ ]  A)   a  A  (φ , f)  a 

ext2contr : {A : Set}  Ext A  Contr A
fst (ext2contr e) = fst (e cofFalse ∅-elim)
fst (snd (ext2contr e) a) i = fst (e (i ≈I)  _  a))
fst (snd (snd (ext2contr {A} e) a)) = cong (λ{(φ , f)  fst (e φ f)}) (Σext bothFalse bothElim) where
  bothFalse : O ≈I  cofFalse
  bothFalse = Σext (propext O≠I ∅-elim) refl
  bothElim : subst  z  [ z ]  A) bothFalse  _  a)  ∅-elim
  bothElim = funext  false  ∅-elim false)
snd (snd (snd (ext2contr e) a)) = symm (snd (e (I ≈I)  _  a)) refl)

contr2ext : {Γ : Set}{A : Γ  Set}(α : Fib A)(x : Γ)  Contr (A x)  Ext (A x)
contr2ext {Γ} {A} α x (a , eq) φ f = (fst a' ,  u  trans (q u) (p u))) where
  path : [ φ ]  Int  A x
  path u = fst (eq (f u))
  
  a' :  a'  (A x)  (φ , path)  I  a' 
  a' = α O'  _  x) φ path (a ,  u  fst (snd (eq (f u)))))

  p : (u : [ φ ])  f u  fst (eq (f u)) I
  p u = symm (snd (snd (eq (f u))))

  q : (u : [ φ ])  fst (eq (f u)) I  fst a'
  q = snd a'

ext2fib : {Γ : Set}{A : Γ  Set}  ((x : Γ)  Ext (A x))  Fib A
ext2fib ext e p φ f a = ext (p  ! e ) φ  z  f z  ! e )

----------------------------------------------------------------------
-- Equivalences and quasi-inverses
----------------------------------------------------------------------
Fiber : {A B : Set}(f : A  B)(b : B)  Set
Fiber {A} f b = Σ a  A , f a ~ b

Equiv : {A B : Set}(f : A  B)  Set
Equiv {A} {B} f = (b : B)  Contr (Fiber f b)

Qinv : {A B : Set}(f : A  B)  Set
Qinv {A} {B} f = Σ g  (B  A) , ((b : B)  f (g b) ~ b) × ((a : A)  g (f a) ~ a)

fiberext : {A B : Set}{f : A  B}{b : B}{x y : Fiber f b}  fst x  fst y  fst (snd x)  fst (snd y)  x  y
fiberext refl refl = Σext refl (PathExt refl)

-- This is a standard result in HoTT.
-- Work towards proving this result can be found in the
-- scratchpad module (accessible from the root module).
postulate
 qinv2equiv :
  {Γ : Set}{A B : Γ  Set}(α : Fib A)(β : Fib B)
  (f : (x : Γ)  A x  B x)(x : Γ)  Qinv (f x)  Equiv (f x)

qinv2equivSimple :
  {A B : Set}(α : Fib {Γ = Unit}  _  A))(β : Fib {Γ = Unit}  _  B))
  (f : A  B)  Qinv (f)  Equiv (f)
qinv2equivSimple α β f qinv = qinv2equiv α β  _  f) tt qinv

  
equiv2qinv :
  {Γ : Set}{A B : Γ  Set}(α : Fib A)(β : Fib B)
  (f : (x : Γ)  A x  B x)(x : Γ)  Equiv (f x)  Qinv (f x)
fst (equiv2qinv α β f x equiv) b = fst (fst (equiv b))
fst (snd (equiv2qinv α β f x equiv)) b = snd (fst (equiv b))
snd (snd (equiv2qinv α β f x equiv)) a =
  (fst  (fst path)) , cong fst (fst (snd path)) , cong fst (snd (snd path)) where
    path = snd (equiv (f x a)) ((a ,  _  f x a) , refl , refl))

----------------------------------------------------------------------
-- Fext
----------------------------------------------------------------------
Fext :
 {A B : Set}
 (f : A  B)  Set
Fext {A} {B} f = (b : B)(φ : Cof)(p : ( p  ([ φ ]  A)  (φ , f  p)  b ))
    c  (Σ a  A , f a ~ b)  (φ ,  u  (fst p u , reflPath' (snd p u))))  c 

fext2qinv : {A B : Set}{f : A  B}  Fext f  Qinv f
fst (fext2qinv fext) b = fst (fst (fext b cofFalse (∅-elim ,  u  ∅-elim u))))
fst (snd (fext2qinv fext)) b = snd (fst (fext b cofFalse (∅-elim ,  u  ∅-elim u))))
fst (snd (snd (fext2qinv {A} {B} {f} fext)) a) i = fst (fst (fext (f a) (i ≈I) ((λ _  a) ,  _  refl))))
fst (snd (snd (snd (fext2qinv {A} {B} {f} fext)) a)) = cong (λ{(φ , e)  fst (fst (fext (f a) φ e))}) falseEq where
  falseEq : (O ≈I ,  _  a) ,  _  refl))  (cofFalse , ∅-elim ,  u  ∅-elim u))
  falseEq = Σext (cofEq (propext O≠I ∅-elim)) (Σext (funext  emp  ∅-elim emp)) (funext  emp  ∅-elim emp)))
snd (snd (snd (snd (fext2qinv {A} {B} {f} fext)) a)) = symm (Σeq₁ (snd (fext (f a) (I ≈I) ((λ _  a) ,  _  refl))) refl))

equiv2fext :
  {Γ : Set}
  {A B : Γ  Set}
  (α : Fib A)
  (β : Fib B)
  (f : (x : Γ)  A x  B x)
  (x : Γ)
   ----------
  Equiv (f x)  Fext (f x)
equiv2fext α β f x equiv b φ p = ce α β f x b (equiv b) φ  u  (fst p u , reflPath' (snd p u))) where
  ce : {Γ : Set}{A B : Γ  Set}(α : Fib A)(β : Fib B)(f : (x : Γ)  A x  B x)(x : Γ)(b : B x) 
     Contr (Fiber (f x) b)  Ext (Fiber (f x) b)
  ce {Γ} {A} {B} α β f x b = contr2ext σ (x , b) where
    A' : Σ Γ B  Set
    A' (x , b) = A x
    PathB : Σ (Σ Γ B) A'  Set
    PathB ((x , b) , a) = f x a ~ b
    σ : Fib {Γ = Σ Γ B} (λ{(x , b)  Fiber (f x) b})
    σ = FibΣ {B = PathB}  e p  α e (fst  p))  e p  FibPath {A = B} β e  i  let ((x , b) , a) = p i in (x , f x a , b)))

fext2fib :
   {Γ : Set}
   {A B : Γ  Set}
   {f : (x : Γ)  A x  B x}
   (fext : (x : Γ)  Fext (f x))
    ----------
   Fib B  Fib A
fext2fib {Γ} {A} {B} {f} fext β e p φ g (a₀ , g↗a₀) = a₁ where
  h : [ φ ]  Π (B  p)
  h u i = f (p i) (g u i)
  b₁ :  b  B (p  ! e )  (φ , h)   ! e   b 
  b₁ = β e p φ h ((f (p  e ) a₀ ,  u  cong (f (p  e )) (g↗a₀ u))))
  q : [ φ ]  A (p  ! e )
  q u = g u  ! e 
  a₁ :  a  A (p  ! e )  (φ , g)   ! e   a 
  fst a₁ = fst (fst (fext (p  ! e ) (fst b₁) φ ((q , snd b₁))))
  snd a₁ u = Σeq₁ (snd (fext (p  ! e ) (fst b₁) φ ((q , snd b₁))) u)