relativization

gistfile1.txt

import logic data.nat

inductive funext [class] : Prop :=
intro : (∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x = g x), f = g) → funext

namespace funext
definition apply [F : funext] : ∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x = g x), f = g :=
rec_on F (λax, ax)
end funext


section
  variables [F₁₁ : funext.{1 1}]
  include F₁₁

  open nat
  theorem ex : (λx y, x + y) = (λx y, y + x) :=
  funext.apply (take x, funext.apply (take y, add.comm x y))
end

check ex -- Error funext cannot be synthesized

check (λ F : funext, ex) -- Ok F is used as argument for ex

axiom funext_ax : ∀ (A : Type) (B : A → Type) (f g : Π x, B x) (H : ∀ x, f x = g x), f = g

theorem funext_ax_inst [instance] : funext :=
funext.intro funext_ax

check ex -- Ok, funext_inst is used