{-# OPTIONS --without-K #-}
module Util.HoTT.HLevel where

open import Util.HoTT.HLevel.Core public

open import Util.HoTT.Equiv
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.Homotopy
open import Util.HoTT.Univalence.Axiom
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁺ ; Σ-≡⁻ ; Σ-≡⁺∘Σ-≡⁻ )
open import Util.Relation.Binary.LogicalEquivalence


private
  variable
    α β γ : Level
    A B C : Set α


infixr  _→-HProp_


-- Note that A and B must be at the same level. A more direct proof could
-- probably avoid this.
≃-pres-IsOfHLevel : ∀ {A B : Set α} n → A ≃ B → IsOfHLevel n A → IsOfHLevel n B
≃-pres-IsOfHLevel n A≃B = subst (IsOfHLevel n) (≃→≡ A≃B)


≅-pres-IsOfHLevel : ∀ {A B : Set α} n → A ≅ B → IsOfHLevel n A → IsOfHLevel n B
≅-pres-IsOfHLevel n A≅B = ≃-pres-IsOfHLevel n (≅→≃ A≅B)


∀-IsProp : {B : A → Set β} → (∀ a → IsProp (B a)) → IsProp (∀ a → B a)
∀-IsProp B-prop f g = funext λ a → B-prop _ _ _


∀∙-IsProp : {B : A → Set β} → (∀ a → IsProp (B a)) → IsProp (∀ {a} → B a)
∀∙-IsProp B-prop f g = funext∙ (B-prop _ _ _)


→-IsProp : IsProp B → IsProp (A → B)
→-IsProp B-prop = ∀-IsProp λ _ → B-prop


∀-HProp : (A : Set α) → ((a : A) → HProp β) → HProp (α ⊔ℓ β)
∀-HProp A B = HLevel⁺ (∀ a → B a .type) (∀-IsProp (λ a → B a .level))


∀∙-HProp : {A : Set α} → ((a : A) → HProp β) → HProp (α ⊔ℓ β)
∀∙-HProp B = HLevel⁺ (∀ {a} → B a .type) (∀∙-IsProp (λ a → B a .level))


_→-HProp_ : Set α → HProp β → HProp (α ⊔ℓ β)
A →-HProp B = HLevel⁺ (A → B .type) (→-IsProp (B .level))


_→-HProp′_ : HProp α → HProp β → HProp (α ⊔ℓ β)
A →-HProp′ B = A .type →-HProp B


IsContr-IsProp : IsProp (IsContr A)
IsContr-IsProp (x , x-unique) (y , y-unique)
  = Σ-≡⁺ (x-unique y , eq-prop _ _)
  where
  eq-prop : IsProp (∀ y′ → y ≡ y′)
  eq-prop = ∀-IsProp λ γ′ → IsOfHLevel-suc  (IsOfHLevel-suc  (x , x-unique))


IsProp-IsProp : IsProp (IsProp A)
IsProp-IsProp A-prop A-prop′
  = ∀-IsProp (λ x → ∀-IsProp λ y → IsOfHLevel-suc  A-prop) A-prop A-prop′


IsOfHLevel-IsProp : ∀ n → IsProp (IsOfHLevel n A)
IsOfHLevel-IsProp {A = A} zero = IsContr-IsProp
IsOfHLevel-IsProp (suc zero) = IsProp-IsProp
IsOfHLevel-IsProp (suc (suc n))
  = ∀∙-IsProp λ x → ∀∙-IsProp λ y → IsOfHLevel-IsProp (suc n)


IsSet-IsProp : IsProp (IsSet A)
IsSet-IsProp = IsOfHLevel-IsProp 


∀-IsSet : {A : Set α} {B : A → Set β}
  → (∀ a → IsSet (B a))
  → IsSet (∀ a → B a)
∀-IsSet B-set {f} {g} p q = let open ≡-Reasoning in
  begin
    p
  ≡˘⟨ funext∘≡→~ p ⟩
    funext (≡→~ p)
  ≡⟨ cong funext (funext λ a → B-set a (≡→~ p a) (≡→~ q a)) ⟩
    funext (≡→~ q)
  ≡⟨ funext∘≡→~ q ⟩
    q
  ∎


∀∙-IsSet : {A : Set α} {B : A → Set β}
  → (∀ a → IsSet (B a))
  → IsSet (∀ {a} → B a)
∀∙-IsSet {A = A} {B = B} B-set = ≅-pres-IsOfHLevel  iso (∀-IsSet B-set)
  where
    iso : (∀ a → B a) ≅ (∀ {a} → B a)
    iso = record
      { forth = λ f {a} → f a
      ; isIso = record
        { back = λ f a → f {a}
        ; back∘forth = λ _ → refl
        ; forth∘back = λ _ → refl
        }
      }


→-IsSet : IsSet B → IsSet (A → B)
→-IsSet B-set = ∀-IsSet (λ _ → B-set)


∀-HSet : (A : Set α) → (A → HSet β) → HSet (α ⊔ℓ β)
∀-HSet A B = HLevel⁺ (∀ a → B a .type) (∀-IsSet (λ a → B a .level))


∀∙-HSet : {A : Set α} → (A → HSet β) → HSet (α ⊔ℓ β)
∀∙-HSet B = HLevel⁺ (∀ {a} → B a .type) (∀∙-IsSet (λ a → B a .level))


HLevel-≡⁺ : ∀ {n} (A B : HLevel α n)
  → A .type ≡ B .type
  → A ≡ B
HLevel-≡⁺ (HLevel⁺ A A-level) (HLevel⁺ B B-level) refl
  = cong (HLevel⁺ A) (IsOfHLevel-IsProp _ _ _)


IsContr-≅⁺ : IsContr A → IsContr B → A ≅ B
IsContr-≅⁺ (a , a-uniq) (b , b-uniq) = record
  { forth = λ _ → b
  ; isIso = record
    { back = λ _ → a
    ; back∘forth = λ _ → a-uniq _
    ; forth∘back = λ _ → b-uniq _
    }
  }


HContr-≡⁺ : (A B : HContr α) → A ≡ B
HContr-≡⁺ A B = HLevel-≡⁺ A B (≅→≡ (IsContr-≅⁺ (A .level) (B .level)))


IsProp-≅⁺ : IsProp A → IsProp B → A ↔ B → A ≅ B
IsProp-≅⁺ A-prop B-prop A↔B = record
  { forth = A↔B .forth
  ; isIso = record
    { back = A↔B .back
    ; back∘forth = λ _ → A-prop _ _
    ; forth∘back = λ _ → B-prop _ _
    }
  }


HProp-≡⁺ : (A B : HProp α) → A .type ↔ B .type → A ≡ B
HProp-≡⁺ A B A↔B = HLevel-≡⁺ A B (≅→≡ (IsProp-≅⁺ (A .level) (B .level) A↔B))