mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
21 lines
No EOL
869 B
TeX
21 lines
No EOL
869 B
TeX
\section*{Appendix}
|
||
\begin{frame}[t, fragile, blank]{App: Category Theory in Agda}{Setoid-enriched Categories}
|
||
\begin{minted}{agda}
|
||
record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
|
||
field
|
||
Obj : Set o
|
||
_⇒_ : Obj → Obj → Set ℓ
|
||
_≈_ : ∀ {A B} → (A ⇒ B) → (A ⇒ B) → Set e
|
||
|
||
id : ∀ {A} → (A ⇒ A)
|
||
_∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)
|
||
|
||
field
|
||
assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D}
|
||
→ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
|
||
identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
|
||
identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
|
||
equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
|
||
∘-resp-≈ : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i
|
||
\end{minted}
|
||
\end{frame} |