Mathlib Map

Structures · Category theory

CategoryTheory.CopyDiscardCategory

Category where objects have compatible copy and discard operations.

Defined in
Mathlib.CategoryTheory.CopyDiscardCategory.Basic
Shape
One type argument · adds comonObj, isCommComonObj, copy_tensor, discard_tensor, copy_unit, discard_unit

Extends1

Extended by1

Forgetful instances

Every CategoryTheory.CopyDiscardCategory is also a

Concrete types that are instances2

  • CategoryTheory.WideSubcategory
  • SFinKer

How is a type an instance?

Loading the hierarchy index…

Assumed by11

Ancestors3