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₂).

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

• 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)

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 CategoryTheory.UnbundledHom.bundledHom (c : Type u → Type u) (hom : ⦃α β : Type u⦄ → c α → c β → (α → β) → Prop) [𝒞 : CategoryTheory.UnbundledHom hom] : CategoryTheory.BundledHom fun α β Iα Iβ => Subtype (hom α β Iα Iβ)

def CategoryTheory.UnbundledHom.mkHasForget₂ {c : Type u → Type u} {hom : ⦃α β : Type u⦄ → c α → c β → (α → β) → Prop} [𝒞 : CategoryTheory.UnbundledHom hom] {c' : Type u → Type u} {hom' : ⦃α β : Type u⦄ → c' α → c' β → (α → β) → Prop} [𝒞' : CategoryTheory.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) : CategoryTheory.HasForget₂ (CategoryTheory.Bundled c) (CategoryTheory.Bundled c')

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