```{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness #-}
module Agda.Builtin.Cubical.Glue where

open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
primHComp to hcomp; primTransp to transp; primComp to comp;
itIsOne to 1=1)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to ouc)

module Helpers where
-- Homogeneous filling
hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
(u : ∀ i → Partial φ A)
(u0 : A [ φ ↦ u i0 ]) (i : I) → A
hfill {φ = φ} u u0 i =
hcomp (λ j → \ { (φ = i1) → u (i ∧ j) 1=1
; (i = i0) → ouc u0 })
(ouc u0)

-- Heterogeneous filling defined using comp
fill : ∀ {ℓ : I → Level} (A : ∀ i → Set (ℓ i)) {φ : I}
(u : ∀ i → Partial φ (A i))
(u0 : A i0 [ φ ↦ u i0 ]) →
∀ i →  A i
fill A {φ = φ} u u0 i =
comp (λ j → A (i ∧ j)) _
(λ j → \ { (φ = i1) → u (i ∧ j) 1=1
; (i = i0) → ouc u0 })
(ouc {φ = φ} u0)

module _ {ℓ} {A : Set ℓ} where
refl : {x : A} → x ≡ x
refl {x = x} = λ _ → x

sym : {x y : A} → x ≡ y → y ≡ x
sym p = λ i → p (~ i)

cong : ∀ {ℓ'} {B : A → Set ℓ'} {x y : A}
(f : (a : A) → B a) (p : x ≡ y)
→ PathP (λ i → B (p i)) (f x) (f y)
cong f p = λ i → f (p i)

isContr : ∀ {ℓ} → Set ℓ → Set ℓ
isContr A = Σ A \ x → (∀ y → x ≡ y)

fiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ ⊔ ℓ')
fiber {A = A} f y = Σ A \ x → f x ≡ y

open Helpers

-- We make this a record so that isEquiv can be proved using
-- copatterns. This is good because copatterns don't get unfolded
-- unless a projection is applied so it should be more efficient.
record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
no-eta-equality
field
equiv-proof : (y : B) → isContr (fiber f y)

open isEquiv public

infix 4 _≃_

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) \ f → (isEquiv f)

equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B
equivFun e = fst e

-- Improved version of equivProof compared to Lemma 5 in CCHM. We put
-- the (φ = i0) face in contr' making it be definitionally c in this
-- case. This makes the computational behavior better, in particular
-- for transp in Glue.
equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A)
→ ∀ ψ → (Partial ψ (fiber (w .fst) a)) → fiber (w .fst) a
equivProof A B w a ψ fb = contr' {A = fiber (w .fst) a} (w .snd .equiv-proof a) ψ fb
where
contr' : ∀ {ℓ} {A : Set ℓ} → isContr A → (φ : I) → (u : Partial φ A) → A
contr' {A = A} (c , p) φ u = hcomp (λ i → λ { (φ = i1) → p (u 1=1) i
; (φ = i0) → c }) c

{-# BUILTIN EQUIV      _≃_        #-}
{-# BUILTIN EQUIVFUN   equivFun   #-}
{-# BUILTIN EQUIVPROOF equivProof #-}

primitive
primGlue    : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
→ (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
→ Set ℓ'
prim^glue   : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
→ {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
→ (t : PartialP φ T) → (a : A) → primGlue A T e
prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
→ {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
→ primGlue A T e → A

-- Needed for transp in Glue.
primFaceForall : (I → I) → I

module _ {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) where
private
E : (i : I) → Set (ℓ i)
E  = λ i → P i
~E : (i : I) → Set (ℓ (~ i))
~E = λ i → P (~ i)

A = P i0
B = P i1

f : A → B
f x = transp E i0 x

g : B → A
g y = transp ~E i0 y

u : ∀ i → A → E i
u i x = transp (λ j → E (i ∧ j)) (~ i) x

v : ∀ i → B → E i
v i y = transp (λ j → ~E ( ~ i ∧ j)) i y

fiberPath : (y : B) → (xβ0 xβ1 : fiber f y) → xβ0 ≡ xβ1
fiberPath y (x0 , β0) (x1 , β1) k = ω , λ j → δ (~ j) where
module _ (j : I) where
private
sys : A → ∀ i → PartialP (~ j ∨ j) (λ _ → E (~ i))
sys x i (j = i0) = v (~ i) y
sys x i (j = i1) = u (~ i) x
ω0 = comp ~E _ (sys x0) ((β0 (~ j)))
ω1 = comp ~E _ (sys x1) ((β1 (~ j)))
θ0 = fill ~E (sys x0) (inc (β0 (~ j)))
θ1 = fill ~E (sys x1) (inc (β1 (~ j)))
sys = λ {j (k = i0) → ω0 j ; j (k = i1) → ω1 j}
ω = hcomp sys (g y)
θ = hfill sys (inc (g y))
δ = λ (j : I) → comp E _
(λ i → λ { (j = i0) → v i y ; (k = i0) → θ0 j (~ i)
; (j = i1) → u i ω ; (k = i1) → θ1 j (~ i) })
(θ j)

γ : (y : B) → y ≡ f (g y)
γ y j = comp E _ (λ i → λ { (j = i0) → v i y
; (j = i1) → u i (g y) }) (g y)

pathToisEquiv : isEquiv f
pathToisEquiv .equiv-proof y .fst .fst = g y
pathToisEquiv .equiv-proof y .fst .snd = sym (γ y)
pathToisEquiv .equiv-proof y .snd = fiberPath y _

pathToEquiv : A ≃ B
pathToEquiv .fst = f
pathToEquiv .snd = pathToisEquiv

{-# BUILTIN PATHTOEQUIV pathToEquiv #-}
```