Theory HoTT_Base

theory HoTT_Base
  imports Pure
begin

section ‹Expressions, judgments, and universes›

typedecl expr
typedecl level

judgment has_type :: "expr ⇒ expr ⇒ prop"
  (infix "∷⇩h" 50)

consts
  level_zero :: level
  level_succ :: "level ⇒ level"
  level_less :: "level ⇒ level ⇒ prop"
    (infix "≺⇩l" 50)
  universe :: "level ⇒ expr"

text ‹
  The level relation is a strict order.  Pure has no falsity, so irreflexivity
  is stated in its ex-falso form: a hypothetical self-relation ‹i ≺⇩l i›
  derives an arbitrary Pure proposition.  Every axiom below holds in the
  intended model, which reads levels as natural numbers, ‹level_succ› as the
  successor, and ‹≺⇩l› as the strict order; there the irreflexivity
  premise is impossible, so the axiom is sound and serves only to derive
  asymmetry.
›

axiomatization where
  level_step: "i ≺⇩l level_succ i" and
  level_trans: "i ≺⇩l j ⟹ j ≺⇩l k ⟹ i ≺⇩l k" and
  level_irrefl: "i ≺⇩l i ⟹ PROP W" and
  universe_form: "universe i ∷⇩h universe (level_succ i)" and
  universe_cumul:
    "i ≺⇩l j ⟹ A ∷⇩h universe i ⟹ A ∷⇩h universe j" and
  type_conversion:
    "a ∷⇩h A ⟹ A ≡ B ⟹ a ∷⇩h B" and
  term_conversion:
    "a ≡ b ⟹ a ∷⇩h A ⟹ b ∷⇩h A"

lemma level_two_steps:
  "i ≺⇩l level_succ (level_succ i)"
  by (rule level_trans[OF level_step level_step])

lemma level_asym:
  assumes ij: "i ≺⇩l j"
    and ji: "j ≺⇩l i"
  shows "PROP W"
  by (rule level_irrefl[OF level_trans[OF ij ji]])

lemma level_succ_not_below:
  assumes "level_succ i ≺⇩l i"
  shows "PROP W"
  by (rule level_asym[OF level_step assms])

lemma level_two_steps_not_below:
  assumes "level_succ (level_succ i) ≺⇩l i"
  shows "PROP W"
  by (rule level_asym[OF level_two_steps assms])

lemma universe_cumul_two:
  assumes "A ∷⇩h universe i"
  shows "A ∷⇩h universe (level_succ (level_succ i))"
  by (rule universe_cumul[OF level_two_steps assms])

end