```----------------------------------------------------------------------
-- 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 fibrations where

open import prelude
open import impredicative
open import interval
open import cof

----------------------------------------------------------------------
-- Path composition structure
----------------------------------------------------------------------
Comp : OI → (Int → Set) → Set
Comp e A = (φ : Cof)(f : [ φ ] → Π A) →
⟦ x₁ ∈ (A ⟨ e ⟩) ∣ (φ , f) ∙ ⟨ e ⟩ ↗ x₁ ⟧ →
⟦ x₀ ∈ (A ⟨ ! e ⟩) ∣ (φ , f) ∙ ⟨ ! e ⟩ ↗ x₀ ⟧

----------------------------------------------------------------------
-- Fibrations
----------------------------------------------------------------------
Fib : {Γ : Set}(A : Γ → Set) → Set
Fib {Γ} A = (e : OI)(p : Int → Γ) → Comp e (A ∘ p)

----------------------------------------------------------------------
-- Terminal object is fibrant
----------------------------------------------------------------------
FibUnit : {Γ : Set} → Fib(λ(_ : Γ) → Unit)
fst (FibUnit _ _ _ _ (unit , _))   = unit
snd (FibUnit _ _ _ _ (unit , _)) _ = refl

----------------------------------------------------------------------
-- Initial object is fibrant
----------------------------------------------------------------------
Fib∅ : {Γ : Set} → Fib(λ(_ : Γ) → ∅)
Fib∅ _ _ _ _ (() , _)

----------------------------------------------------------------------
-- Fibrations are closed under isomorphism
----------------------------------------------------------------------
_≅_ : {Γ : Set}(A B : Γ → Set) → Set
_≅_ {Γ} A B = (x : Γ) → Σ f ∈ (A x → B x) , Σ g ∈ (B x → A x) , (g ∘ f ≡ id) × (f ∘ g ≡ id)

FibIso : {Γ : Set}(A B : Γ → Set) → (A ≅ B) → Fib A → Fib B
FibIso A B iso α e p φ q b = b' where
!e : Int
!e = ⟨ ! e ⟩
f : (i : Int) → A (p i) → B (p i)
f i = fst (iso (p i))
g : (i : Int) → B (p i) → A (p i)
g i = fst (snd (iso (p i)))
q' : [ φ ] → Π (A ∘ p)
q' u i = g i (q u i)
a : ⟦ a ∈ ((A ∘ p) ⟨ e ⟩) ∣ ((φ , q') ∙ ⟨ e ⟩) ↗ a ⟧
fst a = g ⟨ e ⟩ (fst b)
snd a u = cong (g ⟨ e ⟩) (snd b u)
a' : ⟦ a ∈ ((A ∘ p) !e) ∣ ((φ , q') ∙ !e) ↗ a ⟧
a' = α e p φ q' a
b' : ⟦ b ∈ ((B ∘ p) !e) ∣ ((φ , q) ∙ !e) ↗ b ⟧
fst b' = f !e (fst a')
snd b' u = trans fgq≡b' (symm (fgq≡q)) where
fgq≡b' : f !e (g !e (q u !e)) ≡ fst b'
fgq≡b' = cong (f !e) (snd a' u)
fgq≡q : f !e (g !e (q u !e)) ≡ q u !e
fgq≡q = cong (λ f → f (q u !e)) (snd (snd (snd (iso (p !e)))))

----------------------------------------------------------------------
-- Path filling structure
----------------------------------------------------------------------
Fill : OI → (Int → Set) → Set
Fill e A =
(φ : Cof)
(f : [ φ ] → Π A)
(a : A ⟨ e ⟩)
(_ : prf ((φ , f) ∙ ⟨ e ⟩ ↗ a))
→ --------------------------------------
⟦ p ∈ Π A ∣ ((φ , f ) ↗ p) & (p ⟨ e ⟩ ≈ a) ⟧

----------------------------------------------------------------------
-- Compatible partial functions
----------------------------------------------------------------------
_⌣_ : {A : Set} → □ A → □ A → Ω
(φ , f) ⌣ (ψ , g) = All u ∈ [ φ ] , All v ∈ [ ψ ] , f u ≈ g v

_∪_ :
{A : Set}
{φ ψ : Cof}
(f : [ φ ] → A)
(g : [ ψ ] → A)
{p : prf((φ , f) ⌣ (ψ , g))}
→ ---------------------------
[ φ ∨ ψ ] → A
_∪_ {A} {φ} {ψ} f g {p} w = ∥∥-elim h q w where

h : [ φ ] ⊎ [ ψ ] → A
h (inl u) = f u
h (inr v) = g v

q : (z z' : [ φ ] ⊎ [ ψ ]) → h z ≡ h z'
q (inl _) (inl _) = cong f (eq (fst φ))
q (inl u) (inr v) = p u v
q (inr v) (inl u) = symm (p u v)
q (inr _) (inr _) = cong g (eq (fst ψ))

----------------------------------------------------------------------
-- Path filling from path composition
----------------------------------------------------------------------

private
fillInternal :
{Γ : Set}
{A : Γ → Set}
(e : OI)
(α : Fib A)
(p : Int → Γ)
(φ : Cof)
(f : [ φ ] → Π (A ∘ p))
(a : A (p ⟨ e ⟩))
(u : prf ((φ , f) ∙ ⟨ e ⟩ ↗ a))
→ -----------
Σ fill ∈ ⟦ p ∈ Π (A ∘ p) ∣ ((φ , f ) ↗ p) & (p ⟨ e ⟩ ≈ a) ⟧ , fst fill ⟨ ! e ⟩ ≡ fst (α e p φ f (a , u))
fillInternal {Γ} {A} e α p φ f a u = (result , fillAtOne) where
p' : (i : Int) → Int → Γ
p' i j = p (cnx e i j)

f' : (i : Int) → [ φ ] → Π(A ∘ (p' i))
f' i u j = f u (cnx e i j)

g : (i : Int) → [ i ≈OI e ] → Π(A ∘ (p' i))
g .(⟨ e ⟩) refl j = a

agree : (i : Int) → prf ((φ , f' i) ⌣ (i ≈OI e , g i))
agree .(⟨ e ⟩) v refl = funext (λ j → u v)

h : (i : Int) → [ φ ∨ i ≈OI e ] → Π(A ∘ (p' i))
h i = _∪_ {φ = φ} {ψ = i ≈OI e} (f' i) (g i) { p = agree i }

AtZero : Int → Ω
AtZero i = ((φ ∨ i ≈OI e) , h i) ∙ ⟨ e ⟩ ↗ a
hAtZero : (i : Int) → prf (AtZero i)
hAtZero i v = ∥∥-rec (AtZero i) (cases i) v v where
cases : (i : Int) → prf (fst φ) ⊎ (i ≡ ⟨ e ⟩) → prf (AtZero i)
cases i (inl x) v = -- φ holds
proof:
snd (((φ ∨ i ≈OI e) , h i) ∙ ⟨ e ⟩) v
≡[ cong (snd (((φ ∨ i ≈OI e) , h i) ∙ ⟨ e ⟩)) (equ ((fst φ or i ≈ ⟨ e ⟩)) v (∣ inl x ∣)) ]≡
snd (((φ ∨ i ≈OI e) , h i) ∙ ⟨ e ⟩) (∣ inl x ∣)
≡[ refl ]≡
f x ⟨ e ⟩
≡[ u x ]≡
a
qed
cases .(⟨ e ⟩) (inr refl) v = -- i=0 holds
proof:
snd (((φ ∨ ⟨ e ⟩ ≈OI e) , h ⟨ e ⟩) ∙ ⟨ e ⟩) v
≡[ cong (snd (((φ ∨ ⟨ e ⟩ ≈OI e) , h ⟨ e ⟩) ∙ ⟨ e ⟩)) (equ ((fst φ or ⟨ e ⟩ ≈ ⟨ e ⟩)) v (∣ inr refl ∣)) ]≡
snd (((φ ∨ ⟨ e ⟩ ≈OI e) , h ⟨ e ⟩) ∙ ⟨ e ⟩) (∣ inr refl ∣)
≡[ refl ]≡
g ⟨ e ⟩ refl ⟨ e ⟩
≡[ refl ]≡
a
qed

fill : (i : Int) → ⟦ a ∈ (A ∘ p) i ∣ ((φ ∨ i ≈OI e) , h i) ∙ ⟨ ! e ⟩ ↗ a ⟧
fill i = (α e (p' i) (φ ∨ i ≈OI e) (h i) (a , hAtZero i))

extendsF : (v : [ φ ])(i : Int) → f v i ≡ fst (fill i)
extendsF v i = snd (fill i) ∣ inl v ∣

atZero : fst (fill ⟨ e ⟩) ≡ a
atZero = symm (snd (fill ⟨ e ⟩) ∣ inr refl ∣)

result : ⟦ p ∈ Π (A ∘ p) ∣ ((φ , f ) ↗ p) & (p ⟨ e ⟩ ≈ a) ⟧
fst result i = fst (fill i)
fst (snd result) v = funext (extendsF v)
snd (snd result) = atZero

φAtOne : (φ ∨ ⟨ ! e ⟩ ≈OI e) ≡ φ
φAtOne = cofEq (propext forwards backwards) where
forwards : prf (fst (φ ∨ ⟨ ! e ⟩ ≈OI e)) → prf (fst φ)
forwards v = ∥∥-rec (fst φ) cases v where
cases : prf (fst φ) ⊎ (⟨ ! e ⟩ ≡ ⟨ e ⟩) → prf (fst φ)
cases (inl p) = p
cases (inr !e=e) = e≠!e (symm !e=e)
backwards : prf (fst φ) → prf (fst (φ ∨ ⟨ ! e ⟩ ≈OI e))
backwards v = ∣ inl v ∣

propSwap :
{A : Set}
{P Q : Cof}
(p : P ≡ Q)
{f : [ P ] → A}
(u : [ Q ])
(v : [ P ])
→ -----------
subst (λ φ → [ φ ] → A) p f u ≡ f v
propSwap {A} {P} .{P} refl {f} u v = cong f (equ (fst P) u v)

hAtOne : _≡_ {A = □ ((i : Int) → A (p i))} ((φ ∨ ⟨ ! e ⟩ ≈OI e) , h ⟨ ! e ⟩) (φ , f)
hAtOne = Σext φAtOne (funext hIi≡fi) where
hIi≡fi : (u : [ φ ]) → subst (λ φ₁ → [ φ₁ ] → (i : Int) → A (p i)) φAtOne (h ⟨ ! e ⟩) u ≡ f u
hIi≡fi u =
proof:
subst (λ φ₁ → [ φ₁ ] → (i : Int) → A (p i)) φAtOne (h ⟨ ! e ⟩) u
≡[ propSwap φAtOne u  ∣ inl u ∣ ]≡
h ⟨ ! e ⟩  ∣ inl u ∣
≡[ refl ]≡
f u
qed

tupleFiddle :
{A : Set}
{B : A → Set}
{C : (x : A) → B x → Set}
{a a' : A}
{b : B a}{b' : B a'}
{c : C a b}{c' : C a' b'}
(p : ((a , b) , c) ≡ ((a' , b') , c'))
→ -----------
(a , (b , c)) ≡ (a' , (b' , c'))
tupleFiddle refl = refl

abstract
fillAtOne : fst (fill ⟨ ! e ⟩) ≡ fst (α e p φ f (a , u))
fillAtOne =
proof:
fst (fill ⟨ ! e ⟩)
≡[ refl ]≡
fst (α e p (φ ∨ ⟨ ! e ⟩ ≈OI e) (h ⟨ ! e ⟩) (a , hAtZero ⟨ ! e ⟩))
≡[ cong (λ{(ψ , f , u) → fst (α e p ψ f (a , u))}) (tupleFiddle (Σext hAtOne (eq (((φ , f) ∙ ⟨ e ⟩ ↗ a))))) ]≡
fst (α e p φ f (a , u))
qed

abstract
fill :
{Γ : Set}
{A : Γ → Set}
(e : OI)
(α : Fib A)
(p : Int → Γ)
→ -----------
Fill e (A ∘ p)
fill {Γ} {A} e α p φ f a u = fst (fillInternal {A = A} e α p φ f a u)

abstract
fillAtEnd :
{Γ : Set}
{A : Γ → Set}
(e : OI)
(α : Fib A)
(p : Int → Γ)
(φ : Cof)
(f : [ φ ] → Π (A ∘ p))
(a : A (p ⟨ e ⟩))
(u : prf ((φ , f) ∙ ⟨ e ⟩ ↗ a))
→ -----------
fst (fill {A = A} e α p φ f a u) ⟨ ! e ⟩ ≡ fst (α e p φ f (a , u))
fillAtEnd {Γ} {A} α e p φ f a u = snd (fillInternal {A = A} α e p φ f a u)

```