-
Notifications
You must be signed in to change notification settings - Fork 0
/
Preorder.agda
166 lines (151 loc) · 13.9 KB
/
Preorder.agda
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
------------------------------------------------------------------------
-- This file contains the definition of a preorder as a category with --
-- additional properties. --
------------------------------------------------------------------------
module Category.Preorder where
open import Level renaming (suc to lsuc)
open import Data.Empty
open import Setoid.Total
open import Category.Category
open import Equality.Eq
record PO {l : Level} : Set (lsuc l) where
field
-- The underlying category.
ℙ : Cat {l}
-- The preorder axiom.
POax : ∀{A B}{f g : el (Hom ℙ A B)} → ⟨ Hom ℙ A B ⟩[ f ≡ g ]
open PO public renaming (ℙ to po-cat)
-- A PO with 4 objects.
module 4PO where
-- The objects.
data 4Obj {l : Level} : Set l where
i₁ : 4Obj
i₂ : 4Obj
i₃ : 4Obj
i₄ : 4Obj
-- The PreHom.
data 4PHom {l : Level} : 4Obj {l} → 4Obj {l} → Set l where
id₁ : 4PHom i₁ i₁
f₁ : 4PHom i₁ i₂
f₂ : 4PHom i₁ i₃
id₂ : 4PHom i₂ i₂
f₃ : 4PHom i₂ i₄
id₃ : 4PHom i₃ i₃
f₄ : 4PHom i₃ i₄
f₅ : 4PHom i₁ i₄
id₄ : 4PHom i₄ i₄
-- The Hom.
4Hom : {l : Level} → 4Obj {l} → 4Obj {l} → Setoid {l}
4Hom i₁ i₁ = record { el = 4PHom i₁ i₁; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom i₁ i₂ = record { el = 4PHom i₁ i₂; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom i₁ i₃ = record { el = 4PHom i₁ i₃; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom i₁ i₄ = record { el = 4PHom i₁ i₄; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom i₂ i₂ = record { el = 4PHom i₂ i₂; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom i₂ i₄ = record { el = 4PHom i₂ i₄; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom i₃ i₃ = record { el = 4PHom i₃ i₃; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom i₃ i₄ = record { el = 4PHom i₃ i₄; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom i₄ i₄ = record { el = 4PHom i₄ i₄; eq = λ a b → a ≅ b; eqRpf = isEqRel }
4Hom _ _ = EmptySetoid
4Comp : {l : Level}{a b c : 4Obj {l}} → BinSetoidFun (4Hom a b) (4Hom b c) (4Hom a c)
4Comp {_} {i₁} {i₂} {i₁} = record { appT = λ x → record { appT = λ x₁ → id₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₁} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₂} {i₁} {i₂} = record { appT = λ x → record { appT = λ x₁ → id₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₁} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₂} {i₁} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₁} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₃} {i₂} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₁} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₃} {i₁} {i₃} = record { appT = λ x → record { appT = λ x₁ → id₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₁} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₄} {i₁} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₄} {i₂} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₄} {i₁} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₄} {i₁} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₄} {i₃} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₄} {i₁} {i₄} = record { appT = λ x → record { appT = λ x₁ → ⊥-poly-elim x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₄} {i₄} {i₃} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₄} {i₄} {i₂} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₄} {i₄} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₄} {i₃} {i₄} = record { appT = λ x → record { appT = λ x₁ → id₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₄} {i₃} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₄} {i₃} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₄} {i₂} {i₄} = record { appT = λ x → record { appT = λ x₁ → id₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₄} {i₂} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₄} {i₂} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₃} {i₄} {i₃} = record { appT = λ x → record { appT = λ x₁ → id₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₄} {i₂} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₄} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₃} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₃} {i₂} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₃} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₂} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₂} {i₃} = record { appT = λ x → record { appT = λ x₁ → id₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₃} {i₂} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₃} {i₄} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₄} {i₃} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₄} {i₂} = record { appT = λ x → record { appT = λ x₁ → id₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₄} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₃} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₃} {i₂} = record { appT = λ x → record { appT = λ x₁ → id₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₃} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₂} {i₂} {i₄} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₂} {i₃} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₂} {i₂} = record { appT = λ x → record { appT = λ x₁ → id₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₂} {i₃} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₂} {i₄} {i₄} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
4Comp {_} {i₁} {i₄} {i₃} = record { appT = λ x → record { appT = λ x₁ → f₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₄} {i₂} = record { appT = λ x → record { appT = λ x₁ → f₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₄} {i₁} = record { appT = λ x → record { appT = λ x₁ → id₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₃} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₅; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₃} {i₂} = record { appT = λ x → record { appT = λ x₁ → f₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₃} {i₁} = record { appT = λ x → record { appT = λ x₁ → id₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₂} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₅; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₂} {i₃} = record { appT = λ x → record { appT = λ x₁ → f₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₂} {i₂} = record { appT = λ x → record { appT = λ x₁ → f₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₃} {i₃} = record { appT = λ x → record { appT = λ x₁ → f₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {_} {i₁} {i₄} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₅; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
4Comp {l} {i₁} {i₁} {c} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refPf (eqRpf (4Hom i₁ c)) {x₂} }
4Comp {l} {i₂} {i₂} {c} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refPf (eqRpf (4Hom i₂ c)) {x₂} }
4Comp {l} {i₃} {i₃} {c} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refPf (eqRpf (4Hom i₃ c)) {x₂} }
4Comp {l} {i₄} {i₄} {c} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refPf (eqRpf (4Hom i₄ c)) {x₂} }
4Id : {l : Level}{A : 4Obj {l}} → el (4Hom A A)
4Id {_}{i₁} = id₁
4Id {_}{i₂} = id₂
4Id {_}{i₃} = id₃
4Id {_}{i₄} = id₄
4PO-ax : ∀{l}{A B : 4Obj {l}}{f g : el (4Hom A B)} → eq (4Hom A B) f g
4PO-ax {A = i₁} {i₁} {id₁} {id₁} = refl
4PO-ax {A = i₁} {i₂} {f₁} {f₁} = refl
4PO-ax {A = i₁} {i₃} {f₂} {f₂} = refl
4PO-ax {A = i₁} {i₄} {f₅} {f₅} = refl
4PO-ax {A = i₂} {i₂} {id₂} {id₂} = refl
4PO-ax {A = i₂} {i₄} {f₃} {f₃} = refl
4PO-ax {A = i₃} {i₃} {id₃} {id₃} = refl
4PO-ax {A = i₃} {i₄} {f₄} {f₄} = refl
4PO-ax {A = i₄} {i₄} {id₄} {id₄} = refl
4PO-ax {A = i₂} {i₁} {f} = ⊥-poly-elim f
4PO-ax {A = i₃} {i₁} {f} = ⊥-poly-elim f
4PO-ax {A = i₄} {i₁} {f} = ⊥-poly-elim f
4PO-ax {A = i₃} {i₂} {f} = ⊥-poly-elim f
4PO-ax {A = i₄} {i₂} {f} = ⊥-poly-elim f
4PO-ax {A = i₂} {i₃} {f} = ⊥-poly-elim f
4PO-ax {A = i₄} {i₃} {f} = ⊥-poly-elim f
4AssocPf : ∀{l}{A B C D : 4Obj {l}} {f : el (4Hom A B)} {g : el (4Hom B C)}{h : el (4Hom C D)}
→ ⟨ 4Hom A D ⟩[ f ○[ 4Comp {l} {A}{B}{D} ] (g ○[ 4Comp {l}{B}{C}{D} ] h) ≡ (f ○[ 4Comp {l} {A}{B}{C} ] g) ○[ 4Comp {l}{A}{C}{D} ] h ]
4AssocPf {l}{A}{B}{C}{D} {f}{g} = 4PO-ax {l} {A} {D}
4IdPF : {l : Level}{A B : 4Obj {l}} {f : el (4Hom A B)}
→ ⟨ 4Hom A B ⟩[ (4Id {l}{A}) ○[ 4Comp {l}{A}{A}{B} ] f ≡ f ○[ 4Comp {l}{A}{B}{B} ] (4Id {l}{B}) ]
4IdPF {l}{A}{B}{f} = 4PO-ax {l} {A} {B}
-- We have a category.
4cat : {l : Level} → Cat {l}
4cat {l} = record { Obj = 4Obj {l};
Hom = 4Hom;
comp = λ {A} {B} {C} → 4Comp {l} {A}{B}{C};
id = λ {A} → 4Id {l}{A};
assocPf = λ {A} {B} {C} {D} {f} {g} {h} → 4AssocPf {l}{A}{B}{C}{D}{f}{g}{h};
idPfCom = λ {A} {B} {f} → 4IdPF {l}{A}{B}{f};
idPf = λ {A} {B} {f} → 4PO-ax {l} {A} {B}}
-- We have a preorder.
4po : {l : Level} → PO {l}
4po {l} = record { ℙ = 4cat;
POax = λ {A} {B} {f} {g} → 4PO-ax {l} {A} {B} {f} {g} }