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

open import Data.Nat using (_+_)
open import Level using (Lift ; lift ; lower)

open import Util.Prelude
open import Util.Relation.Binary.LogicalEquivalence using (_↔_ ; forth ; back)
open import Util.Relation.Binary.PropositionalEquality using
( Σ-≡⁺ ; Σ-≡⁻ ; Σ-≡⁺∘Σ-≡⁻ ; trans-injectiveˡ )

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

IsContr : Set α → Set α
IsContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

IsProp : Set α → Set α
IsProp A = (x y : A) → x ≡ y

IsProp′ : Set α → Set α
IsProp′ A = (x y : A) → IsContr (x ≡ y)

IsProp→IsProp′ : IsProp A → IsProp′ A
IsProp→IsProp′ {A = A} A-prop x y = (A-prop x y) , canon
where
go : (p : x ≡ y) → trans p (A-prop y y) ≡ A-prop x y
go refl = refl

canon : (p : x ≡ y) → A-prop x y ≡ p
canon refl = trans-injectiveˡ (A-prop y y) (go (A-prop y y))

IsProp′→IsProp : IsProp′ A → IsProp A
IsProp′→IsProp A-prop x y = proj₁ (A-prop x y)

IsProp↔IsProp′ : IsProp A ↔ IsProp′ A
IsProp↔IsProp′ .forth = IsProp→IsProp′
IsProp↔IsProp′ .back = IsProp′→IsProp

IsSet : Set α → Set α
IsSet A = {x y : A} → IsProp (x ≡ y)

IsOfHLevel : ℕ → Set α → Set α
IsOfHLevel 0 A = IsContr A
IsOfHLevel 1 A = IsProp A
IsOfHLevel (suc (suc n)) A = {x y : A} → IsOfHLevel (suc n) (x ≡ y)

IsOfHLevel′ : ℕ → Set α → Set α
IsOfHLevel′ zero A = IsContr A
IsOfHLevel′ (suc n) A = ∀ {x y : A} → IsOfHLevel′ n (x ≡ y)

IsOfHLevel′→IsOfHLevel : ∀ n → IsOfHLevel′ n A → IsOfHLevel n A
IsOfHLevel′→IsOfHLevel zero A-contr = A-contr
IsOfHLevel′→IsOfHLevel (suc zero) A-prop = IsProp′→IsProp λ _ _ → A-prop
IsOfHLevel′→IsOfHLevel (suc (suc n)) A-level
= IsOfHLevel′→IsOfHLevel (suc n) A-level

IsOfHLevel→IsOfHLevel′ : ∀ n → IsOfHLevel n A → IsOfHLevel′ n A
IsOfHLevel→IsOfHLevel′ zero A-contr = A-contr
IsOfHLevel→IsOfHLevel′ (suc zero) A-prop = IsProp→IsProp′ A-prop _ _
IsOfHLevel→IsOfHLevel′ (suc (suc n)) A-level
= IsOfHLevel→IsOfHLevel′ (suc n) A-level

IsOfHLevel↔IsOfHLevel′ : ∀ n → IsOfHLevel n A ↔ IsOfHLevel′ n A
IsOfHLevel↔IsOfHLevel′ n .forth = IsOfHLevel→IsOfHLevel′ n
IsOfHLevel↔IsOfHLevel′ n .back = IsOfHLevel′→IsOfHLevel n

IsContr→IsProp : IsContr A → IsProp A
IsContr→IsProp (c , c-canon) x y = trans (sym (c-canon x)) (c-canon y)

IsOfHLevel-suc : ∀ n → IsOfHLevel n A → IsOfHLevel (suc n) A
IsOfHLevel-suc 0 A-contr = IsContr→IsProp A-contr
IsOfHLevel-suc 1 A-prop = IsOfHLevel-suc 0 (IsProp→IsProp′ A-prop _ _)
IsOfHLevel-suc (suc (suc n)) A-level-n = IsOfHLevel-suc (suc n) A-level-n

IsOfHLevel-suc-n : ∀ n m → IsOfHLevel n A → IsOfHLevel (m + n) A
IsOfHLevel-suc-n {A = A} n zero A-level = A-level
IsOfHLevel-suc-n n (suc m) A-level
= IsOfHLevel-suc (m + n) (IsOfHLevel-suc-n n m A-level)

IsProp→IsSet : IsProp A → IsSet A
IsProp→IsSet = IsOfHLevel-suc 1

IsContr→IsSet : IsContr A → IsSet A
IsContr→IsSet = IsOfHLevel-suc-n 0 2

