```{-# OPTIONS --without-K #-}

module display where

open import level
open import sum
open import equality
open import function.core
open import function.isomorphism
open import function.extensionality
open import sets.unit
open import hott.hlevel.core
open import hott.weak-equivalence
open import hott.univalence

-- correspondence between dependent types and display maps

-- fix an index set I
module Display {i} (I : Set i) where
Fibration : Set (lsuc i)
Fibration = Σ (Set i) λ X → X → I

Family : Set (lsuc i)
Family = I → Set i

total : Family → Set i
total X = Σ I X

fibration : (X : Family) → total X → I
fibration X = proj₁

family : {X : Set i} → (X → I) → I → Set i
family p i = p ⁻¹ i

iso₁ : (X : I → Set i) → ∀ i → family (fibration X) i ≅ X i
iso₁ X i = begin
Σ (total X) (λ {(j , _) → j ≡ i})
≅⟨ Σ-assoc-iso ⟩
Σ I (λ j → Σ (X j) λ _ → j ≡ i)
≅⟨ Σ-cong-iso refl≅ (λ _ → ×-comm) ⟩
Σ I (λ j → Σ (j ≡ i) λ _ → X j)
≅⟨ Σ-cong-iso refl≅ (λ j →
Σ-cong-iso refl≅ λ p → ≡⇒≅ (cong X p)) ⟩
Σ I (λ j → Σ (j ≡ i) λ _ → X i)
≅⟨ sym≅ (Σ-assoc-iso) ⟩
(Σ I (λ j → j ≡ i) × X i)
≅⟨ Σ-cong-iso (Σ-cong-iso refl≅ λ j → sym≡-iso j i)
(λ _ → refl≅) ⟩
(Σ I (λ j → i ≡ j) × X i)
≅⟨ Σ-cong-iso (contr-⊤-iso (singl-contr i))
(λ i → refl≅) ⟩
(⊤ × X i)
≅⟨ ×-left-unit ⟩
X i
∎
where
open ≅-Reasoning

iso-total : {X : Set i} (p : X → I) → total (family p) ≅ X
iso-total {X} p = begin
total (family p)
≅⟨ sym≅ Σ-assoc-iso ⟩
Σ (I × X) (λ {(i , x) → p x ≡ i })
≅⟨ Σ-cong-iso ×-comm (λ _ → refl≅) ⟩
Σ (X × I) (λ {(x , i) → p x ≡ i })
≅⟨ Σ-assoc-iso ⟩
Σ X (λ x → singleton (p x))
≅⟨ Σ-cong-iso refl≅
(λ x → contr-⊤-iso (singl-contr (p x))) ⟩
(X × ⊤)
≅⟨ ×-right-unit ⟩
X
∎
where open ≅-Reasoning

iso₂ : {X : Set i} (p : X → I) → ∀ x
→ fibration (family p) (invert (iso-total p) x)
≡ p x
iso₂ p x = refl

fam-fib-iso : Family ≅ Fibration
fam-fib-iso = record
{ to = λ X → total X , fibration X
; from = λ {(X , p) → family p }
; iso₁ = λ X → ext' λ i → ≅⇒≡ (iso₁ X i)
; iso₂ = λ {(X , p) → lem (iso-total p , ext (iso₂ p))  } }
where
lem : {A B : Fibration}
→ let (X , f) = A
(Y , g) = B
in Σ (X ≅ Y) (λ p → f ∘ invert p ≡ g)
→ (A ≡ B)
lem {X , f} {Y , g} (isom , q) =
uncongΣ (p , lem-subst p f ⊚ cong (λ h → f ∘ h) p-β ⊚ q)
where
abstract
w : X ≈ Y
w = ≅⇒≈ isom

p : X ≡ Y
p = ≈⇒≡ w

p-β : coerce (sym p) ≡ invert isom
p-β = begin
coerce (sym (≈⇒≡ w))
≡⟨ cong coerce (univ-sym≈ w) ⟩
coerce (≈⇒≡ (sym≈ w))
≡⟨ uni-coherence (sym≈ w) ⟩
invert isom
∎
where open ≡-Reasoning

lem-subst : {X Y : Set i}
→ (p : X ≡ Y)
→ (f : X → I)
→ subst (λ Z → Z → I) p f
≡ f ∘ coerce (sym p)
lem-subst refl f = refl
```