open import 1Lab.Prelude
  hiding
    ( ua
    ; univalence
    ; Fibration-equiv
    ; Map-classifier
    ; isContr-hContr )

module wip.objectclassifier where

variable
  ℓ ℓ' : Level
  A B C P : Type ℓ

χ : (A → B) → B → Type (level-of A ⊔ level-of B)
χ f x = fibre f x

θ : ∀ {ℓ ℓ'} {B : Type ℓ}
  → (Σ[ E ∈ Type (ℓ ⊔ ℓ') ] (E → B))
  → B → Type (ℓ ⊔ ℓ')
θ (E , p) = fibre p

postulate
  Fibration-equiv
    : ∀ {ℓ ℓ'} {B : Type ℓ}
    → isEquiv (θ {ℓ' = ℓ'} {B = B})
  
  Prop-ext : ∀ {ℓ} {A B : Type ℓ}
           → isProp A → isProp B
           → (A → B) → (B → A)
           → A ≡ B
  
Map-classifier
  : ∀ {ℓ ℓ' ℓ''} {B : Type ℓ'} (P : Type (ℓ ⊔ ℓ') → Type ℓ'')
  → (ℓ /[ P ] B) ≃ (B → Σ P)
Map-classifier {ℓ = ℓ} {B = B} P =
  (Σ[ A ∈ Type _ ] Σ[ f ∈ (A → B) ] ((x : B) → P (fibre f x)))       ≃⟨ Σ-assoc ⟩
  (Σ[ (x , f) ∈ Σ[ A ∈ Type _ ] (A → B) ] ((x : B) → P (fibre f x))) ≃⟨ Σ-ap-fst (θ {ℓ' = ℓ} , Fibration-equiv {ℓ' = ℓ}) ⟩
  (Σ[ A ∈ (B → Type _) ] ((x : B) → P (A x)))                        ≃⟨ Σ-Π-distrib e⁻¹ ⟩
  (B → Σ P)                                                          ≃∎

ua-helper : isContr (ℓ /[ isContr ] B)
ua-helper {ℓ = ℓ} = isHLevel≃  (Map-classifier {ℓ = ℓ} isContr e⁻¹) c
  where
    c = isHLevelΠ  λ x →
      contr (Lift _ ⊤ , contr (lift tt) λ _ → refl)
        λ e → Σ-Path
          (Prop-ext (λ _ _ → refl) (isContr→isProp (e .snd))
            (λ _ → e .snd .centre)
            λ _ → lift tt)
          (isProp-isContr _ _)

ua : ∀ {ℓ} {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B)
ua {ℓ = ℓ} {A = A} =
  pathToEquiv , total→equiv f
    where
      open isIso

      isom :  Iso (ℓ /[ isContr ] A) (Σ[ T ∈ Type ℓ ] T ≃ A)
      isom .fst (B , f , e) = B , f , record { isEqv = e }
      isom .snd .inv (B , f , e) = B , f , λ x → e .isEqv x
      isom .snd .rinv x = Σ-PathP refl (Σ-Path refl (isProp-isEquiv _ _ _))
      isom .snd .linv x = Σ-PathP refl (Σ-Path refl (isHLevelΠ  (λ _ → isProp-isContr) _ _))
      
      isom' : Iso (Σ (_≃ A)) (Σ (A ≃_))
      isom' .fst (X , e) = X , e e⁻¹
      isom' .snd .inv (X , e) = X , e e⁻¹
      isom' .snd .rinv _ = Σ-PathP refl (Σ-Path refl (isProp-isEquiv _ _ _))
      isom' .snd .linv _ = Σ-PathP refl (Σ-Path refl (isProp-isEquiv _ _ _))

      f : isEquiv (total {P = A ≡_} {Q = A ≃_} (λ _ → pathToEquiv))
      f = isContr→isEquiv
        (contr _ isContr-Singleton)
        (isHLevel≃  (Iso→Equiv isom ∙e Iso→Equiv isom') (ua-helper {ℓ = ℓ}))