Structures · Category theory
CategoryTheory.HasPullbacksOfInclusions
A category has pullback of inclusions if it has all pullbacks along coproduct injections.
- Defined in
- Mathlib.CategoryTheory.Extensive
- Shape
- One type argument · adds hasPullbackInl
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- CompHausLike
How is a type an instance?
Loading the hierarchy index…
Assumed by7
- CategoryTheory.finitaryExtensive_of_preserves_and_reflects
- CategoryTheory.finitaryExtensive_of_reflective
- CategoryTheory.finitaryExtensive_iff_of_isTerminal
- CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr'
- CategoryTheory.HasPullbacksOfInclusions.hasPullbackInl
- CategoryTheory.HasPullbacksOfInclusions.preservesPullbackInl'
- CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr
Ancestors0
No ancestors.