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