\import Equiv
\import Equiv.Path
\import Logic
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Arith.Nat
\open Nat(+)

-- # Prop

\func isProp (A : \Type) => \Pi (a a' : A) -> a = a'
  \where
    \use \level levelProp (A : \Type) (e e' : isProp A) : e = e'
      => path (\lam i a a' => isProp=>isSet A e a a' (e a a') (e' a a') @ i)

\func \infix  ofHLevel_-1+ (A : \Type) (n : Nat) : \Type \elim n
  |  => isProp A
  | suc n => \Pi (a a' : A) -> (a = a') ofHLevel_-1+ n
  \where
    \use \level levelProp (A : \Type) (n : Nat) (e e' : A ofHLevel_-1+ n) : e = e' \elim n
      |  => isProp.levelProp A e e'
      | suc n => path (\lam i a a' => levelProp (a = a') n (e a a') (e' a a') @ i)

\func isProp=>isSet (A : \Type) (p : isProp A) (a a' : A) : isProp (a = a') => isContr=>isProp (isProp=>HLevel_-2+1 A p a a')

\func isSet (A : \Type) => A ofHLevel_-1+ 

\func isGpd (A : \Type) => A ofHLevel_-1+ 

\lemma isSet=>isGpd (A : \Type) (p : isSet A) : isGpd A => \lam a a' => isProp=>isSet (a = a') (p a a')

\func hLevel-inh {A : \Type} (n : Nat) (f : A -> A ofHLevel_-1+ n) : A ofHLevel_-1+ n \elim n
  |  => \lam a => f a a
  | suc n => \lam a => f a a

-- # Contr

\class Contr (A : \Type) (center : A) (contraction : \Pi (a' : A) -> center = a')
  \where {
    \func make {A : \Type} (a : A) (p : \Pi (a' : A) -> a = a')  => \new Contr A a p

    \use \level levelProp (A : \Type) (c1 c2 : Contr A) : c1 = c2 => exts Contr {
      | center => c1.contraction c2.center
      | contraction a' => isProp=>isSet A (isContr=>isProp c1) c2.center a' _ _
    }
  }

\lemma contr-equiv (A B : Contr) {f : A -> B} : Equiv f
  => \new QEquiv {
    | ret _ => A.center
    | ret_f x => A.contraction x
    | f_sec y => isContr=>isProp B _ _
  }

\func isContr=>isProp {A : \Type} (c : Contr A) : isProp A => \lam a a' => inv (c.contraction a) *> c.contraction a'

\lemma isContr'=>isProp {A : \Type} (c : A -> Contr A) : isProp A => \lam a => isContr=>isProp (c a) a

\lemma isProp=>isContr {A : \Type} (p : isProp A) (a : A) : Contr A => Contr.make a (p a)

\lemma isProp'=>isContr {A : \Type} (p : isProp A) (a : TruncP A) : Contr A \elim a
  | inP a => isProp=>isContr p a

\func I-isContr : Contr I \cowith
  | center => left
  | contraction i => path (I.squeeze i)

\func \infix  ofHLevel_-2+ (A : \Type) (n : Nat) : \Prop \elim n
  |  => Contr A
  | suc n => \Pi (a a' : A) -> (a = a') ofHLevel_-2+ n

-- # Prop-based and Contr-base hLevels are equivalent

\func HLevel_-2+1=>HLevel_-1 (A : \Type) (n : Nat) (p : A ofHLevel_-2+ suc n) : A ofHLevel_-1+ n \elim n
  |  => \lam a a' => Contr.center {p a a'}
  | suc n => \lam a a' => HLevel_-2+1=>HLevel_-1 (a = a') n (p a a')

\func isProp=>HLevel_-2+1 (A : \Type) (p : isProp A) (a a' : A) : Contr (a = a') => \new Contr (a = a') {
  | center => inv (p a a) *> p a a'
  | contraction => Jl (\lam x q => inv (p a a) *> p a x = q) (inv_*> (p a a))
}

\lemma HLevel_-1=>HLevel_-2+1 (A : \Type) (n : Nat) (p : A ofHLevel_-1+ n) : A ofHLevel_-2+ suc n \elim n
  |  => isProp=>HLevel_-2+1 A p
  | suc n => \lam a a' => HLevel_-1=>HLevel_-2+1 (a = a') n (p a a')

-- # Every k-level is n-level whenever k <= n

\func HLevel_-1_suc {A : \Type} {n : Nat} (p : A ofHLevel_-1+ n) : A ofHLevel_-1+ suc n \elim n
  |  => isProp=>isSet A p
  | suc n => \lam a a' => HLevel_-1_suc (p a a')

\func HLevel_-1_+ {A : \Type} {k : Nat} (n : Nat) (p : A ofHLevel_-1+ k) : A ofHLevel_-1+ k + n \elim n
  |  => p
  | suc n => HLevel_-1_suc (HLevel_-1_+ n p)

\func HLevel_-1_<= {A : \Type} (k : Nat) (n : Nat) (q : k <= n) (p : A ofHLevel_-1+ k) : A ofHLevel_-1+ n
  => rewriteI (<=_exists q) (HLevel_-1_+ (n -' k) p)

{- # Properties of hLevels
 - I'm not sure which version of ofHLevel is more convenient, so I proved each lemma twice.
 -}

-- ## Properties of prop-based hLevels

-- | hLevels are closed under retracts
\func HLevel-retracts (s : Section) {n : Nat} (p : s.B ofHLevel_-1+ n) : s.A ofHLevel_-1+ n \elim n
  |  => \lam a a' => inv (s.ret_f a) *> pmap s.ret (p (s a) (s a')) *> s.ret_f a'
  | suc n => \lam a a' => HLevel-retracts (pmapSection s) (p (s a) (s a'))

-- | hLevels are closed under pi-types
\func HLevels-pi {A : \Type} (B : A -> \Type) {n : Nat} (p : \Pi (a : A) -> B a ofHLevel_-1+ n) : (\Pi (a : A) -> B a) ofHLevel_-1+ n \elim n
  |  => \lam f f' => path (\lam i a => p a (f a) (f' a) @ i)
  | suc n => \lam f f' => HLevel-retracts (piEquiv B f f') (HLevels-pi (\lam a => f a = f' a) (\lam a => p a (f a) (f' a)))

-- | hLevels are closed under sigma-types
\func HLevels-sigma {A : \Type} (B : A -> \Type) {n : Nat} (pA : A ofHLevel_-1+ n) (pB : \Pi (a : A) -> B a ofHLevel_-1+ n) : (\Sigma (a : A) (B a)) ofHLevel_-1+ n \elim n
  |  => \lam p p' => ext (pA p. p'., pB p'. _ _)
  | suc n => \lam p p' => HLevel-retracts (sigmaEquiv B p p') (HLevels-sigma (transport B __ p. = p'.) (pA p. p'.) (\lam s => pB _ _ _))

