Documentation

Mathlib.CategoryTheory.WithTerminal.FinCategory

WithTerminal C and WithInitial C are finite whenever C is #

If C has finitely many objects, then so do WithTerminal C and WithInitial C, and likewise if C has finitely many morphisms as well.

source
🔸 coverage
def CategoryTheory.WithTerminal.optionEquiv (C : Type u) :
Option C ≃ WithTerminal C

The equivalence between Option C and WithTerminal C (they are both the type C plus an extra object none or star).

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance CategoryTheory.WithTerminal.instFintype (C : Type u) [Fintype C] :
    Fintype (WithTerminal C)
    source
    🔸 coverage
    @[implicit_reducible]
    instance CategoryTheory.WithTerminal.instFinCategory (C : Type u) [SmallCategory C] [FinCategory C] :
    FinCategory (WithTerminal C)
    source
    🔸 coverage
    def CategoryTheory.WithInitial.optionEquiv (C : Type u) :
    Option C ≃ WithInitial C

    The equivalence between Option C and WithInitial C (they are both the type C plus an extra object none or star).

    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance CategoryTheory.WithInitial.instFintype (C : Type u) [Fintype C] :
      Fintype (WithInitial C)
      source
      🔸 coverage
      @[implicit_reducible]
      instance CategoryTheory.WithInitial.instFinCategory (C : Type u) [SmallCategory C] [FinCategory C] :
      FinCategory (WithInitial C)