instance Category.ofSort : Category (Sort u)

A generalization of the category of types to apply to any sort.

The main reason for this generalization is to define the category of propositions, but we also get wacky higher types for free as well.

Equations

• Category.ofSort = Category.mk @Category.ofSort.proof_1 @Category.ofSort.proof_2 @Category.ofSort.proof_3

@[reducible, inline]

abbrev Category.ofProp : Category Prop

The category whose objects are propositions, and whose morphisms are implications.

Equations

• Category.ofProp = Category.ofSort

@[reducible, inline]

abbrev Category.ofType : Category Type

The category whose objects are types, and whose morphisms are functions.

This is our version of SET in textbook category theory.

Equations

• Category.ofType = Category.ofSort

structure Opposite (α : Sort u_1) : Sort (max 1 u_1)

A carrier for the opposite of a category.

• unop : α

def Category.Op {O : Sort u_1} (C : Category O) : Category (Opposite O)

Give a category, explicitly construct the opposite category.

This provides a way to get the canonical instance of the opposite category, allowing us to easily use the fact that we've used the standard instance in proving things.

This allows us to lean on opposites when defining categorical constructs.

Equations

• C.Op = Category.mk ⋯ ⋯ ⋯

instance instCategoryOpposite {O : Sort u_1} [C : Category O] : Category (Opposite O)

The canonical instance for the opposite category.

Equations

• instCategoryOpposite = C.Op