record HLevel α n : Set (lsuc α) where
constructor HLevel⁺
field
type : Set α
level : IsOfHLevel n type

open HLevel public

HContr : ∀ α → Set (lsuc α)
HContr α = HLevel α 0

HProp : ∀ α → Set (lsuc α)
HProp α = HLevel α 1

HSet : ∀ α → Set (lsuc α)
HSet α = HLevel α 2

HLevel-suc : ∀ {α n} → HLevel α n → HLevel α (suc n)
HLevel-suc (HLevel⁺ A A-level) = HLevel⁺ A (IsOfHLevel-suc _ A-level)

⊤-IsContr : IsContr ⊤
⊤-IsContr = ⊤.tt , λ { ⊤.tt → refl }

⊤-IsProp : IsProp ⊤
⊤-IsProp = IsOfHLevel-suc 0 ⊤-IsContr

⊥-IsProp : IsProp ⊥
⊥-IsProp ()

×-IsProp : IsProp A → IsProp B → IsProp (A × B)
×-IsProp A-prop B-prop (x , y) (x′ , y′) = cong₂ _,_ (A-prop _ _) (B-prop _ _)

Lift-IsProp : IsProp A → IsProp (Lift α A)
Lift-IsProp A-prop (lift x) (lift y) = cong lift (A-prop _ _)

⊤-HProp : HProp 0ℓ
⊤-HProp = HLevel⁺ ⊤ ⊤-IsProp

⊥-HProp : HProp 0ℓ
⊥-HProp = HLevel⁺ ⊥ ⊥-IsProp

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

Lift-HProp : ∀ α → HProp β → HProp (α ⊔ℓ β)
Lift-HProp α (HLevel⁺ A A-prop) = HLevel⁺ (Lift α A) (Lift-IsProp A-prop)

⊤-IsSet : IsSet ⊤
⊤-IsSet = IsOfHLevel-suc 1 ⊤-IsProp

⊥-IsSet : IsSet ⊥
⊥-IsSet = IsOfHLevel-suc 1 ⊥-IsProp

Σ-IsSet : {A : Set α} {B : A → Set β}
→ IsSet A
→ (∀ a → IsSet (B a))
→ IsSet (Σ A B)
Σ-IsSet A-set B-set p q
= trans (sym (Σ-≡⁺∘Σ-≡⁻ p))
(sym (trans (sym (Σ-≡⁺∘Σ-≡⁻ q))
(cong Σ-≡⁺ (Σ-≡⁺ (A-set _ _ , B-set _ _ _)))))

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

Lift-IsSet : IsSet A → IsSet (Lift α A)
Lift-IsSet A-set p q
= trans (sym (Lift-≡⁺∘Lift-≡⁻ p))
(sym (trans (sym (Lift-≡⁺∘Lift-≡⁻ q)) (cong Lift-≡⁺ (A-set _ _))))
where
Lift-≡⁻ : {x y : Lift α A} → x ≡ y → lower x ≡ lower y
Lift-≡⁻ refl = refl

Lift-≡⁺ : {x y : Lift α A} → lower x ≡ lower y → x ≡ y
Lift-≡⁺ refl = refl

Lift-≡⁻∘Lift-≡⁺ : {x y : Lift α A} (p : lower x ≡ lower y)
→ Lift-≡⁻ {α = α} (Lift-≡⁺ p) ≡ p
Lift-≡⁻∘Lift-≡⁺ refl = refl

Lift-≡⁺∘Lift-≡⁻ : {x y : Lift α A} (p : x ≡ y)
→ Lift-≡⁺ {α = α} (Lift-≡⁻ p) ≡ p
Lift-≡⁺∘Lift-≡⁻ refl = refl

⊤-HSet : HSet 0ℓ
⊤-HSet = HLevel⁺ ⊤ ⊤-IsSet

⊥-HSet : HSet 0ℓ
⊥-HSet = HLevel⁺ ⊥ ⊥-IsSet

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

_×-HSet_ : HSet α → HSet β → HSet (α ⊔ℓ β)
A ×-HSet B = HLevel⁺ (A .type × B .type) (×-IsSet (A .level) (B .level))

Lift-HSet : ∀ α → HSet β → HSet (α ⊔ℓ β)
Lift-HSet α (HLevel⁺ B B-set) = HLevel⁺ (Lift α B) (Lift-IsSet B-set)

IsProp∧Pointed→IsContr : IsProp A → (a : A) → IsContr A
IsProp∧Pointed→IsContr A-prop a = a , λ b → A-prop a b
```