diff options
Diffstat (limited to 'hott/Propositions.thy')
| -rw-r--r-- | hott/Propositions.thy | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/hott/Propositions.thy b/hott/Propositions.thy index 66e34d2..2c98a5a 100644 --- a/hott/Propositions.thy +++ b/hott/Propositions.thy @@ -5,8 +5,11 @@ imports begin -definition isProp where "isProp A \<equiv> \<Prod>x y: A. x =\<^bsub>A\<^esub> y" -definition isSet where "isSet A \<equiv> \<Prod>x y: A. \<Prod>p q: x =\<^bsub>A\<^esub> y. p =\<^bsub>x =\<^bsub>A\<^esub> y\<^esub> q" +Definition isProp: ":= \<Prod>x y: A. x = y" + where "A: U i" by typechk + +Definition isSet: ":=\<Prod>x y: A. \<Prod>p q: x = y. p = q" + where "A: U i" by typechk Theorem isProp_Top: "isProp \<top>" unfolding isProp_def @@ -16,4 +19,5 @@ Theorem isProp_Bot: "isProp \<bottom>" unfolding isProp_def by (intros, elim) + end |