ReflQuiv

📁 Source: Mathlib/CategoryTheory/Category/ReflQuiv.lean

Statistics

Metric	Count
Definitions FreeRefl, homMk, induction, instCategory, instUnique, instUniqueHom, lift', mk, morphismPropertyHomMk, quotientFunctor, FreeReflRel, freeRefl, freeReflMap, freeReflNatTrans, toFreeRefl, toFunctor, ReflQuiv, adj, homEquiv, category, forget, forgetToQuiv, instCoeSortType, instInhabited, instReflQuiverα, isoOfEquiv, isoOfQuivIso, of, toQuiv	29
Theorems functor_ext, homMk_id, hom_induction, instFullPathsQuotientFunctor, instSubsingletonHomOfUnique, lift'_map, lift'_obj, lift_map, lift_obj, lift_spec, lift_unique', morphismPropertyHomMk_homMk, morphismProperty_eq_top, multiplicativeClosure_morphismPropertyHomMk, quotientFunctor_map_cons, quotientFunctor_map_id, quotientFunctor_map_nil, freeReflMap_map, freeReflMap_naturality, freeReflMap_obj, freeRefl_map, freeRefl_obj, toFreeRefl_map, toFreeRefl_obj, comp_app_eq, homEquiv_apply, homEquiv_naturality_left_symm, homEquiv_naturality_right, homEquiv_symm_apply, map_app_eq, adj_counit_app, adj_homEquiv, adj_unit_app, comp_eq_comp, comp_map, comp_obj, forgetToQuiv_faithful, forgetToQuiv_map, forgetToQuiv_obj, forget_faithful, forget_forgetToQuiv, forget_map, forget_obj, id_eq_id, id_map, id_obj, of_val	47
Total	76

CategoryTheory

Definitions

Name	Category	Theorems
ReflQuiv 📖	CompOp	28 math math: SSet.oneTruncation₂_obj, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, ReflQuiv.adj_homEquiv, Cat.freeRefl_map, SSet.oneTruncation₂_map, ReflQuiv.id_map, ReflQuiv.adj_unit_app, ReflQuiv.comp_map, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, ReflQuiv.comp_eq_comp, ReflQuiv.forget_map, ReflQuiv.adj.unit.map_app_eq, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, ReflQuiv.forget_obj, ReflQuiv.forgetToQuiv_obj, ReflQuiv.comp_obj, ReflQuiv.forget_forgetToQuiv, SSet.Truncated.hoFunctor₂_naturality, ReflQuiv.adj_counit_app, ReflQuiv.forget.Faithful, ReflQuiv.forgetToQuiv_map, ReflQuiv.id_eq_id, ReflQuiv.id_obj, Cat.freeRefl_obj, ReflQuiv.adj.counit.comp_app_eq, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, ReflQuiv.forgetToQuiv.Faithful

CategoryTheory.Cat

Definitions

