Index

Symbols

1

2 3

A

abstract category, [1] ACLat Agda algebra (examples) group algebraic lattice

application morphism arity Arrow arrow category associative law ATP (v)

B

BLat Boolean algebra

Boolean algebra homomorphism bound object terminal object

C

cartesian closed category Cat category category (examples) 1 (one object) 2 (two objects) 3 (three objects) ACLat (algebraic complete lattices) BLat (Boolean lattices); CLat (complete lattices); Cat (small categories) Fin (finite sets) Grph (graphs), [1], [2] HLat (Heyting lattices); Lat (lattices); Mon (monoids) Par (partial functions) Pos (posets), [1] Rel (relational structures) Set (sets), [1] arrow category comma category presheaf slice category Δ (finite ordinals) category of categories, [1] category of small categories CCC CiC CLat

cocone codomain domain, [1] colimit Comma comma category commutative diagram, [1], [2] compact element complete lattice complete lattice homomorphism component composition, [1] of functions of graphs of morphisms of relations concatenation concrete category, [1] cone consecutive functions, [1] chain of consecutive morphisms constant functor constant natural transformation contravariant embedding contravariant powerset functor coproduct, [1] Coq covariant embedding covariant powerset functor Curry-Howard correspondence

D

degeneracy map dependent type diagram (formally) (informally) directed graph

domain codomain, [1] dual category opposite category duality

E

edge set edges functor endofunctor, [1] endomorphism, [1] epimorphism, [1] equivalence of categories equivalent categories equivalent categories equivalence of categories ER essentially surjective on objects

ETT evaluation functor, [1] evaluation natural transformation existential image functor, [1] exponential, [1] exponential graph exponential object (examples) Grph` Pos Set extensional

F

face map faithful functor Fin finite ordinals finite ordinals, Δ simplex category free algebra, [1] free monoid Kleene closure free object initial object

full embedding full functor full subcategory fully faithful functor function extensionality functor, [1] functor (examples) (covariant) powerset function existential image functor universal image functor functor category, [1]

G

generalized element, [1] global element point graph directed

graph morphism, [1] group, [1] Grph

H

Heyting algebra Heyting algebra homomorphism HLat

hom set morphisms homomorphism (examples) Mon (monoids)

I

identity law identity morphism impredicative indexing category initial object free object

intensional internal reflection isomorphism, [1], [2] ITP (v) ITT

K

Kleene closure free monoid

L

large category Lat lattice lattice homomorphism

Lean legs (of a diagram) limit locally small category, [1], [2]

M

metaprogram Mon monoid, [1] monoid homomorphism monomorphism, [1], [2] monotone function, [1]

morphism (examples) Grph (graphs) identity morphism category morphisms hom set

N

natural isomorphism naturally isomorphic natural transformation, [1]

naturality condition naturally isomorphic natural isomorphism NuPRL

O

opposite category dual category

P

Par parallel functor parallel morphism parallel morphisms partial function total function point global element

polymorphic function Pos poset, [1], [2] predicative presheaf, [1] product, [1] product morphism proof tactic

R

reflection Rel relation, [1]

relational product relational structure representable functor

S

self-dual self-dual category Set signature simplex category finite ordinals, Δ

simplicial identities simplicial set Slice slice category small category, [1], [2] source natural transformation source vertex

T

target natural transformation target vertex terminal object bound object

topos total function partial function TT

U

UIP underlying set functor

universal image functor, [1] universal mapping property universal property, [1]

V

vertex source target

vertex set vertices functor

Y

Yoneda embedding

Yoneda's Lemma