```----------------------------------------------------------------------
-- 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)
```