{-# 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