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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
||| Basic definition and notation for indexed setoids
module Data.Setoid.Indexed.Definition
import public Control.Relation
import public Data.Setoid.Definition
import Syntax.PreorderReasoning.Setoid
infix 5 ~>, ~~>, <~>
%ambiguity_depth 4
%default total
public export
record IndexedEquivalence (0 A : Type) (0 B : A -> Type) where
constructor MkIndexedEquivalence
0 relation : (i : A) -> Rel (B i)
reflexive : (i : A) -> (x : B i) -> relation i x x
symmetric : (i : A) -> (x, y : B i) -> relation i x y -> relation i y x
transitive : (i : A) -> (x, y, z : B i) -> relation i x y -> relation i y z -> relation i x z
public export
EqualIndexedEquivalence : (0 b : a -> Type) -> IndexedEquivalence a b
EqualIndexedEquivalence b = MkIndexedEquivalence
{ relation = \_ => (===)
, reflexive = \_, _ => Refl
, symmetric = \_, _, _ => symmetric
, transitive = \_, _, _, _ => transitive
}
public export
record IndexedSetoid (0 A : Type) where
constructor MkIndexedSetoid
0 U : A -> Type
equivalence : IndexedEquivalence A U
||| Creates an indexed setoid from a family of setoids.
public export
bundle : (a -> Setoid) -> IndexedSetoid a
bundle x = MkIndexedSetoid
{ U = U . x
, equivalence = MkIndexedEquivalence
{ relation = \i => (x i).equivalence.relation
, reflexive = \i => (x i).equivalence.reflexive
, symmetric = \i => (x i).equivalence.symmetric
, transitive = \i => (x i).equivalence.transitive
}
}
||| Extracts the setoid at an index.
public export
index : IndexedSetoid a -> (i : a) -> Setoid
index x i = MkSetoid
{ U = x.U i
, equivalence = MkEquivalence
{ relation = x.equivalence.relation i
, reflexive = x.equivalence.reflexive i
, symmetric = x.equivalence.symmetric i
, transitive = x.equivalence.transitive i
}
}
public export
reindex : (a -> b) -> IndexedSetoid b -> IndexedSetoid a
reindex f x = bundle (index x . f)
namespace ToSetoid
public export
irrelevantCast : (0 b : a -> Type) -> IndexedSetoid a
irrelevantCast b = MkIndexedSetoid { U = b , equivalence = EqualIndexedEquivalence b }
public export
Cast (a -> Type) (IndexedSetoid a) where
cast b = irrelevantCast b
public export 0
IndexedSetoidHomomorphism : (x, y : IndexedSetoid a) -> (f : (i : a) -> x.U i -> y.U i) -> Type
IndexedSetoidHomomorphism x y f = (i : a) -> (a, b : x.U i)
-> x.equivalence.relation i a b -> (y.equivalence.relation i `on` f i) a b
public export
record (~>) {0 a : Type} (x, y : IndexedSetoid a) where
constructor MkIndexedSetoidHomomorphism
H : (i : a) -> x.U i -> y.U i
homomorphic : IndexedSetoidHomomorphism x y H
public export
mate : {y : IndexedSetoid a} -> ((i : a) -> x i -> y.U i) -> irrelevantCast x ~> y
mate f = MkIndexedSetoidHomomorphism
{ H = f
, homomorphic = \_, _, _, Refl => y.equivalence.reflexive _ _
}
||| Identity IndexedSetoid homomorphism
public export
id : (0 x : IndexedSetoid a) -> x ~> x
id x = MkIndexedSetoidHomomorphism { H = \_ => id , homomorphic = \_, _, _ => id }
||| Composition of IndexedSetoidSetoid homomorphisms
public export
(.) : {0 x, y, z : IndexedSetoid a} -> y ~> z -> x ~> y -> x ~> z
f . g = MkIndexedSetoidHomomorphism
{ H = \i => f.H i . g.H i
, homomorphic = \i, _, _ => f.homomorphic i _ _ . g.homomorphic i _ _
}
public export 0
pwEq : (0 x, y : IndexedSetoid a) -> Rel (x ~> y)
pwEq x y f g = (i : a) -> (u : x.U i) -> y.equivalence.relation i (f.H i u) (g.H i u)
public export
(~~>) : (x, y : IndexedSetoid a) -> Setoid
x ~~> y = MkSetoid (x ~> y) $ MkEquivalence
{ relation = pwEq x y
, reflexive = \f, i, u => y.equivalence.reflexive i (f.H i u)
, symmetric = \f, g, eq, i, u => y.equivalence.symmetric i _ _ (eq i u)
, transitive = \f, g, h, eq, eq', i, u => y.equivalence.transitive i _ _ _ (eq i u) (eq' i u)
}
public export
post : {0 x, y, z : IndexedSetoid a} -> y ~> z -> (x ~~> y) ~> (x ~~> z)
post f = MkSetoidHomomorphism
{ H = (.) f
, homomorphic = \_, _, eq, i, u => f.homomorphic i _ _ $ eq i u
}
||| Two indexed setoid homomorphism are each other's inverses
public export
record IndexedIsomorphism {0 a : Type} {0 x, y : IndexedSetoid a} (Fwd : x ~> y) (Bwd : y ~> x) where
constructor IsIndexedIsomorphism
BwdFwdId : (x ~~> x).equivalence.relation (Bwd . Fwd) (id x)
FwdBwdId : (y ~~> y).equivalence.relation (Fwd . Bwd) (id y)
||| Indexed setoid isomorphism
namespace Indexed
public export
record (<~>) {0 a : Type} (0 x, y : IndexedSetoid a) where
constructor MkIsomorphism
Fwd : x ~> y
Bwd : y ~> x
isomorphic : IndexedIsomorphism Fwd Bwd
||| Identity (isomorphism _)
public export
refl : {x : IndexedSetoid a} -> x <~> x
refl = MkIsomorphism
{ Fwd = id x
, Bwd = id x
, isomorphic = IsIndexedIsomorphism
{ BwdFwdId = \_, _ => x.equivalence.reflexive _ _
, FwdBwdId = \_, _ => x.equivalence.reflexive _ _
}
}
||| Reverse an isomorphism
public export
sym : Indexed.(<~>) a b -> b <~> a
sym iso = MkIsomorphism
{ Fwd = iso.Bwd
, Bwd = iso.Fwd
, isomorphic = IsIndexedIsomorphism
{ BwdFwdId = iso.isomorphic.FwdBwdId
, FwdBwdId = iso.isomorphic.BwdFwdId
}
}
||| Compose isomorphisms
public export
trans : {x, z : IndexedSetoid a} -> x <~> y -> y <~> z -> x <~> z
trans iso iso' = MkIsomorphism
{ Fwd = iso'.Fwd . iso.Fwd
, Bwd = iso.Bwd . iso'.Bwd
, isomorphic = IsIndexedIsomorphism
{ BwdFwdId = \i, u => CalcWith (index x i) $
|~ iso.Bwd.H i (iso'.Bwd.H i (iso'.Fwd.H i (iso.Fwd.H i u)))
~~ iso.Bwd.H i (iso.Fwd.H i u) ...(iso.Bwd.homomorphic i _ _ $ iso'.isomorphic.BwdFwdId i _)
~~ u ...(iso.isomorphic.BwdFwdId i u)
, FwdBwdId = \i, u => CalcWith (index z i) $
|~ iso'.Fwd.H i (iso.Fwd.H i (iso.Bwd.H i (iso'.Bwd.H i u)))
~~ iso'.Fwd.H i (iso'.Bwd.H i u) ...(iso'.Fwd.homomorphic i _ _ $ iso.isomorphic.FwdBwdId i _)
~~ u ...(iso'.isomorphic.FwdBwdId i u)
}
}
public export
IndexedIsoEquivalence : Equivalence (IndexedSetoid a)
IndexedIsoEquivalence = MkEquivalence
{ relation = \x, y => x <~> y
, reflexive = \_ => refl
, symmetric = \_, _ => sym
, transitive = \_, _, _ => trans
}
||| Quotient a type by a function into an indexed setoid
|||
||| Instance of the more general coequaliser of two indexed setoid morphisms.
public export
Quotient : forall x . (y : IndexedSetoid a) -> ((i : a) -> x i -> y.U i) -> IndexedSetoid a
Quotient y f = MkIndexedSetoid
{ U = x
, equivalence = MkIndexedEquivalence
{ relation = \i => y.equivalence.relation i `on` f i
, reflexive = \i, _ => y.equivalence.reflexive i _
, symmetric = \i, _, _ => y.equivalence.symmetric i _ _
, transitive = \i, _, _, _ => y.equivalence.transitive i _ _ _
}
}
|
