search

HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
http://coq.inria.fr/
GNU Lesser General Public License v2.1
27 stars 5 forks source link

Theorem about transport? #51

Closed JasonGross closed 11 years ago

JasonGross commented 11 years ago

Is there a good name for the theorem

(forall A X Y Z x y p a b, @transport A (fun a => forall (x : X) (y : Y a x), Z a x y) x y p a b
                                    = @transport A (fun a => forall y : Y a b, Z a b y) x y p (a b))

which is trivially provable by path induction and reflexivity? Also, is the a version where X depends on A?

mikeshulman commented 11 years ago

transport_forall_constant and transport_forall in types/Forall.v?

JasonGross commented 11 years ago

Ah, thanks. (Oops, I seem to have posted this in the wrong repository.)