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

open import level
open import decidable
open import equality
open import function.isomorphism.core
-- open import function.isomorphism.properties
open import sum
open import hott.level.core
open import hott.equivalence.core
open import hott.univalence
open import sets.nat.core
open import sets.nat.ordering.leq.core
open import sets.nat.ordering.leq.decide
open import sets.empty
open import sets.unit

Σ-contr :  {i j}{X : Set i}{Y : X  Set j}
         contr X  ((x : X)  contr (Y x))
         contr (Σ X Y)
Σ-contr {X = X}{Y = 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 = ap  x  (x , proj₁ (hY x))) (cx x)
            · ap (_,_ x) (proj₂ (hY x) y)

×-contr :  {i j}{X : Set i}{Y : Set j}
         contr X  contr Y
         contr (X × Y)
×-contr hX hY = Σ-contr hX  _  hY)

unique-contr :  {i}{A B : Set i}
              contr A
              contr B
              A  B
unique-contr {i}{A}{B} hA hB = ≈⇒≡ (f , f-we)
  where
    f : A  B
    f _ = proj₁ hB

    f-we : weak-equiv f
    f-we b = ×-contr hA (h↑ hB _ _)

h-≤ :  {i n m}{X : Set i}
     n  m  h n X  h m X
h-≤ {m = 0} z≤n hX = hX
h-≤ {m = suc m} z≤n hX = λ x y
   h-≤ {m = m} z≤n (h↑ hX x y)
h-≤ (s≤s p) hX = λ x y
   h-≤ p (hX x y)

h! :  {i n m}{X : Set i}
    {p : True (n ≤? m)}
    h n X  h m X
h! {p = p} = h-≤ (witness p)

abstract
  -- retractions preserve levels
  retract-level :  {i j n} {X : Set i}{Y : Set j}
                  (f : X  Y)(g : Y  X)
                  ((y : Y)  f (g y)  y)
                  h n X  h n Y
  retract-level {n = 0}{X}{Y} f g r (x , c) = (f x , c')
    where
      c' : (y : Y)  f x  y
      c' y = ap f (c (g y)) · r y
  retract-level {n = suc n}{X}{Y} f g r hX = λ y y'
     retract-level f' g' r' (hX (g y) (g y'))
    where
      f' : {y y' : Y}  g y  g y'  y  y'
      f' {y}{y'} p = sym (r y) · ap f p · r y'

      g' : {y y' : Y}  y  y'  g y  g y'
      g' = ap g

      r' : {y y' : Y}(p : y  y')  f' (g' p)  p
      r' {y}{.y} refl = ap  α  α · r y) (left-unit (sym (r y)))
                      · right-inverse (r y)

  iso-level :  {i j n}{X : Set i}{Y : Set j}
              X  Y  h n X  h n Y
  iso-level (iso f g H K) = retract-level f g K