{-# OPTIONS --without-K #-}
module hott.hlevel.closure where

open import level
open import decidable
open import sum
open import level using (lsuc; ↑; lift)
open import equality.core
open import equality.calculus
open import function using (_∘_; const)
open import function.extensionality
open import function.isomorphism
open import sets.bool
open import sets.unit
open import sets.nat.core using (ℕ; suc; _≤_)
open import hott.hlevel.core
open import hott.hlevel.sets using (⊤-contr; bool-set)
open import hott.hlevel.properties
open import hott.weak-equivalence.core
  using (weak-equiv; _≈_)
open import hott.univalence

abstract
  -- Π preserves h-levels
  Π-hlevel : ∀ {i j n} {X : Set i}{Y : X → Set j}
           → ((x : X) → h n (Y x))
           → h n ((x : X) → Y x)
  Π-hlevel {n = } c = Π-contr c
  Π-hlevel {n = suc n} {X = X}{Y} hn = λ f g →
    subst (h n) strong-ext (Π-hlevel (λ x → hn x (f x) (g x)))

  -- Σ preserves h-levels
  Σ-hlevel : ∀ {i j n} {X : Set i}{Y : X → Set j}
           → h n X → ((x : X) → h n (Y x))
           → h n (Σ X Y)
  Σ-hlevel {n = }{X = X}{Y} (x₀ , cx) hy =
    (x₀ , proj₁ (hy x₀)) , λ { (x , y) → c x y }
    where
      c : (x : X)(y : Y x) → (x₀ , proj₁ (hy x₀)) ≡ (x , y)
      c x y = cong (λ x → (x , proj₁ (hy x))) (cx x)
            ⊚ cong (_,_ x) (proj₂ (hy x) y)
  Σ-hlevel {n = suc n} hx hy = λ a b → iso-hlevel Σ-split-iso
    (Σ-hlevel (hx _ _) (λ p → hy (proj₁ b) _ _))

  -- × preserves h-levels
  ×-hlevel : ∀ {i j n}{X : Set i}{Y : Set j}
           → h n X → h n Y → h n (X × Y)
  ×-hlevel hx hy = Σ-hlevel hx (λ _ → hy)

  -- ⊎ preserves h-levels
  ⊎-hlevel : ∀ {i j n}{X : Set i}{Y : Set j}
           →  ≤ n → h n X → h n Y → h n (X ⊎ Y)
  ⊎-hlevel {i}{j}{n} {X}{Y} p hx hy = iso-hlevel lem
    (Σ-hlevel (h! {p = decide p} bool-set) P-hlevel)
    where
      P : Bool → Set (i ⊔ j)
      P true = ↑ j X
      P false = ↑ i Y

      P-hlevel : (b : Bool) → h n (P b)
      P-hlevel true = iso-hlevel (lift-iso j X) hx
      P-hlevel false = iso-hlevel (lift-iso i Y) hy

      lem : Σ Bool P ≅ (X ⊎ Y)
      lem = iso f g H K
        where
          f : (Σ Bool P) → (X ⊎ Y)
          f (true , lift x) = inj₁ x
          f (false , lift y) = inj₂ y

          g : (X ⊎ Y) → (Σ Bool P)
          g (inj₁ x) = (true , lift x)
          g (inj₂ y) = (false , lift y)

          H : (x : Σ Bool P) → g (f x) ≡ x
          H (true , lift x) = refl
          H (false , lift y) = refl

          K : (x : X ⊎ Y) → f (g x) ≡ x
          K (inj₁ x) = refl
          K (inj₂ y) = refl

  Π-hlevel-impl : ∀ {i j n} {X : Set i}{Y : X → Set j}
                → ((x : X) → h n (Y x))
                → h n ({x : X} → Y x)
  Π-hlevel-impl {X = X}{Y} hY = iso-hlevel impl-iso (Π-hlevel hY)

  -- being contractible is a proposition
  contr-h1 : ∀ {i}(X : Set i) → h  (contr X)
  contr-h1 X = prop⇒h1 λ { (x₀ , c₀) (x₁ , c₁) →
      uncongΣ (c₀ x₁ , contr⇒prop (lem (x₀ , c₀) x₁) _ _) }
    where
      lem : ∀ {i}{A : Set i} → contr A → (x : A) → contr ((x' : A) → x ≡ x')
      lem c x = Π-hlevel (λ x' → h↑ c x x')

  -- being of h-level n is a proposition
  hn-h1 : ∀ {i} n (X : Set i) → h  (h n X)
  hn-h1  X = contr-h1 X
  hn-h1 (suc n) X = Π-hlevel λ x → Π-hlevel λ y → hn-h1 n (x ≡ y)

  -- being a weak equivalence is a proposition
  weak-equiv-h1 : ∀ {i j}{X : Set i}{Y : Set j}
                → (f : X → Y)
                → h  (weak-equiv f)
  weak-equiv-h1 f = Π-hlevel λ y
                  → contr-h1 _