From 212b073990426dccd8799294c583e2e58a015463 Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Mon, 1 Aug 2016 13:22:21 -0700
Subject: Add documentation: Equality, HProp, Isomorphism, Sigma (#41)

* Add doc: Equality, HProp, Isomorphism, Sigma

* Update documentation with suggestions from Andres
---
 src/Util/HProp.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/Util/HProp.v')

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)).
-- 
cgit v1.2.3