Documentation

Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom

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) :
  • hom_id : ∀ {α : Type u} (ia : c α), hom ia ia id
  • hom_comp : ∀ {α β γ : Type u} { : c α} { : c β} { : c γ} {g : βγ} {f : αβ}, hom ghom fhom (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 α → β.

Instances
    instance CategoryTheory.UnbundledHom.bundledHom (c : Type u → Type u) (hom : α β : Type u⦄ → c αc β(αβ) → Prop) [𝒞 : CategoryTheory.UnbundledHom hom] :
    CategoryTheory.BundledHom fun α β => Subtype (hom α β )
    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⦄ → : c α⦄ → : c β⦄ → f : αβ⦄ → hom α β fhom' α β (obj α ) (obj β ) f) :

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

    Instances For