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

open import prelude
open import impredicative
open import interval
open import cof
open import fibrations
open import equivs
open import Data.paths

----------------------------------------------------------------------
-- Glueing
----------------------------------------------------------------------

res : (Γ : Set)(Φ : Γ → Cof) → Set
res Γ Φ = Σ x ∈ Γ , [ Φ x ]

Glue :
{Γ : Set}
(Φ : Γ → Cof)
(A : res Γ Φ → Set)
(B : Γ → Set)
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
Γ → Set
Glue Φ A B f x = Σ a ∈ ((u : [ Φ x ]) → A (x , u)) , ⟦ b ∈ (B x) ∣ All u ∈ [ Φ x ] , f x u (a u) ≈ b ⟧

glue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(xu : res Γ Φ) → A xu → Glue Φ A B f (fst xu)
glue {Γ} {Φ} {A} {B} f (x , u) a = ((λ v → moveA v a) , (f x u a , (λ v → cong (λ{(u , a) → f x u a}) (symm (moveMove v))))) where
moveA : (v : [ Φ x ]) → A (x , u) → A (x , v)
moveA v = subst (λ v → A (x , v)) (eq (fst (Φ x)))
moveMove : (v : [ Φ x ]) → (u , a) ≡ (v , moveA v a)
moveMove v = Σext (eq (fst (Φ x))) refl

unglue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(x : Γ) → Glue Φ A B f x → B x
unglue _ _ (_ , b , _) = b

unglueGlue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(xu : res Γ Φ) → (unglue {Φ = Φ} f (fst xu)) ∘ (glue {Φ = Φ} f xu) ≡ f (fst xu) (snd xu)
unglueGlue f (x , u) = funext (λ a → refl)

glue' :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(x : Γ) → (a : (u : [ Φ x ]) → A (x , u)) → ⟦ b ∈ B x ∣ all [ Φ x ] (λ u → f x u (a u) ≈ b) ⟧ → Glue Φ A B f x
glue' f x a (b , bPrf) = (a , b , bPrf)

