Theorems · Definition · category theory
CategoryTheory.ReflQuiv.of
(C : Type u) → [CategoryTheory.ReflQuiver C] → CategoryTheory.ReflQuiv
Construct a bundled ReflQuiv from the underlying type and the typeclass.
- Defined in
- Mathlib.CategoryTheory.Category.ReflQuiv
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- CategoryTheory.ReflQuiver
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.ReflQuiverstatement and proof · cited by 64
- CategoryTheory.ReflQuivstatement · cited by 28
- CategoryTheory.Bundled.ofproof · cited by 6
Cited by12
Results whose statement or proof uses this declaration.
- CategoryTheory.ReflQuiv.forgetproof · cited by 14
- SSet.oneTruncation₂proof · cited by 8
- CategoryTheory.ReflQuiv.adj_homEquivstatement and proof · cited by 0
- CategoryTheory.ReflQuiv.adj_unit_appstatement · cited by 0
- SSet.OneTruncation₂.ofNerve₂statement · cited by 0
- CategoryTheory.ReflQuiv.forget_objstatement · cited by 0
- CategoryTheory.ReflQuiv.isoOfEquivstatement · cited by 0
- CategoryTheory.ReflQuiv.isoOfQuivIsostatement · cited by 0
- CategoryTheory.ReflQuiv.of_valstatement · cited by 0
- SSet.oneTruncation₂_objstatement · cited by 0
- CategoryTheory.ReflQuiv.adj.unit.map_app_eqstatement · cited by 0
- CategoryTheory.ReflPrefunctor.toFunctorstatement and proof · cited by 0