Name	Category	Theorems
FreeRefl 📖	CompOp	31 math math: freeRefl_map, CategoryTheory.ReflQuiv.adj.homEquiv_symm_apply, freeReflMap_obj, FreeRefl.lift_map, FreeRefl.homMk_id, FreeRefl.lift_spec, toFreeRefl_obj, FreeRefl.instFullPathsQuotientFunctor, FreeRefl.multiplicativeClosure_morphismPropertyHomMk, SSet.OneTruncation₂.HoRel₂.mk, SSet.Truncated.HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor, CategoryTheory.ReflQuiv.adj.unit.map_app_eq, FreeRefl.lift'_map, freeReflMap_naturality, FreeRefl.quotientFunctor_map_id, FreeRefl.quotientFunctor_map_nil, toFreeRefl_map, SSet.Truncated.hoFunctor₂_naturality, CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm, CategoryTheory.ReflQuiv.adj_counit_app, CategoryTheory.ReflQuiv.adj.homEquiv_apply, CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right, FreeRefl.lift'_obj, freeRefl_obj, FreeRefl.morphismProperty_eq_top, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, FreeRefl.instSubsingletonHomOfUnique, SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap, freeReflMap_map, FreeRefl.lift_obj, FreeRefl.quotientFunctor_map_cons
FreeReflRel 📖	CompData	—
freeRefl 📖	CompOp	8 math math: CategoryTheory.ReflQuiv.adj_homEquiv, freeRefl_map, CategoryTheory.ReflQuiv.adj_unit_app, CategoryTheory.ReflQuiv.adj.unit.map_app_eq, SSet.Truncated.hoFunctor₂_naturality, CategoryTheory.ReflQuiv.adj_counit_app, freeRefl_obj, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq
freeReflMap 📖	CompOp	5 math math: freeRefl_map, freeReflMap_obj, freeReflMap_naturality, CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm, freeReflMap_map
freeReflNatTrans 📖	CompOp	—
toFreeRefl 📖	CompOp	5 math math: CategoryTheory.ReflQuiv.adj_unit_app, FreeRefl.lift_spec, toFreeRefl_obj, toFreeRefl_map, CategoryTheory.ReflQuiv.adj.homEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeReflMap_map 📖	mathematical	—	CategoryTheory.Functor.map FreeRefl FreeRefl.instCategory freeReflMap FreeRefl.homMk Prefunctor.obj CategoryTheory.ReflQuiver.toQuiver CategoryTheory.ReflPrefunctor.toPrefunctor Prefunctor.map	—	—
freeReflMap_naturality 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Paths CategoryTheory.Paths.categoryPaths CategoryTheory.ReflQuiver.toQuiver FreeRefl FreeRefl.instCategory FreeRefl.quotientFunctor freeReflMap freeMap CategoryTheory.ReflPrefunctor.toPrefunctor	—	CategoryTheory.Paths.ext_functor
freeReflMap_obj 📖	mathematical	—	CategoryTheory.Functor.obj FreeRefl FreeRefl.instCategory freeReflMap Prefunctor.obj CategoryTheory.ReflQuiver.toQuiver CategoryTheory.ReflPrefunctor.toPrefunctor	—	—
freeRefl_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ReflQuiv CategoryTheory.ReflQuiv.category CategoryTheory.Cat category freeRefl CategoryTheory.Functor.toCatHom FreeRefl CategoryTheory.Bundled.α CategoryTheory.ReflQuiver CategoryTheory.ReflQuiv.instReflQuiverα FreeRefl.instCategory freeReflMap	—	—
freeRefl_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ReflQuiv CategoryTheory.ReflQuiv.category CategoryTheory.Cat category freeRefl of FreeRefl CategoryTheory.Bundled.α CategoryTheory.ReflQuiver CategoryTheory.ReflQuiv.instReflQuiverα FreeRefl.instCategory	—	—
toFreeRefl_map 📖	mathematical	—	Prefunctor.map CategoryTheory.ReflQuiver.toQuiver FreeRefl CategoryTheory.catToReflQuiver FreeRefl.instCategory CategoryTheory.ReflPrefunctor.toPrefunctor toFreeRefl FreeRefl.homMk	—	—
toFreeRefl_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.ReflQuiver.toQuiver FreeRefl CategoryTheory.catToReflQuiver FreeRefl.instCategory CategoryTheory.ReflPrefunctor.toPrefunctor toFreeRefl	—	—

CategoryTheory.Cat.FreeRefl

Definitions

