2015-03-12 07:31:10 +00:00
|
|
|
|
open eq is_equiv funext
|
|
|
|
|
|
|
|
|
|
|
|
constant f : nat → nat → nat
|
|
|
|
|
|
|
|
|
|
|
|
example : (λ x y : nat, f x y) = f :=
|
|
|
|
|
|
rfl
|
|
|
|
|
|
|
|
|
|
|
|
namespace hide
|
|
|
|
|
|
|
|
|
|
|
|
variables {A : Type} {B : A → Type} {C : Πa, B a → Type}
|
|
|
|
|
|
|
|
|
|
|
|
definition homotopy2 [reducible] (f g : Πa b, C a b) : Type :=
|
|
|
|
|
|
Πa b, f a b = g a b
|
|
|
|
|
|
notation f `∼2`:50 g := homotopy2 f g
|
|
|
|
|
|
|
|
|
|
|
|
definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g :=
|
|
|
|
|
|
eq_of_homotopy (λa, eq_of_homotopy (H a))
|
|
|
|
|
|
|
|
|
|
|
|
definition apD100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g :=
|
2015-04-29 17:15:13 +00:00
|
|
|
|
λa b, apd10 (apd10 p a) b
|
2015-03-12 07:31:10 +00:00
|
|
|
|
|
|
|
|
|
|
local attribute eq_of_homotopy [reducible]
|
|
|
|
|
|
|
|
|
|
|
|
definition foo (f g : Πa b, C a b) (H : f ∼2 g) (a : A)
|
|
|
|
|
|
: apD100 (eq_of_homotopy2 H) a = H a :=
|
|
|
|
|
|
begin
|
2015-03-28 00:26:06 +00:00
|
|
|
|
esimp [apD100, eq_of_homotopy2, eq_of_homotopy],
|
2015-04-29 17:15:13 +00:00
|
|
|
|
rewrite (right_inv apd10 (λ(a : A), eq_of_homotopy (H a))),
|
|
|
|
|
|
apply (right_inv apd10)
|
2015-03-12 07:31:10 +00:00
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
end hide
|
