Structures · Category theory
CategoryTheory.Limits.HasCoreflexiveEqualizers
C has coreflexive equalizers if it has equalizers for every coreflexive pair.
- Shape
- One type argument · adds has_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
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 by12
- CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv
- CategoryTheory.LiftRightAdjoint.constructRightAdjointObj
- CategoryTheory.isLeftAdjoint_triangle_lift_comonadic
- CategoryTheory.LiftRightAdjoint.constructRightAdjoint
- CategoryTheory.isLeftAdjoint_triangle_lift
- CategoryTheory.Comonad.comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms
- CategoryTheory.Limits.hasEqualizer_of_common_retraction
- CategoryTheory.Limits.HasCoreflexiveEqualizers.has_eq
- CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply
- CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply
- CategoryTheory.isLeftAdjoint_square_lift
- CategoryTheory.isLeftAdjoint_square_lift_comonadic
Ancestors0
No ancestors.