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
|
||| Product of setoids
module Data.Setoid.Pair
import Data.Setoid.Definition
import Data.Setoid.Either
%default total
||| Binary relation conjunction
public export
record And {A,B : Type} (p : Rel A) (q : Rel B) (xy1, xy2 : (A, B)) where
constructor MkAnd
fst : p (fst xy1) (fst xy2)
snd : q (snd xy1) (snd xy2)
||| Product of setoids
public export
Pair : (a,b : Setoid) -> Setoid
Pair a b = MkSetoid
{ U = (U a, U b)
, equivalence = MkEquivalence
{ relation = a.equivalence.relation `And` b.equivalence.relation
, reflexive = \xy => MkAnd
(a.equivalence.reflexive $ fst xy)
(b.equivalence.reflexive $ snd xy)
, symmetric = \xy1,xy2,prf => MkAnd
(a.equivalence.symmetric (fst xy1) (fst xy2) prf.fst)
(b.equivalence.symmetric (snd xy1) (snd xy2) prf.snd)
, transitive = \xy1,xy2,xy3,prf1,prf2 => MkAnd
(a.equivalence.transitive (fst xy1) (fst xy2) (fst xy3) prf1.fst prf2.fst)
(b.equivalence.transitive (snd xy1) (snd xy2) (snd xy3) prf1.snd prf2.snd)
}
}
||| Left projection setoid homomorphism
public export
(.fst) : {0 a,b : Setoid} -> Pair a b ~> a
(.fst) = MkSetoidHomomorphism
{ H = Builtin.fst
, homomorphic = \xy1,xy2,prf => prf.fst
}
||| Right projection setoid homomorphism
public export
(.snd) : {0 a,b : Setoid} -> Pair a b ~> b
(.snd) = MkSetoidHomomorphism
{ H = Builtin.snd
, homomorphic = \xy1,xy2,prf => prf.snd
}
||| Setoid homomorphism constructor
public export
tuple : {0 a,b,c : Setoid} -> c ~> a -> c ~> b -> c ~> Pair a b
tuple f g = MkSetoidHomomorphism
{ H = \z => (f.H z, g.H z)
, homomorphic = \z1,z2,prf => MkAnd
(f.homomorphic z1 z2 prf)
(g.homomorphic z1 z2 prf)
}
||| Unique value of type unit
public export
unitVal : (x,y : Unit) -> x = y
unitVal () () = Refl
||| The unique setoid map into the terminal type
public export
unit : {a : Setoid} -> a ~> cast Unit
unit = MkSetoidHomomorphism
{ H = const ()
, homomorphic = \_,_,_ => unitVal () ()
}
||| The constant function as a setoid morphism
public export
const : {a,b : Setoid} -> (x : U b) -> a ~> b
const x = mate (Prelude.const x) . unit
||| Setoid homomorphism constructor
public export
bimap : {a,b,c,d : Setoid} -> c ~> a -> d ~> b -> Pair c d ~> Pair a b
bimap f g = tuple (f . (.fst)) (g . (.snd))
-- Distribution of products over sums, degenerate case:
||| Function underlying the bijection 2 x s <~> s + s
public export
distributeFunction : {s : Setoid} -> (Bool, U s) -> (U s `Either` U s)
distributeFunction (False, x) = Left x
distributeFunction (True , x) = Right x
||| States: the function underlying the bijection 2 x s <~> s + s is a setoid homomorphism
public export
distributeHomomorphism : {s : Setoid} ->
SetoidHomomorphism ((cast Bool) `Pair` s) (s `Either` s)
(distributeFunction {s})
distributeHomomorphism (b1,x1) (b2,x2) prf =
case prf.fst of
Refl => case b2 of
False => Left prf.snd
True => Right prf.snd
||| Setoid homomorphism involved in the bijection 2 x s <~> s + s
public export
distribute : {s : Setoid} -> ((cast Bool) `Pair` s) ~> (s `Either` s)
distribute = MkSetoidHomomorphism
{ H = distributeFunction
, homomorphic = distributeHomomorphism
}
public export
pairIso : {a,b,c,d : Setoid} -> (a <~> c) -> (b <~> d) -> (Pair a b <~> Pair c d)
pairIso ac bd = MkIsomorphism (bimap ac.Fwd bd.Fwd) (bimap ac.Bwd bd.Bwd)
(IsIsomorphism (\(x,y) => MkAnd (ac.Iso.BwdFwdId x) (bd.Iso.BwdFwdId y))
(\(x,y) => MkAnd (ac.Iso.FwdBwdId x) (bd.Iso.FwdBwdId y)))
|
