symbolic-dynamics/Families.v
-rw-r--r--
2.4 KiB
View raw

` `

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60

```
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
* Type families, a.k.a. constructive predicates and sets...
*
* This module is essentially an adaptation of Ensembles for Type,
* to get over the issue with "indestructibility of propositions":
* i.e. case analysis is not allowed for the ordinary disjunction.
* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
Section Families.
Variable U: Type. (* a universe, the index type of the family *)
Definition Family := U -> Type.
(* Families may be thought of as predicates, and sets as well:
The legend is that for every element of U there is given a type,
empty or not; respectively, the predicate is false or true *)
Inductive Empty: Family := . (* i.e. the empty type on every index *)
Inductive Full: Family := Full_intro: forall x: U, Full x.
(* i.e. whatever element of U is taken, the type is non-empty *)
Definition Included (A B: Family): Type := forall x: U, A x -> B x.
Definition Same (A B: Family): Type :=
(Included A B) * (Included B A). (* a.k.a. equivalence *)
Lemma Empty_is_a_subtype (A: Family): Included Empty A.
Proof. unfold Included. intros. contradict X. Qed.
Lemma Full_is_a_supertype (A: Family): Included A Full.
Proof. unfold Included. intros. apply Full_intro. Qed.
Definition Emptiness (A: Family) := Included A Empty.
Definition Fullness (A: Family) := Included Full A.
Inductive Intersection (A B: Family): Family :=
Intersection_intro: forall x: U, A x -> B x -> (Intersection A B) x.
Inductive Union (A B: Family): Family :=
| Union_intro_0: forall x: U, A x -> (Union A B) x
| Union_intro_1: forall x: U, B x -> (Union A B) x.
(* The (co)product is defined via currying & recursion principles;
alternatively, these might be defined via A + B and A * B *)
Definition Disjoint (A B: Family): Type :=
Emptiness (Intersection A B).
Definition Covering (A B: Family): Type :=
Fullness (Union A B).
Inductive Singleton (x: U): Family :=
Singleton_intro: Singleton x x. (* a.k.a. reflexivity *)
(** Extensionality Axiom *)
Axiom Extensionality_Families: forall A B: Family, Same A B -> A = B.
End Families.
Hint Unfold Included Same Emptiness Covering Disjoint Covering:
families.
Hint Resolve Full_intro Intersection_intro Union_intro_0 Union_intro_1
Singleton_intro Extensionality_Families: families.
```