Structures · Category theory
CategoryTheory.CanonicallyOverClass
X.CanonicallyOverClass S is the typeclass containing the data of a
structure morphism X ↘ S : X ⟶ S,
and that S is (uniquely) inferable from the structure of X.
- Shape
- 2 explicit arguments
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by7
- CategoryTheory.CanonicallyOverClass.toOverClass
- CategoryTheory.CanonicallyOverClass.over_def
- CategoryTheory.CanonicallyOverClass.instOverClass
- CategoryTheory.instHomIsOverOfIsOverTower_1
- CategoryTheory.CanonicallyOverClass.Simps.over
- CategoryTheory.instIsOverTower_2
- CategoryTheory.instHomIsOverOfIsOverTower