Name	Category	Theorems
homMk 📖	CompOp	7 math math: lift_map, homMk_id, lift'_map, CategoryTheory.Cat.toFreeRefl_map, morphismPropertyHomMk_homMk, CategoryTheory.Cat.freeReflMap_map, quotientFunctor_map_cons
induction 📖	CompOp	—
instCategory 📖	CompOp	31 math math: CategoryTheory.Cat.freeRefl_map, CategoryTheory.ReflQuiv.adj.homEquiv_symm_apply, CategoryTheory.Cat.freeReflMap_obj, lift_map, homMk_id, lift_spec, CategoryTheory.Cat.toFreeRefl_obj, instFullPathsQuotientFunctor, multiplicativeClosure_morphismPropertyHomMk, SSet.OneTruncation₂.HoRel₂.mk, SSet.Truncated.HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor, CategoryTheory.ReflQuiv.adj.unit.map_app_eq, lift'_map, CategoryTheory.Cat.freeReflMap_naturality, quotientFunctor_map_id, quotientFunctor_map_nil, CategoryTheory.Cat.toFreeRefl_map, SSet.Truncated.hoFunctor₂_naturality, CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm, CategoryTheory.ReflQuiv.adj_counit_app, CategoryTheory.ReflQuiv.adj.homEquiv_apply, CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right, lift'_obj, CategoryTheory.Cat.freeRefl_obj, morphismProperty_eq_top, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, instSubsingletonHomOfUnique, SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap, CategoryTheory.Cat.freeReflMap_map, lift_obj, quotientFunctor_map_cons
instUnique 📖	CompOp	—
instUniqueHom 📖	CompOp	—
lift' 📖	CompOp	2 math math: lift'_map, lift'_obj
mk 📖	CompOp	—
morphismPropertyHomMk 📖	CompOp	3 math math: multiplicativeClosure_morphismPropertyHomMk, morphismPropertyHomMk_homMk, SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap
quotientFunctor 📖	CompOp	8 math math: instFullPathsQuotientFunctor, SSet.OneTruncation₂.HoRel₂.mk, CategoryTheory.ReflQuiv.adj.unit.map_app_eq, CategoryTheory.Cat.freeReflMap_naturality, quotientFunctor_map_id, quotientFunctor_map_nil, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, quotientFunctor_map_cons

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_ext 📖	—	CategoryTheory.Functor.obj CategoryTheory.Cat.FreeRefl instCategory CategoryTheory.Functor.map homMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—	lift_unique' CategoryTheory.Paths.ext_functor
homMk_id 📖	mathematical	—	homMk CategoryTheory.ReflQuiver.id CategoryTheory.CategoryStruct.id CategoryTheory.Cat.FreeRefl CategoryTheory.Category.toCategoryStruct instCategory	—	CategoryTheory.Quotient.sound
hom_induction 📖	—	homMk CategoryTheory.ReflQuiver.id CategoryTheory.CategoryStruct.comp CategoryTheory.Cat.FreeRefl CategoryTheory.Category.toCategoryStruct instCategory	—	—	CategoryTheory.Functor.map_surjective instFullPathsQuotientFunctor quotientFunctor_map_nil homMk_id
instFullPathsQuotientFunctor 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Paths CategoryTheory.Paths.categoryPaths CategoryTheory.ReflQuiver.toQuiver CategoryTheory.Cat.FreeRefl instCategory quotientFunctor	—	CategoryTheory.Quotient.full_functor
instSubsingletonHomOfUnique 📖	mathematical	Quiver.Hom CategoryTheory.ReflQuiver.toQuiver	CategoryTheory.Cat.FreeRefl CategoryTheory.catToReflQuiver instCategory	—	Unique.instSubsingleton unique_iff_subsingleton_and_nonempty
lift'_map 📖	mathematical	CategoryTheory.ReflQuiver.id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.map CategoryTheory.Cat.FreeRefl instCategory lift' homMk	—	lift_map
lift'_obj 📖	mathematical	CategoryTheory.ReflQuiver.id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj CategoryTheory.Cat.FreeRefl instCategory lift'	—	—
lift_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat.FreeRefl instCategory lift homMk Prefunctor.map CategoryTheory.ReflQuiver.toQuiver CategoryTheory.catToReflQuiver CategoryTheory.ReflPrefunctor.toPrefunctor	—	CategoryTheory.Category.id_comp
lift_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Cat.FreeRefl instCategory lift Prefunctor.obj CategoryTheory.ReflQuiver.toQuiver CategoryTheory.catToReflQuiver CategoryTheory.ReflPrefunctor.toPrefunctor	—	—
lift_spec 📖	mathematical	—	CategoryTheory.ReflPrefunctor.comp CategoryTheory.Cat.FreeRefl CategoryTheory.catToReflQuiver instCategory CategoryTheory.Cat.toFreeRefl CategoryTheory.Functor.toReflPrefunctor lift	—	CategoryTheory.ReflPrefunctor.ext lift_map
lift_unique' 📖	—	CategoryTheory.Functor.comp CategoryTheory.Paths CategoryTheory.Paths.categoryPaths CategoryTheory.ReflQuiver.toQuiver CategoryTheory.Cat.FreeRefl instCategory quotientFunctor	—	—	CategoryTheory.Quotient.lift_unique'
morphismPropertyHomMk_homMk 📖	mathematical	—	morphismPropertyHomMk homMk	—	CategoryTheory.MorphismProperty.ofHoms_iff
morphismProperty_eq_top 📖	mathematical	homMk	Top.top CategoryTheory.MorphismProperty CategoryTheory.Cat.FreeRefl CategoryTheory.Category.toCategoryStruct instCategory BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	le_antisymm multiplicativeClosure_morphismPropertyHomMk CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff
multiplicativeClosure_morphismPropertyHomMk 📖	mathematical	—	CategoryTheory.MorphismProperty.multiplicativeClosure CategoryTheory.Cat.FreeRefl instCategory morphismPropertyHomMk Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	le_antisymm hom_induction CategoryTheory.MorphismProperty.le_multiplicativeClosure morphismPropertyHomMk_homMk CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition CategoryTheory.MorphismProperty.instIsMultiplicativeMultiplicativeClosure
quotientFunctor_map_cons 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Paths CategoryTheory.Paths.categoryPaths CategoryTheory.ReflQuiver.toQuiver CategoryTheory.Cat.FreeRefl instCategory quotientFunctor Quiver.Path.cons CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj homMk	—	—
quotientFunctor_map_id 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Paths CategoryTheory.Paths.categoryPaths CategoryTheory.ReflQuiver.toQuiver CategoryTheory.Cat.FreeRefl instCategory quotientFunctor Quiver.Hom.toPath CategoryTheory.ReflQuiver.id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Quotient.sound
quotientFunctor_map_nil 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Paths CategoryTheory.Paths.categoryPaths CategoryTheory.ReflQuiver.toQuiver CategoryTheory.Cat.FreeRefl instCategory quotientFunctor Quiver.Path.nil CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_id

