include "datatypes/subsets.ma".
-record ssigma (A:Type) (S: powerset A) : Type ≝
- { witness:> A;
- proof:> witness ∈ S
- }.
-
-coercion ssigma.
-
-record binary_relation (A,B: Type) (U: Ω \sup A) (V: Ω \sup B) : Type ≝
- { satisfy:2> U → V → CProp }.
+record binary_relation (A,B: setoid) : Type ≝
+ { satisfy:> binary_morphism1 A B CPROP }.
notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}.
notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}.
-interpretation "relation applied" 'satisfy r x y = (satisfy ____ r x y).
+interpretation "relation applied" 'satisfy r x y = (fun1 ___ (satisfy __ r) x y).
-definition composition:
- ∀A,B,C.∀U1: Ω \sup A.∀U2: Ω \sup B.∀U3: Ω \sup C.
- binary_relation ?? U1 U2 → binary_relation ?? U2 U3 →
- binary_relation ?? U1 U3.
- intros (A B C U1 U2 U3 R12 R23);
+definition binary_relation_setoid: setoid → setoid → setoid1.
+ intros (A B);
constructor 1;
- intros (s1 s3);
- apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
-qed.
-
-interpretation "binary relation composition" 'compose x y = (composition ______ x y).
-
-definition equal_relations ≝
- λA,B,U,V.λr,r': binary_relation A B U V.
- ∀x,y. r x y ↔ r' x y.
-
-interpretation "equal relation" 'eq x y = (equal_relations ____ x y).
-
-lemma refl_equal_relations: ∀A,B,U,V. reflexive ? (equal_relations A B U V).
- intros 5; intros 2; split; intro; assumption.
-qed.
-
-lemma sym_equal_relations: ∀A,B,U,V. symmetric ? (equal_relations A B U V).
- intros 7; intros 2; split; intro;
- [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption.
-qed.
-
-lemma trans_equal_relations: ∀A,B,U,V. transitive ? (equal_relations A B U V).
- intros 9; intros 2; split; intro;
- [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
- [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
- assumption.
-qed.
-
-lemma associative_composition:
- ∀A,B,C,D.∀U1,U2,U3,U4.
- ∀r1:binary_relation A B U1 U2.
- ∀r2:binary_relation B C U2 U3.
- ∀r3:binary_relation C D U3 U4.
- (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
- intros 13;
- split; intro;
- cases H; clear H; cases H1; clear H1;
- [cases H; clear H | cases H2; clear H2]
- cases H1; clear H1;
- exists; try assumption;
- split; try assumption;
- exists; try assumption;
- split; assumption.
-qed.
-
-lemma composition_morphism:
- ∀A,B,C.∀U1,U2,U3.
- ∀r1,r1':binary_relation A B U1 U2.
- ∀r2,r2':binary_relation B C U2 U3.
- r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
- intros 14; split; intro;
- cases H2; clear H2; cases H3; clear H3;
- [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
- [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
- exists; try assumption;
- split; assumption.
+ [ apply (binary_relation A B)
+ | constructor 1;
+ [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y)
+ | simplify; intros 3; split; intro; assumption
+ | simplify; intros 5; split; intro;
+ [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption
+ | simplify; intros 7; split; intro;
+ [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
+ [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
+ assumption]]
qed.
-definition binary_relation_setoid: ∀A,B. Ω \sup A → Ω \sup B → setoid.
- intros (A B U V);
+definition composition:
+ ∀A,B,C.
+ binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
+ intros;
constructor 1;
- [ apply (binary_relation ?? U V)
- | constructor 1;
- [ apply equal_relations
- | apply refl_equal_relations
- | apply sym_equal_relations
- | apply trans_equal_relations
- ]]
+ [ intros (R12 R23);
+ constructor 1;
+ constructor 1;
+ [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
+ | intros;
+ split; intro; cases H2 (w H3); clear H2; exists; [1,3: apply w ]
+ [ apply (. (H‡#)‡(#‡H1)); assumption
+ | apply (. ((H \sup -1)‡#)‡(#‡(H1 \sup -1))); assumption]]
+ | intros 8; split; intro H2; simplify in H2 ⊢ %;
+ cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); clear H3;
+ [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
+ [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
+ exists; try assumption;
+ split; assumption]
qed.
-record sigma (A:Type) (P: A → Type) : Type ≝
- { s_witness:> A;
- s_proof:> P s_witness
- }.
-
-interpretation "sigma" 'sigma \eta.x = (sigma _ x).
-
-definition REL: category.
+definition REL: category1.
constructor 1;
- [ apply (ΣA:Type.Ω \sup A)
- | intros; apply (binary_relation_setoid ?? (s_proof ?? s) (s_proof ?? s1))
- | intros; constructor 1; intros; apply (s=s1)
+ [ apply setoid
+ | intros (T T1); apply (binary_relation_setoid T T1)
| intros; constructor 1;
- [ apply composition
- | apply composition_morphism
- ]
- | intros; unfold mk_binary_morphism; simplify;
- apply associative_composition
- |6,7: intros 5; simplify; split; intro;
- [1,3: cases H; clear H; cases H1; clear H1;
- [ rewrite > H | rewrite < H2 ]
- assumption
- |*: exists; try assumption; split; first [ reflexivity | assumption ]]]
+ constructor 1; unfold setoid1_of_setoid; simplify;
+ [ intros; apply (c = c1)
+ | intros; split; intro;
+ [ apply (trans ????? (H \sup -1));
+ apply (trans ????? H2);
+ apply H1
+ | apply (trans ????? H);
+ apply (trans ????? H2);
+ apply (H1 \sup -1)]]
+ | apply composition
+ | intros 9;
+ split; intro;
+ cases f (w H); clear f; cases H; clear H;
+ [cases f (w1 H); clear f | cases f1 (w1 H); clear f1]
+ cases H; clear H;
+ exists; try assumption;
+ split; try assumption;
+ exists; try assumption;
+ split; assumption
+ |6,7: intros 5; unfold composition; simplify; split; intro;
+ unfold setoid1_of_setoid in x y; simplify in x y;
+ [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
+ [ apply (. (H \sup -1 : eq1 ? w x)‡#); assumption
+ | apply (. #‡(H : eq1 ? w y)); assumption]
+ |2,4: exists; try assumption; split; first [apply refl | assumption]]]
qed.
-definition elements: objs REL → Type ≝
- λb:ΣA.Ω\sup A.ssigma (s_witness ?? b) (s_proof ?? b).
-
-coercion elements.
-
-definition carrier: objs REL → Type ≝
- λb:ΣA.Ω\sup A.s_witness ?? b.
+definition full_subset: ∀s:REL. Ω \sup s.
+ apply (λs.{x | True});
+ intros; simplify; split; intro; assumption.
+qed.
-interpretation "REL carrier" 'card c = (carrier c).
+coercion full_subset.
-definition subset: ∀b:objs REL. Ω \sup (carrier b) ≝
- λb:ΣA.Ω\sup A.s_proof ?? b.
+definition setoid1_of_REL: REL → setoid ≝ λS. S.
-coercion subset.
+coercion setoid1_of_REL.
\ No newline at end of file