From 19797bd0eb8cc1b879562728da63255dafcde893 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 23 Jan 2017 17:30:52 -0500 Subject: Minor additions --- src/Util/Equality.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/Equality.v') diff --git a/src/Util/Equality.v b/src/Util/Equality.v index b128305f0..b7bce062d 100644 --- a/src/Util/Equality.v +++ b/src/Util/Equality.v @@ -41,6 +41,9 @@ Proof. case q; case p; reflexivity. Defined. Lemma inv_V {A x y} (p : x = y :> A) : eq_sym (eq_sym p) = p. Proof. case p; reflexivity. Defined. +Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x) + : eq_rect _ P u _ p = eq_rect _ (fun T => T) u _ (f_equal P p). +Proof. case p; reflexivity. Defined. (** To classify the equalities of a type [A] at a point [a : A], we must give a "code" that stands in for the type [a = x] for each @@ -112,3 +115,10 @@ Section hprop. apply f_equal; apply allpath_hprop. Qed. End hprop. + + +Lemma commute_eq_rect {A} (P Q : A -> Type) (f : forall a, P a -> Q a) a b (H : a = b :> A) + (v : P a) + : f b (eq_rect _ P v _ H) + = eq_rect _ Q (f a v) _ H. +Proof. destruct H; reflexivity. Defined. -- cgit v1.2.3