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₂).
@[class]
structure
category_theory.unbundled_hom
{c : Type u → Type u} :
(Π {α β : Type u}, c α → c β → (α → β) → Prop) → Type
- hom_id : ∀ {α : Type ?} (ia : c α), hom ia ia id
- hom_comp : ∀ {α β γ : Type ?} {Iα : c α} {Iβ : c β} {Iγ : c γ} {g : β → γ} {f : α → β}, hom Iβ Iγ g → hom Iα Iβ f → hom Iα 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 α → β.
@[instance]
def
category_theory.unbundled_hom.bundled_hom
(c : Type u → Type 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β))
Equations
- category_theory.unbundled_hom.bundled_hom c hom = {to_fun := λ (_x _x_1 : Type u) (_x_2 : c _x) (_x_3 : c _x_1), subtype.val, id := λ (α : Type u) (Iα : c α), ⟨id α, _⟩, comp := λ (_x _x_1 _x_2 : Type u) (_x_3 : c _x) (_x_4 : c _x_1) (_x_5 : c _x_2) (g : subtype (hom _x_4 _x_5)) (f : subtype (hom _x_3 _x_4)), ⟨g.val ∘ f.val, _⟩, hom_ext := _, id_to_fun := _, comp_to_fun := _}
def
category_theory.unbundled_hom.mk_has_forget₂
{c : Type u → Type u}
{hom : Π ⦃α β : Type u⦄, c α → c β → (α → β) → Prop}
[𝒞 : category_theory.unbundled_hom hom]
{c' : Type u → Type u}
{hom' : Π ⦃α β : Type u⦄, c' α → c' β → (α → β) → Prop}
[𝒞' : category_theory.unbundled_hom hom']
(obj : Π ⦃α : Type u⦄, c α → c' α) :
(∀ ⦃α β : Type u⦄ ⦃Iα : c α⦄ ⦃Iβ : c β⦄ ⦃f : α → β⦄, hom Iα Iβ f → hom' (obj Iα) (obj Iβ) f) → category_theory.has_forget₂ (category_theory.bundled c) (category_theory.bundled c')
A custom constructor for forgetful functor between concrete categories defined using unbundled_hom.
Equations
- category_theory.unbundled_hom.mk_has_forget₂ obj map = category_theory.bundled_hom.mk_has_forget₂ obj (λ (X Y : category_theory.bundled c) (f : X ⟶ Y), ⟨f.val, _⟩) _