-- This module closely follows a section of Martín Escardó's HoTT lecture notes:
-- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#unicharac
{-# OPTIONS --without-K #-}
module Util.HoTT.Univalence.ContrFormulation where

open import Util.Data.Product using (map₂)
open import Util.Prelude
open import Util.HoTT.Equiv
open import Util.HoTT.HLevel.Core
open import Util.HoTT.Singleton
open import Util.HoTT.Univalence.Axiom
open import Util.HoTT.Univalence.Statement


private
  variable
    α β γ : Level


UnivalenceContr : ∀ α → Set (lsuc α)
UnivalenceContr α = (A : Set α) → IsContr (Σ[ B ∈ Set α ] (A ≃ B))


UnivalenceProp : ∀ α → Set (lsuc α)
UnivalenceProp α = (A : Set α) → IsProp (Σ[ B ∈ Set α ] (A ≃ B))


abstract
  IsEquiv→Σ-IsContr : {A : Set α} {B : A → Set β} (x : A)
    → (f : ∀ y → x ≡ y → B y)
    → (∀ y → IsEquiv (f y))
    → IsContr (Σ A B)
  IsEquiv→Σ-IsContr {A = A} {B = B} x f f-equiv
    = ≃-pres-IsContr Singleton≃ΣB IsContr-Singleton′
    where
      ≡≃B : ∀ y → (x ≡ y) ≃ B y
      ≡≃B y .forth = f y
      ≡≃B y .isEquiv = f-equiv y

      Singleton≃ΣB : Singleton′ x ≃ Σ A B
      Singleton≃ΣB = Σ-≃⁺ ≡≃B


  Σ-IsContr→IsEquiv : {A : Set α} {B : A → Set β} (x : A)
    → (f : ∀ y → x ≡ y → B y)
    → IsContr (Σ A B)
    → ∀ y → IsEquiv (f y)
  Σ-IsContr→IsEquiv {A = A} {B = B} x f Σ-contr
    = IsEquiv-map₂-f→IsEquiv-f f f-equiv
    where
      f-equiv : IsEquiv (map₂ f)
      f-equiv = IsContr→IsEquiv IsContr-Singleton′ Σ-contr (map₂ f)


  Univalence→UnivalenceContr : Univalence α → UnivalenceContr α
  Univalence→UnivalenceContr ua A = IsEquiv→Σ-IsContr A (λ B → ≡→≃) (λ B → ua)


  UnivalenceContr→Univalence : UnivalenceContr α → Univalence α
  UnivalenceContr→Univalence ua {A} {B}
    = Σ-IsContr→IsEquiv A (λ B → ≡→≃) (ua A) B


  univalenceContr : (A : Set α) → IsContr (Σ[ B ∈ Set α ] (A ≃ B))
  univalenceContr = Univalence→UnivalenceContr univalence


  UnivalenceContr→UnivalenceProp : UnivalenceContr α → UnivalenceProp α
  UnivalenceContr→UnivalenceProp ua = IsContr→IsProp ∘ ua


  UnivalenceProp→UnivalenceContr : UnivalenceProp α → UnivalenceContr α
  UnivalenceProp→UnivalenceContr ua A
    = IsProp∧Pointed→IsContr (ua A) (A , ≃-refl)


  Univalence→UnivalenceProp : Univalence α → UnivalenceProp α
  Univalence→UnivalenceProp
    = UnivalenceContr→UnivalenceProp ∘ Univalence→UnivalenceContr


  UnivalenceProp→Univalence : UnivalenceProp α → Univalence α
  UnivalenceProp→Univalence
    = UnivalenceContr→Univalence ∘ UnivalenceProp→UnivalenceContr


  univalenceProp : ∀ {α} → UnivalenceProp α
  univalenceProp = Univalence→UnivalenceProp univalence