Structures · Category theory
CategoryTheory.Limits.HasReflexiveCoequalizers
C has reflexive coequalizers if it has coequalizers for every reflexive pair.
- Shape
- One type argument · adds has_coeq
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 by13
- CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj
- CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv
- CategoryTheory.isRightAdjoint_triangle_lift
- CategoryTheory.LiftLeftAdjoint.constructLeftAdjoint
- CategoryTheory.isRightAdjoint_triangle_lift_monadic
- CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj.congr_simp
- CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms
- CategoryTheory.Limits.hasCoequalizer_of_common_section
- CategoryTheory.isRightAdjoint_square_lift
- CategoryTheory.Limits.HasReflexiveCoequalizers.has_coeq
- CategoryTheory.isRightAdjoint_square_lift_monadic
- CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply
- CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply
Ancestors0
No ancestors.