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

open import level using (_⊔_; lsuc)
open import sum
open import sets.nat.core
open import equality.core
open import equality.groupoid
open import function.core using (_$_)

-- h-levels
h : ∀ {i} → ℕ → Set i → Set i
h  X = Σ X λ x → (x' : X) → x ≡ x'
h (suc n) X = (x x' : X) →  h n (x ≡ x')

-- a set is contractible if it has one element and everything in the
-- set is equal to that (h₀)
contr : ∀ {i} → Set i → Set i
contr = h 

-- a set is propositional if all elements are equal
prop : ∀ {i} → Set i → Set i
prop X = (x x' : X) → x ≡ x'

-- propositional and h1 are equivalent

-- (propositional says that all elements are equal and
--             h1 says that all elements are equal and
--                all equality proofs are equal)

h1⇒prop : ∀ {i} {X : Set i} → h  X → prop X
h1⇒prop h1 x x' = proj₁ $ h1 x x' 

prop⇒h1 : ∀ {i} {X : Set i} → prop X → h  X
prop⇒h1 {X = X} f x y = p₀ x y , lem x y
  where
    p₀ : (x y : X) → x ≡ y
    p₀ x y = f x y · (f y y)⁻¹

    lem : (x y : X)(p : x ≡ y) → p₀ x y ≡ p
    lem x .x refl = left-inverse (f x x)

-- a contractible set is propositional
contr⇒prop : ∀ {i} {X : Set i} → contr X → prop X
contr⇒prop (x , p) = λ x' x'' → sym (p x') · p x''

-- h-levels are upwards closed
h↑ : ∀ {i n}{X : Set i} → h n X → h (suc n) X
h↑ {n = } c = prop⇒h1 (contr⇒prop c)
h↑ {n = suc n} hn = λ x x' → h↑ (hn x x')

-- Prop: the set of propositions
HProp : ∀ i → Set (lsuc i)
HProp i = Σ (Set i) (h )

-- HSet : sets
HSet : ∀ i → Set (lsuc i)
HSet i = Σ (Set i) (h )

-- Types by h-level (shifted by 2)
Type : ∀ i → ℕ → Set (lsuc i)
Type i n = Σ (Set i) (h (suc (suc n)))

-- the inverse image of a y ∈ Y considering a function f : X → Y
_⁻¹_ : ∀ {i k} {X : Set i} {Y : Set k} → (X → Y) → Y → Set (i ⊔ k)
f ⁻¹ y = Σ _ λ x → f x ≡ y

-- singletons are contractible
singl-contr : ∀ {i} {A : Set i} → (x : A) → contr (singleton x)
singl-contr {A = A} x = (x , refl) , λ { (x' , p) → lem x' p }
  where
    lem : (x' : A)(p : x ≡ x') → (x , refl) ≡ (x' , p)
    lem .x refl = refl

singl-contr' : ∀ {i} {A : Set i} → (x : A) → contr (singleton' x)
singl-contr' {A = A} x = (x , refl) , λ { (x' , p) → lem x' p }
  where
    lem : (x' : A)(p : x' ≡ x) → (x , refl) ≡ (x' , p)
    lem .x refl = refl