@[reducible, inline]

abbrev Category.Fun (A B : Sort u) : Sort u

A synonym for ->, acting as a carrier for the standard category of Sets.

Think of Fun A B as analogous to the textbook "Set(A, B)".

Equations

• Category.Fun A B = (A → B)

instance Category.Fun.category : Category Category.Fun

Naturally, we can form a category of types (in a given universe) and functions between them.

For Type, we get the usual category of sets.

For Prop, we instead get the category of propositions and implications.

Equations

• Category.Fun.category = Category.mk @Category.Fun.category.proof_1 @Category.Fun.category.proof_2 @Category.Fun.category.proof_3

@[simp]

def Category.Fun.comp_apply {A B C : Sort u_1} {f : Category.Fun A B} {g : Category.Fun B C} {x : A} : (f ≫ g) x = g (f x)

Equations

• ⋯ = ⋯

structure Category.BiMorphism {OA : Sort u_1} {OB : Sort u_2} (A : OA → OA → Sort v_A) (B : OB → OB → Sort v_B) (X Y : OA ×' OB) : Sort (max (max 1 v_A) v_B)

In essence, this is just two morphisms, one in each category.

• fst : A X.fst Y.fst
• snd : B X.snd Y.snd

theorem Category.BiMorphism.ext {OA : Sort u_1} {OB : Sort u_2} {A : OA → OA → Sort v_A} {B : OB → OB → Sort v_B} {X Y : OA ×' OB} {x y : (A ⨂ B) X Y} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

def Category.«term_⨂_» : Lean.TrailingParserDescr

Equations

• Category.«term_⨂_» = Lean.ParserDescr.trailingNode `Category.«term_⨂_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨂ ") (Lean.ParserDescr.cat `term 100))

class Category.BiCategory {OA : Sort u_1} {OB : Sort u_2} (A : OA → OA → Sort v_A) (B : OB → OB → Sort v_B) [𝓐 : Category A] [𝓑 : Category B] extends Category (A ⨂ B) : Sort (max (max (max (max 1 u_1) u_2) v_A) v_B)

A category structure on A ⨂ B which is compatible with the underlying categories.

There's a natural way of turning A ⨂ B into the morphisms of a category, which behaves particularly nicely pointwise. This class captures that this category is being used, allowing us to do reasoning beyond that of a plain category.

This is a bit of a "Lean hack" allowing us to assume that the category instance for A ⨂ B has particular properties relating it to A and B individually.

• id : {x : OA ×' OB} → (A ⨂ B) x x
• comp : {a b c : OA ×' OB} → (A ⨂ B) a b → (A ⨂ B) b c → (A ⨂ B) a c
• pre_id : ∀ {x x_1 : OA ×' OB} {f : (A ⨂ B) x x_1}, Category.Struct.id ≫ f = f
• post_id : ∀ {x x_1 : OA ×' OB} {f : (A ⨂ B) x x_1}, f ≫ Category.Struct.id = f
• comp_assoc : ∀ {a b c d : OA ×' OB} {f : (A ⨂ B) a b} {g : (A ⨂ B) b c} {h : (A ⨂ B) c d}, (f ≫ g) ≫ h = f ≫ g ≫ h
• bi_compat_id : ∀ {x : OA ×' OB}, Category.Struct.id = { fst := Category.Struct.id, snd := Category.Struct.id }
• bi_compat_comp : ∀ {x y z : OA ×' OB} {f : (A ⨂ B) x y} {g : (A ⨂ B) y z}, f ≫ g = { fst := f.fst ≫ g.fst, snd := f.snd ≫ g.snd }

instance Category.BiMorphism.bicategory {OA : Sort u_1} {OB : Sort u_2} {A : OA → OA → Sort v_A} {B : OB → OB → Sort v_B} [𝓐 : Category A] [𝓑 : Category B] : Category.BiCategory A B

Equations

• Category.BiMorphism.bicategory = Category.BiCategory.mk ⋯ ⋯

structure Category.Op {O_A : Sort u_1} (A : O_A → O_A → Sort v_A) (x y : O_A) : Sort (max 1 v_A)

The opposite of a given type of morphisms, i.e. morphisms in the reverse direction.

We define this as an opaque struct for better wieldiness.

• unop : A y x

theorem Category.Op.ext {O_A : Sort u_1} {A : O_A → O_A → Sort v_A} {x y : O_A} {x✝ y✝ : Category.Op A x y} (unop : x✝.unop = y✝.unop) : x✝ = y✝

def Category.Op.op {O_A : Sort u_1} {A : O_A → O_A → Sort v_A} {x y : O_A} (f : A x y) : Category.Op A y x

A morphism can be treated as an opposite morphism, with the direction reversed.

Equations

• Category.Op.op f = { unop := f }

@[simp]

theorem Category.Op.eq_iff_unop_eq {O_A : Sort u_1} {A : O_A → O_A → Sort v_A} {x y : O_A} (f g : Category.Op A x y) : f = g ↔ f.unop = g.unop

To show that two opposite morphisms are the same, show that the underlying morphisms are.

@[simp]

theorem Category.Op.op_unop {O_A : Sort u_1} {A : O_A → O_A → Sort v_A} {x y : O_A} (f : A x y) : (Category.Op.op f).unop = f

instance Category.Op.categoryStruct {O_A : Sort u_1} {A : O_A → O_A → Sort v_A} [𝓐 : Category.Struct A] : Category.Struct (Category.Op A)

The category of opposites.

Because of our morphism centric approach, rather than looking at "the opposite category", we instead look at "the category of opposite morphisms".

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Category.Op.unop_id_eq_id {O_A : Sort u_1} {A : O_A → O_A → Sort v_A} [𝓐 : Category.Struct A] {x : O_A} : Category.Struct.id.unop = Category.Struct.id

The opposite identity is in fact just the identity.

@[simp]

theorem Category.Op.unop_comp_eq_comp_unop {O_A : Sort u_1} {A : O_A → O_A → Sort v_A} [𝓐 : Category.Struct A] {x y z : O_A} (f : Category.Op A x y) (g : Category.Op A y z) : (f ≫ g).unop = g.unop ≫ f.unop

Composing two opposite morphisms is just backwards composition.

instance Category.Op.category {O_A : Sort u_1} {A : O_A → O_A → Sort v_A} [𝓐 : Category A] : Category (Category.Op A)

Naturally, opposite morphisms form a category, if the underlying morphisms do.

Equations

• Category.Op.category = Category.mk ⋯ ⋯ ⋯