Theorems · Inductive type · category theory
CategoryTheory.Pairwise
Type v → Type v
An inductive type representing either a single term of a type ι, or a pair of terms.
We use this as the objects of a category to describe the sheaf condition.
- Defined in
- Mathlib.CategoryTheory.Category.Pairwise
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by95
Results whose statement or proof uses this declaration.
- CategoryTheory.Pairwise.diagramstatement and proof · cited by 30
- TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorstatement · cited by 12
- TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInversestatement · cited by 12
- CategoryTheory.Pairwise.coconestatement · cited by 8
- CategoryTheory.Pairwise.casesOnstatement and proof · cited by 6
- CategoryTheory.Pairwise.Homstatement · cited by 4
- TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivstatement · cited by 4
- CategoryTheory.Pairwise.diagramObjstatement and proof · cited by 3
- TopCat.Presheaf.objPairwiseOfFamilystatement and proof · cited by 3
- TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIsostatement · cited by 3
- TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObjstatement · cited by 3
- TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObjstatement and proof · cited by 3