diff options
Diffstat (limited to 'src/Util/HProp.v')
| -rw-r--r-- | src/Util/HProp.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/HProp.v b/src/Util/HProp.v index 273611fad..89ed16698 100644 --- a/src/Util/HProp.v +++ b/src/Util/HProp.v @@ -1,3 +1,10 @@ +(** * Homotopy Propositions *) +(** A homotopy proposition, or hProp, is a subsingleton type, i.e., a + type with at most one inhabitant. The property of being an hProp, + i.e., being irrelevant when considering propositional equality + ([eq]) of terms, comes up frequently. Since it is frequently + automatically inferrable from the structure of the type, we make a + typeclass for it. *) Class IsHProp T := allpath_hprop : forall x y : T, x = y. Notation IsHPropRel R := (forall x y, IsHProp (R x y)). |