-- | hLevels are closed under embeddings
\func HLevels-embeddings (e : Embedding) {n : Nat} (p : e.B ofHLevel_-1+ n) : e.A ofHLevel_-1+ n \elim n
  |  => \lam a a' => sec {e.isEmb a a'} (p (e a) (e a'))
  | suc n => \lam a a' => HLevels-embeddings (pmapEmbedding e) (p (e a) (e a'))

-- ## Properties of contr-based hLevels

-- | Contr-based hLevels are closed under retracts
\lemma HLevel_-2-retracts (s : Section) {n : Nat} (p : s.B ofHLevel_-2+ n) : s.A ofHLevel_-2+ n \elim n
  |  => \have a0 => s.ret (Contr.center {p}) \in Contr.make a0 (\lam a => inv (s.ret_f a0) *> pmap s.ret (isContr=>isProp p (s a0) (s a)) *> s.ret_f a)
  | suc n => \lam a a' => HLevel_-2-retracts (pmapSection s) (p (s a) (s a'))

-- | Contr-based hLevels are closed under pi-types
\lemma HLevels_-2-pi {A : \Type} (B : A -> \Type) {n : Nat} (p : \Pi (a : A) -> B a ofHLevel_-2+ n) : (\Pi (a : A) -> B a) ofHLevel_-2+ n \elim n
  |  => Contr.make (\lam a => Contr.center {p a}) (\lam f => path (\lam i a => Contr.contraction {p a} (f a) @ i))
  | suc n => \lam f f' => HLevel_-2-retracts (piEquiv B f f') (HLevels_-2-pi (\lam a => f a = f' a) (\lam a => p a (f a) (f' a)))

-- | Contr-based hLevels are closed under sigma-types
\lemma HLevels_-2-sigma {A : \Type} (B : A -> \Type) {n : Nat} (pA : A ofHLevel_-2+ n) (pB : \Pi (a : A) -> B a ofHLevel_-2+ n) : (\Sigma (a : A) (B a)) ofHLevel_-2+ n \elim n
  |  => \let | a0 => Contr.center {pA}
              | p0 => ((a0, Contr.center {pB a0}) : \Sigma (a : A) (B a))
         \in Contr.make p0 (\lam p => ext (Contr.contraction {pA} p., isContr=>isProp (pB p.) _ _))
  | suc n => \lam p p' => HLevel_-2-retracts (sigmaEquiv B p p') (HLevels_-2-sigma (transport B __ p. = p'.) (pA p. p'.) (\lam s => pB _ _ _))