CategoryTheory.ReflPrefunctor

Definitions

Name	Category	Theorems
toFunctor 📖	CompOp	—

CategoryTheory.ReflQuiv

Definitions

Name	Category	Theorems
adj 📖	CompOp	5 math math: adj_homEquiv, adj_unit_app, adj.unit.map_app_eq, adj_counit_app, adj.counit.comp_app_eq
category 📖	CompOp	28 math math: SSet.oneTruncation₂_obj, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, adj_homEquiv, CategoryTheory.Cat.freeRefl_map, SSet.oneTruncation₂_map, id_map, adj_unit_app, comp_map, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, comp_eq_comp, forget_map, adj.unit.map_app_eq, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, forget_obj, forgetToQuiv_obj, comp_obj, forget_forgetToQuiv, SSet.Truncated.hoFunctor₂_naturality, adj_counit_app, forget.Faithful, forgetToQuiv_map, id_eq_id, id_obj, CategoryTheory.Cat.freeRefl_obj, adj.counit.comp_app_eq, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, forgetToQuiv.Faithful
forget 📖	CompOp	14 math math: SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, adj_homEquiv, adj_unit_app, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, forget_map, adj.unit.map_app_eq, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, forget_obj, forget_forgetToQuiv, adj_counit_app, forget.Faithful, adj.counit.comp_app_eq, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map
forgetToQuiv 📖	CompOp	4 math math: forgetToQuiv_obj, forget_forgetToQuiv, forgetToQuiv_map, forgetToQuiv.Faithful
instCoeSortType 📖	CompOp	—
instInhabited 📖	CompOp	—
instReflQuiverα 📖	CompOp	17 math math: SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, adj_homEquiv, CategoryTheory.Cat.freeRefl_map, id_map, comp_map, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, comp_eq_comp, adj.unit.map_app_eq, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, forgetToQuiv_obj, comp_obj, forgetToQuiv_map, id_eq_id, id_obj, CategoryTheory.Cat.freeRefl_obj, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map
isoOfEquiv 📖	CompOp	—
isoOfQuivIso 📖	CompOp	—
of 📖	CompOp	6 math math: SSet.oneTruncation₂_obj, adj_homEquiv, adj_unit_app, adj.unit.map_app_eq, forget_obj, of_val
toQuiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adj_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.comp CategoryTheory.ReflQuiv category forget CategoryTheory.Cat.freeRefl CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.Cat.FreeRefl CategoryTheory.catToReflQuiver CategoryTheory.Cat.FreeRefl.instCategory CategoryTheory.Cat.FreeRefl.lift CategoryTheory.ReflPrefunctor.id	—	—
adj_homEquiv 📖	mathematical	—	CategoryTheory.Adjunction.homEquiv CategoryTheory.ReflQuiv category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.freeRefl forget adj of CategoryTheory.Cat.of Equiv.trans Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.Hom.equivFunctor adj.homEquiv CategoryTheory.ReflQuiver instReflQuiverα	—	Equiv.ext CategoryTheory.Adjunction.homEquiv_unit
adj_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ReflQuiv category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.freeRefl forget CategoryTheory.Adjunction.unit adj of CategoryTheory.Cat.toFreeRefl	—	—
comp_eq_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.ReflQuiv CategoryTheory.Category.toCategoryStruct category CategoryTheory.ReflPrefunctor.comp CategoryTheory.Bundled.α CategoryTheory.ReflQuiver instReflQuiverα	—	—
comp_map 📖	mathematical	—	Prefunctor.map CategoryTheory.Bundled.α CategoryTheory.ReflQuiver CategoryTheory.ReflQuiver.toQuiver instReflQuiverα CategoryTheory.ReflPrefunctor.toPrefunctor CategoryTheory.CategoryStruct.comp CategoryTheory.ReflQuiv CategoryTheory.Category.toCategoryStruct category Prefunctor.obj	—	—
comp_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.Bundled.α CategoryTheory.ReflQuiver CategoryTheory.ReflQuiver.toQuiver instReflQuiverα CategoryTheory.ReflPrefunctor.toPrefunctor CategoryTheory.CategoryStruct.comp CategoryTheory.ReflQuiv CategoryTheory.Category.toCategoryStruct category	—	—
forgetToQuiv_faithful 📖	—	CategoryTheory.Functor.map CategoryTheory.ReflQuiv category CategoryTheory.Quiv CategoryTheory.Quiv.category forgetToQuiv	—	—	—
forgetToQuiv_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ReflQuiv category CategoryTheory.Quiv CategoryTheory.Quiv.category forgetToQuiv CategoryTheory.ReflPrefunctor.toPrefunctor CategoryTheory.Bundled.α CategoryTheory.ReflQuiver instReflQuiverα	—	—
forgetToQuiv_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ReflQuiv category CategoryTheory.Quiv CategoryTheory.Quiv.category forgetToQuiv CategoryTheory.Quiv.of CategoryTheory.Bundled.α CategoryTheory.ReflQuiver CategoryTheory.ReflQuiver.toQuiver instReflQuiverα	—	—
forget_faithful 📖	—	CategoryTheory.Functor.map CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.ReflQuiv category forget CategoryTheory.Cat.of CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.toCatHom	—	—	CategoryTheory.Functor.map_id
forget_forgetToQuiv 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.ReflQuiv category CategoryTheory.Quiv CategoryTheory.Quiv.category forget forgetToQuiv CategoryTheory.Quiv.forget	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.ReflQuiv category forget CategoryTheory.Functor.toReflPrefunctor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.ReflQuiv category forget of CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.catToReflQuiver CategoryTheory.Cat.str	—	—
id_eq_id 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.ReflQuiv CategoryTheory.Category.toCategoryStruct category CategoryTheory.ReflPrefunctor.id CategoryTheory.Bundled.α CategoryTheory.ReflQuiver instReflQuiverα	—	—
id_map 📖	mathematical	—	Prefunctor.map CategoryTheory.Bundled.α CategoryTheory.ReflQuiver CategoryTheory.ReflQuiver.toQuiver instReflQuiverα CategoryTheory.ReflPrefunctor.toPrefunctor CategoryTheory.CategoryStruct.id CategoryTheory.ReflQuiv CategoryTheory.Category.toCategoryStruct category	—	—
id_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.Bundled.α CategoryTheory.ReflQuiver CategoryTheory.ReflQuiver.toQuiver instReflQuiverα CategoryTheory.ReflPrefunctor.toPrefunctor CategoryTheory.CategoryStruct.id CategoryTheory.ReflQuiv CategoryTheory.Category.toCategoryStruct category	—	—
of_val 📖	mathematical	—	CategoryTheory.Bundled.α CategoryTheory.ReflQuiver of	—	—