unglueGlue' :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(x : Γ) → (a : (u : [ Φ x ]) → A (x , u))
→ (unglue {Φ = Φ} f x) ∘ (glue' {Φ = Φ} f x a) ≡ fst
unglueGlue' f x a = refl

glueUnglue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(x : Γ) → (g : Glue Φ A B f x)
→ glue' {Φ = Φ} f x (fst g) (unglue {Φ = Φ} f x g , snd (snd g)) ≡ g
glueUnglue f x g = refl

helper : {A : Set}{a a' : A}(p : a' ≡ a)(p' : a' ~ a)(eq : reflPath' p ≡ p')(i : Int) → a ≡ fst p' i
helper {A} {a} .{a} refl p' eq i = subst (λ p' → a ≡ fst p' i) eq refl

helper' : {A : Set}{B : Set}{a a' : A}{b : B}(f : A → B)(p : a ≡ a')(q : f a ≡ b)(r : f a' ≡ b)
→ subst (λ x → f x ~ b) p (reflPath' q) ≡ reflPath' r
helper' _ refl refl refl = refl

glueExt :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
{x : Γ}
(g g' : Glue Φ A B f x)
(p : fst g ≡ fst g')
(q : fst (snd g) ≡ fst (snd g'))
→ ---------------
g ≡ g'
glueExt _ (_ , _ , fa≡b) (_ , _ , fa≡b') refl refl =
Σext refl (Σext refl (funext (λ u → uip (fa≡b u) (fa≡b' u))))

helper'' :
{A : Set}
(a a' : A)
(p : a ≡ a')
{B : A → Set}
{C : A → Set}
(f : (x : A) → B x → C x)
(b : B a)
(q : b ≡ b) → f a' (subst B p b) ≡ subst C p (f a b)
helper'' _ _ refl _ _ refl = refl

fextunglue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(v : [ Φ x ]) → A (x , v) → B x)
→ -------------
(x : Γ) → ((v : [ Φ x ]) → Fext (f x v)) → Fib B → Fext (unglue {Φ = Φ} f x)
fextunglue {Γ} {Φ} {A} {B} f x fext β b ψ q = ((g , gPath) , (λ u → Σext (extendsQ u) (extendsQ' u))) where
qa : (v : [ Φ x ]) → ⟦ qa ∈ ((u : [ ψ ]) → A (x , v)) ∣ (ψ , f x v ∘ qa) ↗ b ⟧
fst (qa v) u = fst (fst q u) v
snd (qa v) u = trans (snd q u) (snd (snd (fst q u)) v)
a : (v : [ Φ x ]) → A (x , v)
a v = fst (fst (fext v b ψ (qa v)))
fa≡b : (v : [ Φ x ]) → [ ψ ] → f x v (a v) ≡ b
fa≡b v u =
let step1 = cong (f x v) (symm (Σeq₁ (snd (fext v b ψ (qa v)) u)))
step2 = snd (snd (fst q u)) v
in trans (snd q u) (trans step2 step1)
h : (v : [ Φ x ]) → (f x v (a v)) ~ b
h v = snd (fst (fext v b ψ (qa v)))
qb : [ ψ ∨ Φ x ] → Π (λ _ → B x)
qb = _∪_ {φ = ψ} {ψ = Φ x} (λ _ _ → b) (λ v → fst (h v)) {p = agree} where
agree : prf ((ψ , (λ _ _ → b)) ⌣ (Φ x , (λ v → fst (h v))))
agree u v = funext (λ i →
let rr = snd (fext v b ψ (qa v)) u in
let ss = helper' (f x v) (Σeq₁ rr) ((trans (snd q u) (snd (snd (fst q u)) v))) (fa≡b v u) in
helper (fa≡b v u) (h v) (trans (Σeq₂ rr) (symm ss)) i)
pbRaw : ⟦ p ∈ (Int → B x) ∣ (((ψ ∨ Φ x) , qb) ↗ p) & (p I ≈ b) ⟧
pbRaw = fill I' β (λ _ → x) (ψ ∨ Φ x) qb b (λ uv → or-elim-eq (λ u → qb u I) b refl rightEq uv) where
rightEq : {v : [ Φ x ]} → qb ∣ inr v ∣ I ≡ b
rightEq {v} = snd (snd (snd (fst (fext v b ψ (qa v)))))
pb : Int → B x
pb = fst (pbRaw)
fa≡pbO : (v : [ Φ x ]) → f x v (a v) ≡ pb O
fa≡pbO v = trans step2 step1 where
step1 : f x v (a v) ≡ fst (h v) O
step1 = symm (fst (snd (snd (fst (fext v b ψ (qa v))))))
step2 : fst (h v) O ≡ pb O
step2 = cong (λ p → p O) (fst (snd pbRaw) ∣ inr v ∣)
g : Glue Φ A B f x
g = (a , pb O , fa≡pbO)
gPath : pb O ~ b
fst gPath = pb
fst (snd gPath) = refl
snd (snd gPath) = snd (snd pbRaw)
extendsQ : (u : [ ψ ]) →  fst q u ≡ g
extendsQ u = glueExt {Φ = Φ} f (fst q u) g fstEq sndEq where
fstEq : fst (fst q u) ≡ a
fstEq = funext (λ v → Σeq₁ (snd (fext v b ψ (qa v)) u))
sndEq : fst (snd (fst q u)) ≡ pb O
sndEq = trans (cong (λ p → p O) (fst (snd pbRaw) ∣ inl u ∣)) (snd q u)
extendsQ' :  (u : [ ψ ]) → subst (λ v → unglue {Φ = Φ} f x v ~ b) (extendsQ u)
(reflPath' (snd q u)) ≡ gPath
extendsQ' u = PathExt (funext (λ i → trans (b≡pbi i) (trans (rp≡b i) (substrp=rp i)))) where
b≡pbi : (i : Int) → b ≡ pb i
b≡pbi i = cong (λ p → p i) (fst (snd pbRaw) ∣ inl u ∣)
rp≡b : (i : Int) → fst (reflPath' (snd q u)) i ≡ b --reflPath' (snd q u)
rp≡b i = reflPathEval (snd q u) i
fstSubst : {g g' : Glue Φ A B f x}(p : g ≡ g'){q : unglue {Φ = Φ} f x g ~ b}
→ fst (subst (λ g → unglue {Φ = Φ} f x g ~ b) p q) ≡ fst q
fstSubst refl = refl
substrp=rp : (i : Int) → fst (subst (λ g → unglue {Φ = Φ} f x g ~ b) (extendsQ u)
(reflPath' (snd q u))) i ≡ fst (reflPath' (snd q u)) i
substrp=rp i = cong (λ p → p i) (fstSubst (extendsQ u))

FibGlue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
(equiv : (x : Γ)(v : [ Φ x ]) → Equiv (f x v))
→ ---------------
Fib A → Fib B → Fib (Glue Φ A B f)
FibGlue {Γ} {Φ} {A} {B} f equiv α β = fext2fib fext2 β where
B' : res Γ Φ → Set
B' (x , v) = B x
β' : Fib B'
β' e p ψ q b = β e (fst ∘ p) ψ q b
fext1 : (x : Γ)(v : [ Φ x ]) → Fext (f x v)
fext1 x v = equiv2fext α β' (λ{(x , v) → f x v}) (x , v) (equiv x v)
fext2 : (x : Γ) → Fext (unglue {Φ = Φ} f x)
fext2 x = fextunglue {Φ = Φ} f x (fext1 x) β

----------------------------------------------------------------------
-- Strictifying
----------------------------------------------------------------------
record _≅'_(A B : Set) : Set where
field
f : A → B
g : B → A
inv₁ : g ∘ f ≡ id
inv₂ : f ∘ g ≡ id

postulate
reIm :
(φ : Cof)
(A : [ φ ] → Set)
(B : Set)
(m : (u : [ φ ]) → A u ≅' B)
-> ----------------------
Σ B' ∈ Set , Σ m' ∈ B' ≅' B , ((u : [ φ ]) → (A u , m u) ≡ (B' , m'))

strictify :
{Γ : Set}
(Φ : Γ → Cof)
(A : res Γ Φ → Set)
(B : Γ → Set)
(m : (x : Γ)(u : [ Φ x ]) → A (x , u) ≅' B x)
-> ----------------------
Γ → Set
strictify Φ A B m x = fst (reIm (Φ x)(λ u → A (x , u)) (B x) (m x))

isoB :
{Γ : Set}
(Φ : Γ → Cof)
(A : res Γ Φ → Set)
(B : Γ → Set)
(m : (x : Γ)(u : [ Φ x ]) → A (x , u) ≅' B x)
(x : Γ)
-> ----------------------
strictify Φ A B m x ≅' B x
isoB Φ A B m x = fst (snd (reIm (Φ x)(λ u → A (x , u)) (B x) (m x)))

restrictsToA :
{Γ : Set}
(Φ : Γ → Cof)
(A : res Γ Φ → Set)
(B : Γ → Set)
(m : (x : Γ)(u : [ Φ x ]) → A (x , u) ≅' B x)
(x : res Γ Φ)
-> ----------------------
A x ≡ strictify Φ A B m (fst x)
restrictsToA Φ A B m (x , u) = Σeq₁ (snd (snd (reIm (Φ x)(λ u → A (x , u)) (B x) (m x))) u)

restrictsToM :
{Γ : Set}
(Φ : Γ → Cof)
(A : res Γ Φ → Set)
(B : Γ → Set)
(m : (x : Γ)(u : [ Φ x ]) → A (x , u) ≅' B x)
(x : Γ)
(u : [ Φ x ])
-> ----------------------
(A (x , u) , m x u) ≡ (strictify Φ A B m x , isoB Φ A B m x)
restrictsToM Φ A B m x u = snd (snd (reIm (Φ x)(λ u → A (x , u)) (B x) (m x))) u

----------------------------------------------------------------------
-- Strict glueing
----------------------------------------------------------------------
SGlue :
{Γ : Set}
(Φ : Γ → Cof)
(A : res Γ Φ → Set)
(B : Γ → Set)
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
Γ → Set

private
fIso :
{Γ : Set}
(Φ : Γ → Cof)
{A : res Γ Φ → Set}
{B : Γ → Set}
(w : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(x : Γ) (u : [ Φ x ]) → A (x , u) ≅' Glue Φ A B w x
abstract
fIso Φ {A} {B} w x u = iso where
open _≅'_
prfIr : {a : A (x , u)} → subst (λ v → A (x , v)) (equ (fst (Φ x)) u u) a ≡ a
prfIr {a} =
let switch = uip (equ (fst (Φ x)) u u) refl in
cong (λ p → subst (λ v → A (x , v)) p a) switch
iso : A (x , u) ≅' Glue Φ A B w x
f iso a = glue {Φ = Φ} w (x , u) a
g iso (a , _ , _) = a u
inv₁ iso = funext (λ a → prfIr)
inv₂ iso = funext fg≡id where
parEq : {a a' : (u : [ Φ x ]) → A (x , u)} → a u ≡ a' u → a ≡ a'
parEq {a} {a'} eq = funext (λ v → subst (λ v → a v ≡ a' v) (equ (fst (Φ x)) u v) eq)
fg≡id : (gl : Glue Φ A B w x) → (glue {Φ = Φ} w (x , u) (fst gl u)) ≡ gl
fg≡id gl = glueExt {Φ = Φ} w (glue {Φ = Φ} w (x , u) (fst gl u)) gl fstEq sndEq where
fstEq : fst (glue {Φ = Φ} w (x , u) (fst gl u)) ≡ fst gl
fstEq = parEq prfIr
sndEq : w x u (fst gl u) ≡ fst (snd gl)
sndEq = snd (snd gl) u

SGlue {Γ} Φ A B w = strictify Φ A (Glue Φ A B w) (fIso Φ w)

sglue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(w : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(xu : res Γ Φ) → A xu → SGlue Φ A B w (fst xu)
abstract
sglue {Γ} {Φ} {A} {B} w (x , u) = (_≅'_.g iso) ∘ glue {Φ = Φ} w (x , u) where
iso : SGlue Φ A B w x ≅' Glue Φ A B w x
iso = isoB Φ A (Glue Φ A B w) (fIso Φ w) x

sunglue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(w : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
→ ---------------
(x : Γ) → SGlue Φ A B w x → B x
abstract
sunglue {Γ} {Φ} {A} {B} w x = (unglue {Φ = Φ} w x) ∘ _≅'_.f iso where
iso : SGlue Φ A B w x ≅' Glue Φ A B w x
iso = isoB Φ A (Glue Φ A B w) (fIso Φ w) x

FibSGlue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
(equiv : (x : Γ)(v : [ Φ x ]) → Equiv (f x v))
→ ---------------
Fib A → Fib B → Fib (SGlue Φ A B f)
abstract
FibSGlue {Γ} {Φ} {A} {B} f equiv α β =
FibIso (Glue Φ A B f) (SGlue Φ A B f) iso (FibGlue {Φ = Φ} f equiv α β) where
iso : Glue Φ A B f ≅ SGlue Φ A B f
iso x = (_≅'_.g iso' , _≅'_.f iso' , (_≅'_.inv₂ iso' , _≅'_.inv₁ iso')) where
iso' : SGlue Φ A B f x ≅' Glue Φ A B f x
iso' = isoB Φ A (Glue Φ A B f) (fIso Φ f) x

strictness :
{Γ : Set}
(Φ : Γ → Cof)
(A : res Γ Φ → Set)
(B : Γ → Set)
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
(x : Γ)
(u : [ Φ x ])
→ ---------------
SGlue Φ A B f x ≡ A (x , u)
abstract
strictness Φ A B f x u = symm (restrictsToA Φ A (Glue Φ A B f) (fIso Φ f) (x , u))

str :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
(x : Γ)
→ ---------------
Glue Φ A B f x → SGlue Φ A B f x
abstract
str {Γ} {Φ} {A} {B} f x = _≅'_.g (isoB Φ A (Glue Φ A B f) (fIso Φ f) x)

unstr :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
(x : Γ)
→ ---------------
SGlue Φ A B f x → Glue Φ A B f x
abstract
unstr {Γ} {Φ} {A} {B} f x = _≅'_.f (isoB Φ A (Glue Φ A B f) (fIso Φ f) x)

strIsUnglue :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
(x : Γ)
(u : [ Φ x ])
→ ---------------
(g : Glue Φ A B f x) → str {Γ} {Φ} {A} {B} f x g ≡ coe (symm (strictness Φ A B f x u)) (fst g u)
abstract
strIsUnglue {Γ} {Φ} {A} {B} f x u g = inner (restrictsToM Φ A (Glue Φ A B f) (fIso Φ f) x u) g where
inner : {Am Gs : Σ X ∈ Set , X ≅' Glue Φ A B f x}(eq : Am ≡ Gs)(g : Glue Φ A B f x) → _≅'_.g (snd Gs) g ≡ coe (symm (symm (Σeq₁ eq))) (_≅'_.g (snd Am) g)
inner refl b = refl

unstrStr :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
(x : Γ)
→ ---------------
(unstr {Γ} {Φ} {A} {B} f x) ∘ (str {Γ} {Φ} {A} {B} f x) ≡ id
abstract
unstrStr {Γ} {Φ} {A} {B} f x = _≅'_.inv₂ (isoB Φ A (Glue Φ A B f) (fIso Φ f) x)

strUnstr :
{Γ : Set}
{Φ : Γ → Cof}
{A : res Γ Φ → Set}
{B : Γ → Set}
(f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
(x : Γ)
→ ---------------
(str {Γ} {Φ} {A} {B} f x) ∘ (unstr {Γ} {Φ} {A} {B} f x) ≡ id
abstract
strUnstr {Γ} {Φ} {A} {B} f x = _≅'_.inv₁ (isoB Φ A (Glue Φ A B f) (fIso Φ f) x)
```