computer engineer • phd candidate • real life person
A category consists of the following data:
A type of objects
For
any
two
objects
A
and
B
,
a
type
of
morphisms
from
A
to
B
For
each
object
A
,
an
identity
morphism
from
A
to
A
,
called
id
for
any
two
morphisms
f
from
B
to
C
and
g
from
A
to
B
,
a
morphism
f ∘ g
from
A
to
C
called
the
composite
of
f
and
g
with the additional conditions that composition be associative and unital :
(f ∘ g)
∘
h
=
f
∘
(g ∘ h)
f
∘
id
=
f
id
∘
f
=
f
This can be readily formalized as a record type in Agda:
record Category (o ℓ : Level) : Set (suc (o ⊔ ℓ)) where
infix 4 _⇒_
infixr 9 _∘_
field
Obj : Set o
_⇒_ : Obj → Obj → Set ℓ
id : {A : Obj} → A ⇒ A
_∘_ : {A B C : Obj} → B ⇒ C → A ⇒ B → A ⇒ C
assoc
: {A B C D : Obj}
{f : A ⇒ B}
{g : B ⇒ C}
{h : C ⇒ D}
→ (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)
identityˡ : {A B : Obj} {f : A ⇒ B} → id ∘ f ≡ f
identityʳ : {A B : Obj} {f : A ⇒ B} → f ∘ id ≡ f
The record is parameterized by two universe levels, one for the type of objects and one for the type of morphisms.
This
formalization,
though
satisfyingly
close
to
what
might
be
found
in
the
first
chapter
of
a
category
theory
textbook,
has
a
serious
shortcoming,
having
to
do
with
the
notion
of
equality
of
morphisms.
While,
in
many
settings,
mathematicians
would
be
happy
to
take
equality
for
granted
as
a
primitive
notion
coming
from
the
underlying
logic,
working
in
an
intensional
type
theory
(like the one Agda is based on)
usually
requires
a
bit
more
care.
It
is
impossible,
in
general,
to
construct
a
term
witnessing
the
propositional
equality
of
two
functions,
even
if
they
can
be
shown
to
have
the
same
output
for
every
possible
input,
i.e.
to
be
extensionally
equal.
In
other
words,
it
is
not
possible
to
go
from
∀ x → f x ≡ g x
to
f ≡ g
.
This
makes
it
pretty
hard
to
do
anything
useful
in
a
category
where
the
morphisms
are
some
kind
of
function
(read: most categories)
because
there
will
be
morphisms
that
should
be
equal
but
are
not
provably
so.
Nonetheless, in this blog post, we will explore what happens when we keep the definition as is, and save the actual solution for another post.
As
you
may
know,
a
functor
is
structure-preserving
map
between
categories.
Each
object
in
C
is
sent
to
an
object
of
D
,
and
each
morphism
in
C
from
A
to
B
is
sent
to
some
morphism
in
D
from
F
A
to
F
B
.
What
structure
is
preserved?
Well,
the
identity
morphism
on
an
object
is
sent
to
the
identity
morphism
on
the
image
of
that
object,
and
the
composition
(in
C
)
of
two
morphisms
is
sent
to
the
composition
in
(in
D
)
of
their
images:
record Functor
{o₁ o₂ ℓ₁ ℓ₂ : Level}
(C : Category o₁ ℓ₁)
(D : Category o₂ ℓ₂)
: Set (o₁ ⊔ o₂ ⊔ ℓ₁ ⊔ ℓ₂) where
private
module C = Category C
module D = Category D
field
F₀ : C.Obj → D.Obj
F₁ : {X Y : C.Obj} → X C.⇒ Y → F₀ X D.⇒ F₀ Y
identity : {X : C.Obj} → F₁ (C.id {X}) ≡ D.id {F₀ X}
homomorphism
: {X Y Z : C.Obj}
{f : X C.⇒ Y}
{g : Y C.⇒ Z}
→ F₁ (g C.∘ f) ≡ F₁ g D.∘ F₁ f
Here, we use named modules to refer independently to the operations of the source and target categories. The record contains four fields: a function on objects, a function on morphisms, and the two preservation laws (together called functoriality). Once again, the Agda formalization fits the textbook definition line-by-line.
Let's define two categories with the goal of constructing a functor between them.
We'd
like
to
define
a
category
of
functions
between
finite
sets,
while
avoiding
the
awkward
business
of
directly
defining
sets
and
elements.
Often
enough,
the
mathematically
interesting
content
of
a
set
is
not
which
elements
it
has,
but
rather
how
many
elements
it
has
(also known as
cardinality
).
Since
any
two
finite
sets
of
the
same
cardinality
are
isomorphic,
we
may
as
well
let
the
type
of
objects
in
our
category
be
the
natural
numbers,
and
let
a
natural
number
n
represent
all
the
finite
sets
with
n
elements.
This
category
is
what
John
Baez
and
others
in
the
world
of
applied
category
theory
often
refer
to
when
they
say
FinSet.
It
turns
out
that,
in
a
precise
sense,
this
category
is
indeed
equivalent
to
the
(proper)
category
of
finite
sets.
It
is
called
Nat
here
to
avoid
any
confusion:
Nat : Category 0ℓ 0ℓ
Nat = record
{ Obj = ℕ
; _⇒_ = λ n m → Vec (Fin m) n
; id = tabulate id
; _∘_ = λ f g → map (lookup f) g
; assoc = λ {f = f} {g h} → assoc f g h
; identityˡ = identityˡ
; identityʳ = identityʳ
}
Notice
the
type
of
morphisms.
A
morphism
from
n
to
m
is
a
length-
n
vector
of
Fin
m
s.
Essentially,
it's
a
table
specifying
which
of
the
0
to
m
-
1
elements
each
of
the
n
elements
of
the
domain
get
mapped
to.
Representing
the
morphisms
as
purely
data
(i.e. avoiding function types)
means
we
can
actually
construct
morphism
equality
proofs,
even
when
morphisms
are
defined
using
actual
functions
(e.g. via
tabulate
).
The
unitality
and
associativity
proofs
are
simple,
but
not
completely
trivial.
Here
is
associativity:
assoc
: {A B C D : ℕ}
(f : Vec (Fin B) A)
(g : Vec (Fin C) B)
(h : Vec (Fin D) C)
→ map (lookup (map (lookup h) g)) f ≡ map (lookup h) (map (lookup g) f)
assoc f g h = begin
map (lookup (map (lookup h) g)) f ≡⟨ map-cong (λ x → lookup-map x _ g) f ⟩
map (lookup h ∘ lookup g) f ≡⟨ map-∘ (lookup h) (lookup g) f ⟩
map (lookup h) (map (lookup g) f) ∎
The unitality proofs are left as an exercise to the reader.
Even
easier
to
define
is
the
category
of
types
and
functions.
It
is
named
Sets
by
virtue
of
it
being
the
direct
type-theoretic
analog
of
Set
,
the
ubiquitous
category
of
sets.
Associativity
and
unitality
are
proved
by
refl
exivity:
Sets : (o : Level) → Category (suc o) o
Sets o = record
{ Obj = Set o
; _⇒_ = λ A B → A → B
; id = id
; _∘_ = λ f g → f ∘ g
; assoc = refl
; identityˡ = refl
; identityʳ = refl
}
Include : Functor Nat (Sets 0ℓ)
Include = record
{ F₀ = Fin
; F₁ = lookup
; identity = ?
; homomorphism = ?
}
Constructing a functor between them requires function extensionality:
Include : Functor Nat (Sets 0ℓ)
Include = record
{ F₀ = Fin
; F₁ = lookup
; identity = funext (lookup∘tabulate id)
; homomorphism = λ {f = f} {g} → funext λ x → lookup-map x (lookup g) f
}
Coming soon! (I hope)
A sensible definition of a preorder is a type equipped with a relation that is reflexive and transitive: