module CatDef where
open import Basics
Mor : (A : Set₁) → Set₁
Mor A = A → A → Set
record Cat : Set₂ where
field
Obj : Set₁
_⇒_ : Obj → Obj → Set
_≈_ : ∀ {M N} → Rel (M ⇒ N)
isEq : ∀ {M N} → isEquivalence (M ⇒ N) _≈_
id : ∀ {N} → N ⇒ N
_⊚_ : ∀ {M N O} → M ⇒ N → N ⇒ O → M ⇒ O
id1 : ∀ {M N} → (f : M ⇒ N) → (id ⊚ f) ≈ f
id2 : ∀ {M N} → (g : M ⇒ N) → (g ⊚ id) ≈ g
asso : ∀ {M N O P} → (f : M ⇒ N) → (g : N ⇒ O) → (h : O ⇒ P) → ((f ⊚ g) ⊚ h) ≈ (f ⊚ (g ⊚ h))
resp : ∀ {M N O} → (_⊚_ {M}{N}{O}) Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
open Cat public
record Terminal (ℂ : Cat) : Set₁ where
field
Ter : Obj ℂ
A→T : (A : Obj ℂ) → (_⇒_ ℂ) A Ter
uni : (A : Obj ℂ) → (f : (_⇒_ ℂ) A Ter) → (_≈_ ℂ) (A→T A) f
record Initial (ℂ : Cat) : Set₁ where
field
Ini : Obj ℂ
I→A : (A : Obj ℂ) → (_⇒_ ℂ) Ini A
uni : (A : Obj ℂ) → (f : (_⇒_ ℂ) Ini A) → (_≈_ ℂ) (I→A A) f
record Product {ℂ : Cat}(X Y : Obj ℂ) : Set₁ where
field
X×Y : Obj ℂ
π₁ : (_⇒_ ℂ) X×Y X
π₂ : (_⇒_ ℂ) X×Y Y
〈_,_〉 : ∀ {Z} → (_⇒_ ℂ) Z X → (_⇒_ ℂ) Z Y → (_⇒_ ℂ) Z X×Y
c₁ : ∀ {Z}{f : (_⇒_ ℂ) Z X}{g : (_⇒_ ℂ) Z Y} → (_≈_ ℂ)((_⊚_ ℂ) 〈 f , g 〉 π₁) f
c₂ : ∀ {Z}{f : (_⇒_ ℂ) Z X}{g : (_⇒_ ℂ) Z Y} → (_≈_ ℂ)((_⊚_ ℂ) 〈 f , g 〉 π₂) g
uni : ∀ {Z}{f : (_⇒_ ℂ) Z X}{g : (_⇒_ ℂ) Z Y}{h : (_⇒_ ℂ) Z X×Y} → (_≈_ ℂ)((_⊚_ ℂ) h π₁) f → (_≈_ ℂ) ((_⊚_ ℂ) h π₂) g → (_≈_ ℂ) 〈 f , g 〉 h
open Product public
record CarCat : Set₂ where
field
Ucat : Cat
UTer : Terminal Ucat
UProd : (X Y : Obj Ucat) → Product {Ucat} X Y
open CarCat public
record Coproduct {ℂ : Cat}(X Y : Obj ℂ) : Set₁ where
field
X+Y : Obj ℂ
i₁ : (_⇒_ ℂ) X X+Y
i₂ : (_⇒_ ℂ) Y X+Y
[[_,_]] : ∀ {Z} → (_⇒_ ℂ) X Z → (_⇒_ ℂ) Y Z → (_⇒_ ℂ) X+Y Z
c₁' : ∀ {Z}{f : (_⇒_ ℂ) X Z}{g : (_⇒_ ℂ) Y Z} → (_≈_ ℂ)((_⊚_ ℂ) i₁ [[ f , g ]]) f
c₂' : ∀ {Z}{f : (_⇒_ ℂ) X Z}{g : (_⇒_ ℂ) Y Z} → (_≈_ ℂ)((_⊚_ ℂ) i₂ [[ f , g ]]) g
uni' : ∀ {Z}{f : (_⇒_ ℂ) X Z}{g : (_⇒_ ℂ) Y Z}{h : (_⇒_ ℂ) X+Y Z} → (_≈_ ℂ)((_⊚_ ℂ) i₁ h) f → (_≈_ ℂ) ((_⊚_ ℂ) i₂ h) g → (_≈_ ℂ) [[ f , g ]] h
record CoCarCat : Set₂ where
field
UCcat : Cat
UIni : Initial UCcat
UCoProd : (X Y : Obj UCcat) → Coproduct {UCcat} X Y
open CoCarCat public
Pair⇒ : {ℂ : CarCat} → (X Y Z W : Obj (Ucat ℂ)) → (XZ : ((_⇒_ (Ucat ℂ)) X Z)) → (YW : ((_⇒_ (Ucat ℂ)) Y W)) → (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ X Y)) (X×Y (UProd ℂ Z W))
Pair⇒ {ℂ} X Y Z W XZ YW = (〈_,_〉 (UProd ℂ Z W)) ((_⊚_ (Ucat ℂ)) (π₁ (UProd ℂ X Y)) XZ) ((_⊚_ (Ucat ℂ)) (π₂ (UProd ℂ X Y)) YW)
record Exp {ℂ : CarCat}(X Y : Obj (Ucat ℂ)) : Set₁ where
field
Yˣ : Obj (Ucat ℂ)
app : (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ Yˣ X)) Y
curr : (Z : Obj (Ucat ℂ)) → (f : (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ Z X)) Y) → ((_⇒_ (Ucat ℂ)) Z Yˣ)
comm : (Z : Obj (Ucat ℂ)) → (f : (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ Z X)) Y) → (_≈_ (Ucat ℂ))((_⊚_ (Ucat ℂ)) (Pair⇒ {ℂ} Z X Yˣ X (curr Z f) ((id (Ucat ℂ)) {X})) app) f
univ : (Z : Obj (Ucat ℂ)) → (f : (_⇒_ (Ucat ℂ)) (X×Y (UProd ℂ Z X)) Y) → (h : (_⇒_ (Ucat ℂ)) Z Yˣ) → (_≈_ (Ucat ℂ))((_⊚_ (Ucat ℂ)) (Pair⇒ {ℂ} Z X Yˣ X h ((id (Ucat ℂ)) {X})) app) f → (_≈_ (Ucat ℂ)) (curr Z f) h
open Exp public
record CCC : Set₂ where
field
CarC : CarCat
exp : (X Y : Obj (Ucat CarC)) → Exp {CarC} X Y
record Functor (C : Cat) (D : Cat) : Set₁ where
field
onObj : (Obj C) → (Obj D)
onMor : (X Y : Obj C) → (f : (_⇒_ C) X Y) → (_⇒_ D) (onObj X)(onObj Y)
res≈ : (X Y : Obj C) → (f g : (_⇒_ C) X Y) → (_≈_ C) f g → (_≈_ D) (onMor X Y f) (onMor X Y g)
onId : (X : Obj C) → (_≈_ D) (onMor X X ((id C) {X})) ((id D) {onObj X})
onComp : (X Y Z : Obj C) → (f : (_⇒_ C) X Y) → (g : (_⇒_ C) Y Z) → (_≈_ D) ((_⊚_ D) (onMor X Y f) (onMor Y Z g)) (onMor X Z ((_⊚_ C) f g))
open Functor public
record Adjoint (C D : Cat) (F : Functor C D)(G : Functor D C) : Set₁ where
field
counit : (X : Obj D) → (_⇒_ D) ((onObj F) ((onObj G) X)) X
f̂ : (X : Obj D) → (Y : Obj C) → (_⇒_ D) ((onObj F) Y) X → (_⇒_ C) Y ((onObj G) X)
f̂ε : (X : Obj D) → (Y : Obj C) → (f : ((_⇒_ D) ((onObj F) Y) X)) → (_≈_ D) ((_⊚_ D) ((onMor F) Y ((onObj G) X) (f̂ X Y f)) (counit X)) f
unif̂ : (X : Obj D) → (Y : Obj C) → (f : ((_⇒_ D) ((onObj F) Y) X)) → (g : (_⇒_ C) Y ((onObj G) X)) → (_≈_ D) ((_⊚_ D) ((onMor F) Y ((onObj G) X) g) (counit X)) f → (_≈_ C) g (f̂ X Y f)
open Adjoint public
record Pullbacks (C : Cat) (X Y Z : Obj C) (f : (_⇒_ C) X Z)(g : (_⇒_ C) Y Z) : Set₁ where
field
X⊗Y : Obj C
X⊗Y→X : (_⇒_ C) X⊗Y X
X⊗Y→Y : (_⇒_ C) X⊗Y Y
f∘p₁≡g∘p₂ : (_≈_ C) ((_⊚_ C) X⊗Y→X f) ((_⊚_ C) X⊗Y→Y g)
W→X⊗Y : (W : Obj C) → (f' : (_⇒_ C) W X) → (g' : (_⇒_ C) W Y) → (_≈_ C) ((_⊚_ C) f' f) ((_⊚_ C) g' g) → (_⇒_ C) W X⊗Y
WXY₁ : (W : Obj C) → (f' : (_⇒_ C) W X) → (g' : (_⇒_ C) W Y) → (f'g' : (_≈_ C) ((_⊚_ C) f' f) ((_⊚_ C) g' g)) → (_≈_ C) ((_⊚_ C) (W→X⊗Y W f' g' f'g') X⊗Y→X) f'
WXY₂ : (W : Obj C) → (f' : (_⇒_ C) W X) → (g' : (_⇒_ C) W Y) → (f'g' : (_≈_ C) ((_⊚_ C) f' f) ((_⊚_ C) g' g)) → (_≈_ C) ((_⊚_ C) (W→X⊗Y W f' g' f'g') X⊗Y→Y) g'
W↠X⊗Y : (W : Obj C) → (f' : (_⇒_ C) W X) → (g' : (_⇒_ C) W Y) → (f'g' : (_≈_ C) ((_⊚_ C) f' f) ((_⊚_ C) g' g)) → (h : (_⇒_ C) W X⊗Y) → (_≈_ C) ((_⊚_ C) h X⊗Y→X) f' → (_≈_ C) ((_⊚_ C) h X⊗Y→Y) g'
→ (_≈_ C) (W→X⊗Y W f' g' f'g') h
open Pullbacks public
record CatPull (C : Cat) : Set₁ where
field
Pulls : (X Y Z : Obj C) → (f : (_⇒_ C) X Z) → (g : (_⇒_ C) Y Z) → Pullbacks C X Y Z f g
record Iso {C : Cat}(X Y : Obj C) : Set where
field
liso : (_⇒_ C) X Y
riso : (_⇒_ C) Y X
idisl : (_≈_ C) ((_⊚_ C) liso riso) ((id C) {X})
idisr : (_≈_ C) ((_⊚_ C) riso liso) ((id C) {Y})
record Nat (C D : Cat) (F G : Functor C D) : Set₁ where
field
trf : (X : Obj C) → (_⇒_ D) ((onObj F) X) ((onObj G) X)
ntsq : (X Y : Obj C) → (f : (_⇒_ C) X Y) → (_≈_ D) ((_⊚_ D) (trf X) ((onMor G) X Y f)) ((_⊚_ D) ((onMor F) X Y f) (trf Y))