-
Notifications
You must be signed in to change notification settings - Fork 80
/
funext.lean
69 lines (49 loc) · 2.35 KB
/
funext.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
Extensional equality for functions, and a proof of function extensionality from quotients.
-/
prelude
import init.data.quot init.logic
open quotient
universes u v
variables {α : Sort u} {β : α → Sort v}
namespace function
/-- The relation stating that two functions are pointwise equal. -/
protected def equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x
local infix ` ~ `:50 := function.equiv
protected theorem equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl
protected theorem equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ :=
λ h x, eq.symm (h x)
protected theorem equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
λ h₁ h₂ x, eq.trans (h₁ x) (h₂ x)
protected theorem equiv.is_equivalence (α : Sort u) (β : α → Sort v) : equivalence (@function.equiv α β) :=
mk_equivalence (@function.equiv α β) (@equiv.refl α β) (@equiv.symm α β) (@equiv.trans α β)
/-- The setoid generated by pointwise equality. -/
local attribute [instance]
def fun_setoid (α : Sort u) (β : α → Sort v) : setoid (Π x : α, β x) :=
setoid.mk (@function.equiv α β) (function.equiv.is_equivalence α β)
/-- The quotient of the function type by pointwise equality. -/
def extfun (α : Sort u) (β : α → Sort v) : Sort (imax u v) :=
quotient (fun_setoid α β)
/-- The map from functions into the qquotient by pointwise equality. -/
def fun_to_extfun (f : Π x : α, β x) : extfun α β :=
⟦f⟧
/-- From an element of `extfun` we can retrieve an actual function. -/
def extfun_app (f : extfun α β) : Π x : α, β x :=
assume x,
quot.lift_on f
(λ f : Π x : α, β x, f x)
(λ f₁ f₂ h, h x)
end function
open function
local attribute [instance] fun_setoid
/-- Function extensionality, proven using quotients. -/
theorem funext {f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
show extfun_app ⟦f₁⟧ = extfun_app ⟦f₂⟧, from
congr_arg extfun_app (sound h)
attribute [intro!] funext
local infix ` ~ `:50 := function.equiv
instance pi.subsingleton [∀ a, subsingleton (β a)] : subsingleton (Π a, β a) :=
⟨λ f₁ f₂, funext (λ a, subsingleton.elim (f₁ a) (f₂ a))⟩