include "preamble.ma".
-(* ACZEL CATEGORIES
+(* CLASSES:
- We use typoids with a compatible membership relation
- The category is intended to be the domain of the membership relation
- The membership relation is necessary because we need to regard the
*)
record Class: Type ≝ {
- class:> Type;
- cin: class → Prop;
- ces: class → class \to Prop
+ class :> Type;
+ cin : class → Prop;
+ ces : class → class → Prop;
+ ces_cin_fw: ∀c1,c2. cin c1 → ces c1 c2 → cin c2;
+ ces_cin_bw: ∀c1,c2. cin c1 → ces c2 c1 → cin c2
}.
-(* default inhabitance predicates *)
-definition true_f ≝ λ(X:Type). λ(_:X). True.
-definition false_f ≝ λ(X:Type). λ(_:X). False.
+(* equality predicate *******************************************************)
-(* equality predicate *)
inductive ceq (C:Class): class C → class C → Prop ≝
- | ceq_refl : ∀c. cin ? c → ceq ? c c
- | ceq_trans: ∀c1,c,c2. cin ? c1 → ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
- | ceq_conf : ∀c1,c,c2. cin ? c1 → ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
+ | ceq_refl : ∀c. ceq ? c c
+ | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
+ | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
.
+(* default inhabitance predicates *******************************************)
+
+definition true_f ≝ λX:Type. λ_:X. True.
+
+definition false_f ≝ λX:Type. λ_:X. False.
+
+(* default foreward compatibilities *****************************************)
+
+theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A.
+intros; autobatch.
+qed.
+
+definition true_fw ≝ const_fw True.
+
+definition false_fw ≝ const_fw False.
+
+(* default backward compatibilities *****************************************)
+
+theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A.
+intros; autobatch.
+qed.
+
+definition true_bw ≝ const_bw True.
+
+definition false_bw ≝ const_bw False.