include "logic/pts.ma".
-ninductive True: CProp ≝
+ninductive True: CProp[0] ≝
I : True.
-ninductive False: CProp ≝.
+ninductive False: CProp[0] ≝.
-ndefinition Not: CProp → CProp ≝
+ndefinition Not: CProp[0] → CProp[0] ≝
λA. A → False.
interpretation "logical not" 'not x = (Not x).
-ninductive And (A,B:CProp) : CProp ≝
+ninductive And (A,B:CProp[0]) : CProp[0] ≝
conj : A → B → And A B.
interpretation "logical and" 'and x y = (And x y).
-ninductive Or (A,B:CProp) : CProp ≝
+ninductive Or (A,B:CProp[0]) : CProp[0] ≝
or_introl : A → Or A B
| or_intror : B → Or A B.
interpretation "logical or" 'or x y = (Or x y).
-(* BUG HERE: WHY IS IT ACCEPTED??? *)
-inductive Ex (A:Type[1]) (P:A \to CProp[1]) : CProp[0] \def
- ex_intro: \forall x:A. P x \to Ex A P.
+ninductive Ex (A:Type[0]) (P:A → CProp[0]) : CProp[0] ≝
+ ex_intro: ∀x:A. P x → Ex A P.
-interpretation "exists" 'exists x = (Ex ? x).
\ No newline at end of file
+
+ninductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝
+ ex_intro1: ∀x:A. P x → Ex1 A P.
+
+interpretation "exists1" 'exists x = (Ex1 ? x).
+interpretation "exists" 'exists x = (Ex ? x).
+
+ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
+ sig_intro : ∀x:A.P x → sigma A P.
+
+interpretation "sigma" 'sigma \eta.p = (sigma ? p).
+
+nrecord iff (A,B: CProp[0]) : CProp[0] ≝
+ { if: A → B;
+ fi: B → A
+ }.
+
+notation > "hvbox(a break \liff b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+interpretation "logical iff" 'iff x y = (iff x y).