CategoryTheory.ReflQuiv.adj

Definitions

Name	Category	Theorems
homEquiv 📖	CompOp	5 math math: CategoryTheory.ReflQuiv.adj_homEquiv, homEquiv_symm_apply, homEquiv_naturality_left_symm, homEquiv_apply, homEquiv_naturality_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor CategoryTheory.Cat.FreeRefl CategoryTheory.Cat.FreeRefl.instCategory CategoryTheory.ReflPrefunctor CategoryTheory.catToReflQuiver EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.ReflPrefunctor.comp CategoryTheory.Cat.toFreeRefl CategoryTheory.Functor.toReflPrefunctor	—	—
homEquiv_naturality_left_symm 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.ReflPrefunctor CategoryTheory.catToReflQuiver CategoryTheory.Functor CategoryTheory.Cat.FreeRefl CategoryTheory.Cat.FreeRefl.instCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.ReflPrefunctor.comp CategoryTheory.Functor.comp CategoryTheory.Cat.freeReflMap	—	CategoryTheory.Cat.FreeRefl.functor_ext CategoryTheory.Cat.FreeRefl.lift_map CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
homEquiv_naturality_right 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor CategoryTheory.Cat.FreeRefl CategoryTheory.Cat.FreeRefl.instCategory CategoryTheory.ReflPrefunctor CategoryTheory.catToReflQuiver EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.Functor.comp CategoryTheory.ReflPrefunctor.comp CategoryTheory.Functor.toReflPrefunctor	—	—
homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.ReflPrefunctor CategoryTheory.catToReflQuiver CategoryTheory.Functor CategoryTheory.Cat.FreeRefl CategoryTheory.Cat.FreeRefl.instCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.Cat.FreeRefl.lift	—	—

