michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library,hott): define 'congr' in the initialization files

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-02 11:29:31 -07:00
parent 2054d67483
commit 458d13025f
3 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
hott/init/logic.hlean
View file

@ -61,6 +61,9 @@ namespace eq
end ops end ops
end eq end eq
theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
eq.subst H₁ (eq.subst H₂ rfl)
section section
variables {A : Type} {a b c: A} variables {A : Type} {a b c: A}
open eq.ops open eq.ops

3
library/init/logic.lean
View file

@ -57,6 +57,9 @@ namespace eq
end ops end ops
end eq end eq
theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
eq.subst H₁ (eq.subst H₂ rfl)
section section
variables {A : Type} {a b c: A} variables {A : Type} {a b c: A}
open eq.ops open eq.ops

3
library/logic/eq.lean
View file

@ -58,9 +58,6 @@ section
theorem congr_arg (f : A → B) (H : a = a') : f a = f a' := theorem congr_arg (f : A → B) (H : a = a') : f a = f a' :=
H ▸ rfl H ▸ rfl
theorem congr {f g : A → B} (H₁ : f = g) (H₂ : a = a') : f a = g a' :=
H₁ ▸ H₂ ▸ rfl
theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
congr (congr_arg f Ha) Hb congr (congr_arg f Ha) Hb