mathlib documentation


Category instances for structures that use unbundled homs #

This file provides basic infrastructure to define concrete categories using unbundled homs (see class unbundled_hom), and define forgetful functors between them (see unbundled_hom.mk_has_forget₂).

structure category_theory.unbundled_hom {c : Type uType u} (hom : Π {α β : Type u}, c αc β(α → β) → Prop) :
  • hom_id : ∀ {α : Type ?} (ia : c α), hom ia ia id
  • hom_comp : ∀ {α β γ : Type ?} {Iα : c α} {Iβ : c β} {Iγ : c γ} {g : β → γ} {f : α → β}, hom Iβ ghom Iα fhom Iα (g f)

A class for unbundled homs used to define a category. hom must take two types α, β and instances of the corresponding structures, and return a predicate on α → β.

def category_theory.unbundled_hom.bundled_hom (c : Type uType u) (hom : Π ⦃α β : Type u⦄, c αc β(α → β) → Prop) [𝒞 : category_theory.unbundled_hom hom] :
category_theory.bundled_hom (λ (α β : Type u) (Iα : c α) (Iβ : c β), subtype (hom Iα Iβ))
def category_theory.unbundled_hom.mk_has_forget₂ {c : Type uType u} {hom : Π ⦃α β : Type u⦄, c αc β(α → β) → Prop} [𝒞 : category_theory.unbundled_hom hom] {c' : Type uType u} {hom' : Π ⦃α β : Type u⦄, c' αc' β(α → β) → Prop} [𝒞' : category_theory.unbundled_hom hom'] (obj : Π ⦃α : Type u⦄, c αc' α) (map : ∀ ⦃α β : Type u⦄ ⦃Iα : c α⦄ ⦃Iβ : c β⦄ ⦃f : α → β⦄, hom Iα fhom' (obj Iα) (obj Iβ) f) :

A custom constructor for forgetful functor between concrete categories defined using unbundled_hom.