Structures · Category theory
CategoryTheory.IsReflexivePair
The pair f g : A ⟶ B is reflexive if there is a morphism B ⟶ A which is a section for both.
- Shape
- 2 explicit arguments · adds common_section'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CategoryTheory.Monad.Algebra
How is a type an instance?
Loading the hierarchy index…
Assumed by22
- CategoryTheory.commonSection
- CategoryTheory.Limits.ofIsReflexivePair
- CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer
- CategoryTheory.section_comp_left
- CategoryTheory.section_comp_right
- CategoryTheory.IsReflexivePair.common_section
- CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom
- CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv
- CategoryTheory.IsReflexivePair.common_section'
- CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair
- CategoryTheory.Limits.HasReflexiveCoequalizers.has_coeq
- CategoryTheory.IsReflexivePair.swap
- CategoryTheory.commonSection.congr_simp
- CategoryTheory.section_comp_left_assoc
- CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc
- CategoryTheory.Limits.ofIsReflexivePair_hasColimit_of_hasCoequalizer
- CategoryTheory.Limits.ofIsReflexivePair_map_right
- CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out
- CategoryTheory.Limits.inclusionWalkingReflexivePairOfIsReflexivePairIso
- CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc
- CategoryTheory.Limits.ofIsReflexivePair_map_left
- CategoryTheory.section_comp_right_assoc
Ancestors0
No ancestors.