32 lines
824 B
Text
32 lines
824 B
Text
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 :=
|
||
λa b, apd10 (apd10 p a) b
|
||
|
||
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
|
||
esimp [apD100, eq_of_homotopy2, eq_of_homotopy],
|
||
rewrite (right_inv apd10 (λ(a : A), eq_of_homotopy (H a))),
|
||
apply (right_inv apd10)
|
||
end
|
||
|
||
end hide
|