2015-03-13 01:07:55 +00:00
|
|
|
import types.eq
|
|
|
|
|
open eq
|
|
|
|
|
|
|
|
|
|
variables {A : Type} {a1 a2 a3 : A}
|
|
|
|
|
definition my_transport_eq_l (p : a1 = a2) (q : a1 = a3)
|
|
|
|
|
: transport (λx, x = a3) p q = p⁻¹ ⬝ q :=
|
|
|
|
|
begin
|
2016-11-24 05:13:05 +00:00
|
|
|
rewrite eq_transport_l,
|
2015-03-13 01:07:55 +00:00
|
|
|
end
|
