From b98ec63895887435aa6f08436715200d33a62d98 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 14 Sep 2018 21:16:12 -0400 Subject: Add PrimitiveSigma --- src/Util/Equality.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/Equality.v') diff --git a/src/Util/Equality.v b/src/Util/Equality.v index 04335dbd4..d1a711821 100644 --- a/src/Util/Equality.v +++ b/src/Util/Equality.v @@ -8,6 +8,13 @@ Require Import Coq.Classes.Morphisms. Require Import Crypto.Util.Isomorphism. Require Import Crypto.Util.HProp. +Import EqNotations. + +Definition f_equal_dep {A B} (f : forall a : A, B a) (x y : A) (H : x = y) : rew [B] H in f x = f y + := match H with + | eq_refl => eq_refl + end. + (** Most of the structure of proofs of equalities fits into what mathematicians call a weak ∞-groupoid. (In fact, one way of *defining* a weak ∞-groupoid is via what's called the J-rule, -- cgit v1.2.3