Theory HoTT_Function_Extensionality

theory HoTT_Function_Extensionality
  imports HoTT_Equivalence
begin

section ‹The canonical map from function paths to homotopies›

definition happly ::
  "expr ⇒ (expr ⇒ expr) ⇒ expr ⇒ expr ⇒
    expr ⇒ expr"
where
  "happly A B f g p ≡
    identity_ind (pi_type A B) f
      (λg _. homotopy A B f g)
      (homotopy_refl A B f) g p"

lemma happly_type:
  assumes A: "A ∷⇩h universe i"
    and B: "⋀x. x ∷⇩h A ⟹ B x ∷⇩h universe i"
    and f: "f ∷⇩h pi_type A B"
    and g: "g ∷⇩h pi_type A B"
    and p: "p ∷⇩h identity_type (pi_type A B) f g"
  shows "happly A B f g p ∷⇩h homotopy A B f g"
  unfolding happly_def
proof (rule identity_elim)
  show "pi_type A B ∷⇩h universe i"
    by (rule pi_form[OF A B])
next
  show "f ∷⇩h pi_type A B" by (rule f)
next
  fix h q
  assume h: "h ∷⇩h pi_type A B"
  assume "q ∷⇩h identity_type (pi_type A B) f h"
  show "homotopy A B f h ∷⇩h universe i"
    by (rule homotopy_form[OF A B f h])
next
  show "homotopy_refl A B f ∷⇩h homotopy A B f f"
    by (rule homotopy_refl_type[OF A B f])
next
  show "g ∷⇩h pi_type A B" by (rule g)
next
  show "p ∷⇩h identity_type (pi_type A B) f g" by (rule p)
qed

lemma happly_refl [simp]:
  "happly A B f f (reflexivity (pi_type A B) f) ≡
    homotopy_refl A B f"
  unfolding happly_def by simp

definition happly_map ::
  "expr ⇒ (expr ⇒ expr) ⇒ expr ⇒ expr ⇒ expr"
where
  "happly_map A B f g ≡
    lambda (identity_type (pi_type A B) f g)
      (λp. happly A B f g p)"

lemma happly_map_type:
  assumes A: "A ∷⇩h universe i"
    and B: "⋀x. x ∷⇩h A ⟹ B x ∷⇩h universe i"
    and f: "f ∷⇩h pi_type A B"
    and g: "g ∷⇩h pi_type A B"
  shows "happly_map A B f g ∷⇩h
    arrow (identity_type (pi_type A B) f g) (homotopy A B f g)"
proof -
  have functions: "pi_type A B ∷⇩h universe i"
    by (rule pi_form[OF A B])
  have paths: "identity_type (pi_type A B) f g ∷⇩h universe i"
    by (rule identity_form[OF functions f g])
  show "happly_map A B f g ∷⇩h
      arrow (identity_type (pi_type A B) f g) (homotopy A B f g)"
    unfolding happly_map_def
  proof (rule arrow_intro[OF paths])
    fix p
    assume p: "p ∷⇩h identity_type (pi_type A B) f g"
    show "happly A B f g p ∷⇩h homotopy A B f g"
      by (rule happly_type[OF A B f g p])
  qed
qed

section ‹Function extensionality›

consts
  function_extensionality_witness ::
    "expr ⇒ (expr ⇒ expr) ⇒ expr ⇒ expr ⇒ expr"

axiomatization where
  function_extensionality:
    "A ∷⇩h universe i ⟹
      (⋀x. x ∷⇩h A ⟹ B x ∷⇩h universe i) ⟹
      f ∷⇩h pi_type A B ⟹ g ∷⇩h pi_type A B ⟹
      function_extensionality_witness A B f g ∷⇩h
        biinvertible
          (identity_type (pi_type A B) f g)
          (homotopy A B f g)
          (happly_map A B f g)"

definition funext ::
  "expr ⇒ (expr ⇒ expr) ⇒ expr ⇒ expr ⇒
    expr ⇒ expr"
where
  "funext A B f g H ≡
    app
      (left_inverse_function
        (identity_type (pi_type A B) f g)
        (homotopy A B f g)
        (happly_map A B f g)
        (function_extensionality_witness A B f g))
      H"

theorem funext_type:
  assumes A: "A ∷⇩h universe i"
    and B: "⋀x. x ∷⇩h A ⟹ B x ∷⇩h universe i"
    and f: "f ∷⇩h pi_type A B"
    and g: "g ∷⇩h pi_type A B"
    and H: "H ∷⇩h homotopy A B f g"
  shows "funext A B f g H ∷⇩h
    identity_type (pi_type A B) f g"
proof -
  have ext: "function_extensionality_witness A B f g ∷⇩h
      biinvertible
        (identity_type (pi_type A B) f g)
        (homotopy A B f g)
        (happly_map A B f g)"
    by (rule function_extensionality[OF A B f g])
  have inverse: "left_inverse_function
      (identity_type (pi_type A B) f g)
      (homotopy A B f g)
      (happly_map A B f g)
      (function_extensionality_witness A B f g)
      ∷⇩h arrow (homotopy A B f g)
        (identity_type (pi_type A B) f g)"
    by (rule left_inverse_function_type[OF ext])
  show "funext A B f g H ∷⇩h
      identity_type (pi_type A B) f g"
    unfolding funext_def
    by (rule arrow_elim[OF inverse H])
qed

end