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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140 | From HoTT Require Import Basics Types Truncations.
(** The "fiber" of a map with respect to a relation. *)
(** TODO remove? *)
Definition rfiber {X Y : Type} (R : Relation Y) (f : X -> Y) (y : Y) : Type
:= exists x, R (f x) y.
Definition lfiber {X Y : Type} (R : Relation Y) (f : X -> Y) (y : Y) : Type
:= exists x, R y (f x).
(** * The equivalence relation generated by a relation. *)
(** We model the equivalence relation generated by a relation using alternating zig-zags, and by throwing in reflexivity relations. It's easy to show that the resulting relation is an equivalence relation. *)
(** The 'zig' goes forward, and the 'zag' goes backward *)
Fixpoint zig_or_zag {X : Type} (R : Relation X) (n : nat) (x0 x1 : X) : Type
:= match n with
| 0%nat => x0 = x1
| S n => exists x, zig_or_zag R n x0 x * (R x x1 + R x1 x)
end.
(** The equivalence relation generated by a relation [R]. *)
Definition EqRel {X : Type} (R : Relation X) (x0 x1 : X) : Type
:= exists n, zig_or_zag R n x0 x1.
(** We can add ("cons") a zig or a zag at the end of a chain of such. *)
Definition zig_cons {X : Type} (R : Relation X) {x0 x1 x2 : X}
(rho : EqRel R x0 x1) (zig : R x1 x2)
: EqRel R x0 x2
:= (S rho.1; (x1; (rho.2, inl zig))).
Definition zag_cons {X : Type} (R : Relation X) {x0 x1 x2 : X}
(rho : EqRel R x0 x1) (zag : R x2 x1)
: EqRel R x0 x2
:= (S rho.1; (x1; (rho.2, inr zag))).
Global Instance reflexive_eqrel {X : Type} (R : Relation X)
: Reflexive (EqRel R) := fun _ => (0%nat; idpath).
Definition zig_to_eqrel {X : Type} (R : Relation X)
{x0 x1 : X} (zig : R x0 x1) : EqRel R x0 x1
:= zig_cons R (reflexivity _) zig.
Definition zag_to_eqrel {X : Type} (R : Relation X)
{x0 x1 : X} (zag : R x1 x0) : EqRel R x0 x1
:= zag_cons R (reflexivity _) zag.
(** ** [EqRel R] is an equivalence relation. We saw reflexivity above. *)
Global Instance transitive_eqrel {X : Type} (R : Relation X)
: Transitive (EqRel R).
Proof.
intros x0 x1 x2 rho01 [m zzs].
revert x1 x2 rho01 zzs.
induction m as [|m IH]; intros.
- by induction zzs.
- destruct zzs as [x [zzs [zig|zag]]].
+ exact (zig_cons R (IH _ _ rho01 zzs) zig).
+ exact (zag_cons R (IH _ _ rho01 zzs) zag).
Defined.
Global Instance symmetric_eqrel {X : Type} (R : Relation X)
: Symmetric (EqRel R).
Proof.
intros x0 x1 [n zzs]; revert x0 x1 zzs.
induction n as [|n IH].
- intros ? ? p; exact (0%nat; p^).
- intros ? ? [x [zzs zorz]].
transitivity x.
2: by apply IH.
destruct zorz as [zig|zag].
+ exact (zag_to_eqrel R zig).
+ exact (zig_to_eqrel R zag).
Defined.
(** To check whether a map respects [EqRel R], we just need to check that it respects [R]. *)
Definition eqrel_generator {X Y : Type}
(R : Relation X) (Q : Relation Y) (f : X -> Y)
: (forall x0 x1, R x0 x1 -> Q (f x0) (f x1))
-> (forall x0 x1, EqRel R x0 x1 -> EqRel Q (f x0) (f x1)).
Proof.
intros f_resp x0 x1 [n zz].
(* we need a free endpoint before inducting on [n] *)
revert dependent x1.
induction n as [|n IH].
1: intros; by induction zz.
intros x1 [x [zz [zig|zag]]].
- exact (zig_cons _ (IH _ zz) (f_resp _ _ zig)).
- exact (zag_cons _ (IH _ zz) (f_resp _ _ zag)).
Defined.
(** TODO do we use this? *)
Definition MEqRel {X : Type} (R : Relation X) (x0 x1 : X) : Type
:= merely (EqRel R x0 x1).
Definition zig_to_meqrel {X : Type} (R : Relation X)
: forall x0 x1, R x0 x1 -> MEqRel R x0 x1
:= fun _ _ rho => tr (zig_to_eqrel R rho).
Definition zag_to_meqrel {X : Type} (R : Relation X) {x0 x1 : X}
(zag : R x1 x0) : MEqRel R x0 x1
:= tr (zag_to_eqrel R zag).
Global Instance reflexive_meqrel {X : Type} (R : Relation X)
: Reflexive (MEqRel R) := fun _ => tr (0%nat; idpath).
Global Instance transitive_meqrel {X : Type} (R : Relation X)
: Transitive (MEqRel R).
Proof.
Proof.
intros x0 x1 x2 rho01 rho12; strip_truncations.
destruct rho12 as [m zzs].
revert x1 x2 rho01 zzs.
induction m as [|m IH]; intros.
- induction zzs.
exact (tr rho01).
- destruct zzs as [x [zzs [zig|zag]]];
pose proof (IHz := IH _ _ rho01 zzs); strip_truncations.
+ exact (tr (zig_cons R IHz zig)).
+ exact (tr (zag_cons R IHz zag)).
Defined.
Global Instance symmetric_meqrel {X : Type} (R : Relation X)
: Symmetric (MEqRel R).
Proof.
intros x0 x1; apply Trunc_rec; intros [n zzs].
revert x0 x1 zzs.
induction n as [|n IH].
- intros ? ? p; exact (tr (0%nat; p^)).
- intros ? ? [x [zzs zorz]].
transitivity x.
2: by apply IH.
destruct zorz as [zig|zag].
+ exact (tr (zag_to_eqrel R zig)).
+ exact (tr (zig_to_eqrel R zag)).
Defined.
(** todo: Now rewrite HigherExt.v to use this notion. *)
|