Category instances for structures that use unbundled homs

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

@[deprecated "The preferred method for talking about concrete categories is to implement the category manually and then provide the `ConcreteCategory` instance on top of this. See `ConcreteCategory/Basic.lean`" (since := "2025-11-17")]

class CategoryTheory.UnbundledHom {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → (α → β) → Prop) : Prop

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 α → β.

• hom_id {α : Type u} (ia : c α) : hom ia ia id
• hom_comp {α β γ : Type u} {Iα : c α} {Iβ : c β} {Iγ : c γ} {g : β → γ} {f : α → β} : hom Iβ Iγ g → hom Iα Iβ f → hom Iα Iγ (g ∘ f)

instance CategoryTheory.UnbundledHom.bundledHom (c : Type u → Type u) (hom : ⦃α β : Type u⦄ → c α → c β → (α → β) → Prop) [𝒞 : UnbundledHom hom] : BundledHom fun (α β : Type u) (Iα : c α) (Iβ : c β) => Subtype (hom Iα Iβ)

Equations

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

def CategoryTheory.UnbundledHom.mkHasForget₂ {c : Type u → Type u} {hom : ⦃α β : Type u⦄ → c α → c β → (α → β) → Prop} [𝒞 : UnbundledHom hom] {c' : Type u → Type u} {hom' : ⦃α β : Type u⦄ → c' α → c' β → (α → β) → Prop} [𝒞' : UnbundledHom hom'] (obj : ⦃α : Type u⦄ → c α → c' α) (map : ∀ ⦃α β : Type u⦄ ⦃Iα : c α⦄ ⦃Iβ : c β⦄ ⦃f : α → β⦄, hom Iα Iβ f → hom' (obj Iα) (obj Iβ) f) : HasForget₂ (Bundled c) (Bundled c')

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

Equations

• CategoryTheory.UnbundledHom.mkHasForget₂ obj map = CategoryTheory.BundledHom.mkHasForget₂ obj (fun {X Y : CategoryTheory.Bundled c} (f : X ⟶ Y) => ⟨↑f, ⋯⟩) ⋯