Theory HoTT_Univalence

theory HoTT_Univalence
  imports HoTT_Equivalence
begin

section ‹The canonical map from identity to equivalence›

definition idtoequiv ::
  "level ⇒ expr ⇒ expr ⇒ expr ⇒ expr"
where
  "idtoequiv i A B p ≡
    identity_ind (universe i) A
      (λB _. equivalence A B)
      (identity_equivalence A) B p"

lemma idtoequiv_type:
  assumes A: "A ∷⇩h universe i"
    and B: "B ∷⇩h universe i"
    and p: "p ∷⇩h identity_type (universe i) A B"
  shows "idtoequiv i A B p ∷⇩h equivalence A B"
  unfolding idtoequiv_def
proof (rule identity_elim)
  show "universe i ∷⇩h universe (level_succ i)"
    by (rule universe_form)
next
  show "A ∷⇩h universe i" by (rule A)
next
  fix X q
  assume X: "X ∷⇩h universe i"
  assume "q ∷⇩h identity_type (universe i) A X"
  show "equivalence A X ∷⇩h universe i"
    by (rule equivalence_form[OF A X])
next
  show "identity_equivalence A ∷⇩h equivalence A A"
    by (rule identity_equivalence_type[OF A])
next
  show "B ∷⇩h universe i" by (rule B)
next
  show "p ∷⇩h identity_type (universe i) A B" by (rule p)
qed

lemma idtoequiv_refl [simp]:
  "idtoequiv i A A (reflexivity (universe i) A) ≡
    identity_equivalence A"
  unfolding idtoequiv_def by simp

definition idtoequiv_map ::
  "level ⇒ expr ⇒ expr ⇒ expr"
where
  "idtoequiv_map i A B ≡
    lambda (identity_type (universe i) A B)
      (λp. idtoequiv i A B p)"

lemma idtoequiv_map_type:
  assumes A: "A ∷⇩h universe i"
    and B: "B ∷⇩h universe i"
  shows "idtoequiv_map i A B ∷⇩h
    arrow (identity_type (universe i) A B) (equivalence A B)"
proof -
  have paths: "identity_type (universe i) A B
      ∷⇩h universe (level_succ i)"
    by (rule identity_form[OF universe_form A B])
  show "idtoequiv_map i A B ∷⇩h
      arrow (identity_type (universe i) A B) (equivalence A B)"
    unfolding idtoequiv_map_def
  proof (rule arrow_intro[OF paths])
    fix p
    assume p: "p ∷⇩h identity_type (universe i) A B"
    show "idtoequiv i A B p ∷⇩h equivalence A B"
      by (rule idtoequiv_type[OF A B p])
  qed
qed

section ‹Univalence›

consts
  univalence_witness :: "level ⇒ expr ⇒ expr ⇒ expr"

axiomatization where
  univalence:
    "A ∷⇩h universe i ⟹ B ∷⇩h universe i ⟹
      univalence_witness i A B ∷⇩h
        biinvertible
          (identity_type (universe i) A B)
          (equivalence A B)
          (idtoequiv_map i A B)"

definition univalence_equivalence ::
  "level ⇒ expr ⇒ expr ⇒ expr"
where
  "univalence_equivalence i A B ≡
    pair (idtoequiv_map i A B) (univalence_witness i A B)"

theorem univalence_equivalence_type:
  assumes A: "A ∷⇩h universe i"
    and B: "B ∷⇩h universe i"
  shows "univalence_equivalence i A B ∷⇩h
    equivalence (identity_type (universe i) A B) (equivalence A B)"
  unfolding univalence_equivalence_def
proof (rule equivalence_intro)
  show "idtoequiv_map i A B ∷⇩h
      arrow (identity_type (universe i) A B) (equivalence A B)"
    by (rule idtoequiv_map_type[OF A B])
next
  show "univalence_witness i A B ∷⇩h
      biinvertible
        (identity_type (universe i) A B)
        (equivalence A B)
        (idtoequiv_map i A B)"
    by (rule univalence[OF A B])
qed

end