CategoryTheory.ReflQuiv.adj.counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_app_eq 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Paths CategoryTheory.Paths.categoryPaths CategoryTheory.ReflQuiver.toQuiver CategoryTheory.catToReflQuiver CategoryTheory.Cat.FreeRefl CategoryTheory.Cat.FreeRefl.instCategory CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.id CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.FreeRefl.quotientFunctor CategoryTheory.Cat.Hom.toFunctor CategoryTheory.ReflQuiv CategoryTheory.ReflQuiv.category CategoryTheory.ReflQuiv.forget CategoryTheory.Cat.freeRefl CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit CategoryTheory.ReflQuiv.adj CategoryTheory.pathComposition	—	CategoryTheory.Paths.ext_functor CategoryTheory.composePath_toPath CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Cat.FreeRefl.lift_map

CategoryTheory.ReflQuiv.adj.unit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_app_eq 📖	mathematical	—	CategoryTheory.ReflPrefunctor.toPrefunctor CategoryTheory.Bundled.α CategoryTheory.ReflQuiver CategoryTheory.Functor.obj CategoryTheory.ReflQuiv CategoryTheory.ReflQuiv.category CategoryTheory.Functor.id CategoryTheory.ReflQuiv.of CategoryTheory.ReflQuiv.instReflQuiverα CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.freeRefl CategoryTheory.ReflQuiv.forget CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit CategoryTheory.ReflQuiv.adj Prefunctor.comp Quiver CategoryTheory.Quiv CategoryTheory.Quiv.category CategoryTheory.Quiv.of CategoryTheory.ReflQuiver.toQuiver CategoryTheory.Quiv.str' CategoryTheory.Cat.free CategoryTheory.Quiv.forget CategoryTheory.Cat.FreeRefl CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.FreeRefl.instCategory CategoryTheory.Quiv.adj CategoryTheory.Functor.toPrefunctor CategoryTheory.Paths CategoryTheory.Paths.categoryPaths CategoryTheory.Cat.FreeRefl.quotientFunctor	—	—

---

← Back to Index