Skeletal

📁 Source: Mathlib/CategoryTheory/Skeletal.lean

Statistics

Metric	Count
Definitions `skeletonEquiv`, `thinSkeletonOrderIso`, `mapSkeleton`, `toSkeletonFunctorCompMapSkeletonIso`, `IsSkeletonOf`, `Skeletal`, `isoOfEq`, `ThinSkeleton`, `equivalence`, `fromThinSkeleton`, `fromThinSkeletonCompToThinSkeletonIso`, `isSkeletonOfInhabited`, `lowerAdjunction`, `map`, `mapCompFromThinSkeletonIso`, `mapNatTrans`, `map₂`, `map₂Functor`, `map₂NatTrans`, `map₂ObjMap`, `mk`, `preorder`, `thinSkeletonPartialOrder`, `fromSkeleton`, `fromSkeletonToSkeletonIso`, `inhabitedThinSkeleton`, `instCategorySkeleton`, `instCoeSortSkeleton`, `instInhabitedSkeleton`, `preCounitIso`, `skeletonEquivalence`, `toSkeleton`, `toSkeletonFunctor`, `toThinSkeleton`	34
Theorems `eq_of_iso`, `instEssSurjSkeletonMapSkeleton`, `instFaithfulSkeletonMapSkeleton`, `instFullSkeletonMapSkeleton`, `mapSkeleton_injective`, `mapSkeleton_obj_toSkeleton`, `mapSkeleton_surjective`, `eqv`, `skel`, `comp_hom`, `comp_hom_assoc`, `comp_toThinSkeleton`, `equiv_of_both_ways`, `fromThinSkeleton_isEquivalence`, `fromThinSkeleton_map`, `fromThinSkeleton_obj`, `map_comp_eq`, `map_id_eq`, `map_iso_eq`, `map_map`, `map_obj`, `map₂_map`, `map₂_obj`, `skeletal`, `thin`, `thinSkeleton_isSkeleton`, `toThinSkeleton_faithful`, `congr_toSkeleton_of_iso`, `isEquivalence`, `fromSkeleton_map`, `fromSkeleton_obj`, `functor_skeletal`, `instEssSurjSkeletonFromSkeleton`, `instFaithfulSkeletonFromSkeleton`, `instFullSkeletonFromSkeleton`, `skeletonEquivalence_counitIso`, `skeletonEquivalence_functor`, `skeletonEquivalence_inverse`, `skeletonEquivalence_unitIso`, `skeleton_isSkeleton`, `skeleton_skeletal`, `toSkeletonFunctor_map_hom`, `toSkeletonFunctor_obj`, `toSkeleton_eq_iff`, `toSkeleton_eq_toSkeleton_iff`, `toSkeleton_fromSkeleton_obj`, `toThinSkeleton_map`, `toThinSkeleton_obj`	48
Total	82

CategoryTheory

Definitions

Name	Category	Theorems
`IsSkeletonOf` 📖	CompData	4 math math: `SimplexCategory.isSkeletonOf`, `FintypeCat.isSkeleton`, `ThinSkeleton.thinSkeleton_isSkeleton`, `skeleton_isSkeleton`
`Skeletal` 📖	MathDef	6 math math: `SimplexCategory.skeletal`, `IsSkeletonOf.skel`, `skeleton_skeletal`, `FintypeCat.Skeleton.is_skeletal`, `ThinSkeleton.skeletal`, `Subobject.skeletal`
`ThinSkeleton` 📖	CompOp	21 math math: `Limits.hasLimitsOfSize_thinSkeleton`, `Limits.hasColimitsOfShape_thinSkeleton`, `ThinSkeleton.map_map`, `ThinSkeleton.fromThinSkeleton_isEquivalence`, `ThinSkeleton.map_obj`, `ThinSkeleton.fromThinSkeleton_map`, `Limits.hasColimitsOfSize_thinSkeleton`, `ThinSkeleton.fromThinSkeleton_obj`, `ThinSkeleton.thin`, `ThinSkeleton.map₂_obj`, `Limits.hasLimitsOfShape_thinSkeleton`, `toThinSkeleton_map`, `Subobject.lower_comm`, `ThinSkeleton.thinSkeleton_isSkeleton`, `ThinSkeleton.map_id_eq`, `ThinSkeleton.map₂_map`, `ThinSkeleton.skeletal`, `toThinSkeleton_obj`, `ThinSkeleton.map_comp_eq`, `ThinSkeleton.comp_toThinSkeleton`, `ThinSkeleton.toThinSkeleton_faithful`
`fromSkeleton` 📖	CompOp	13 math math: `fromSkeleton.isEquivalence`, `skeletonEquivalence_unitIso`, `toSkeleton_eq_iff`, `toSkeleton_fromSkeleton_obj`, `instEssSurjSkeletonFromSkeleton`, `skeletonEquivalence_counitIso`, `fromSkeleton_obj`, `fromSkeleton_map`, `instFaithfulSkeletonFromSkeleton`, `instFullSkeletonFromSkeleton`, `toSkeletonFunctor_map_hom`, `skeleton_isSkeleton`, `skeletonEquivalence_functor`
`fromSkeletonToSkeletonIso` 📖	CompOp	2 math math: `skeletonEquivalence_counitIso`, `toSkeletonFunctor_map_hom`
`inhabitedThinSkeleton` 📖	CompOp	—
`instCategorySkeleton` 📖	CompOp	28 math math: `Limits.hasColimitsOfShape_skeleton`, `Limits.hasLimitsOfSize_skeleton`, `fromSkeleton.isEquivalence`, `skeletonEquivalence_unitIso`, `skeletonEquivalence_inverse`, `toSkeleton_eq_iff`, `Functor.mapSkeleton_obj_toSkeleton`, `Functor.instFaithfulSkeletonMapSkeleton`, `toSkeleton_fromSkeleton_obj`, `instEssSurjSkeletonFromSkeleton`, `skeleton_skeletal`, `skeletonEquivalence_counitIso`, `fromSkeleton_obj`, `Limits.hasLimitsOfShape_skeleton`, `fromSkeleton_map`, `instFaithfulSkeletonFromSkeleton`, `instFullSkeletonFromSkeleton`, `Functor.instFullSkeletonMapSkeleton`, `Skeleton.comp_hom`, `toSkeletonFunctor_map_hom`, `Functor.instEssSurjSkeletonMapSkeleton`, `toSkeletonFunctor_obj`, `skeleton_isSkeleton`, `skeletonEquivalence_functor`, `Functor.mapSkeleton_injective`, `Limits.hasColimitsOfSize_skeleton`, `Functor.mapSkeleton_surjective`, `Skeleton.comp_hom_assoc`
`instCoeSortSkeleton` 📖	CompOp	—
`instInhabitedSkeleton` 📖	CompOp	—
`preCounitIso` 📖	CompOp	—
`skeletonEquivalence` 📖	CompOp	4 math math: `skeletonEquivalence_unitIso`, `skeletonEquivalence_inverse`, `skeletonEquivalence_counitIso`, `skeletonEquivalence_functor`
`toSkeleton` 📖	CompOp	10 math math: `congr_toSkeleton_of_iso`, `Skeleton.toSkeleton_tensorObj`, `toSkeleton_eq_iff`, `Skeleton.one_eq`, `Functor.mapSkeleton_obj_toSkeleton`, `toSkeleton_fromSkeleton_obj`, `toSkeletonFunctor_map_hom`, `toSkeletonFunctor_obj`, `Skeleton.mul_eq`, `toSkeleton_eq_toSkeleton_iff`
`toSkeletonFunctor` 📖	CompOp	5 math math: `skeletonEquivalence_unitIso`, `skeletonEquivalence_inverse`, `skeletonEquivalence_counitIso`, `toSkeletonFunctor_map_hom`, `toSkeletonFunctor_obj`
`toThinSkeleton` 📖	CompOp	5 math math: `toThinSkeleton_map`, `Subobject.lower_comm`, `toThinSkeleton_obj`, `ThinSkeleton.comp_toThinSkeleton`, `ThinSkeleton.toThinSkeleton_faithful`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_toSkeleton_of_iso` 📖	mathematical	—	`toSkeleton`	—	—
`fromSkeleton_map` 📖	mathematical	—	`Functor.map` `Skeleton` `instCategorySkeleton` `fromSkeleton` `InducedCategory.Hom.hom` `isIsomorphicSetoid` `Quotient.out`	—	—
`fromSkeleton_obj` 📖	mathematical	—	`Functor.obj` `Skeleton` `instCategorySkeleton` `fromSkeleton` `Quotient.out` `isIsomorphicSetoid`	—	—
`functor_skeletal` 📖	mathematical	`Quiver.IsThin` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Skeletal`	`Functor` `Functor.category`	—	`Functor.eq_of_iso`
`instEssSurjSkeletonFromSkeleton` 📖	mathematical	—	`Functor.EssSurj` `Skeleton` `instCategorySkeleton` `fromSkeleton`	—	`Quotient.mk_out`
`instFaithfulSkeletonFromSkeleton` 📖	mathematical	—	`Functor.Faithful` `Skeleton` `instCategorySkeleton` `fromSkeleton`	—	`InducedCategory.faithful`
`instFullSkeletonFromSkeleton` 📖	mathematical	—	`Functor.Full` `Skeleton` `instCategorySkeleton` `fromSkeleton`	—	`InducedCategory.full`
`skeletonEquivalence_counitIso` 📖	mathematical	—	`Equivalence.counitIso` `Skeleton` `instCategorySkeleton` `skeletonEquivalence` `NatIso.ofComponents` `Functor.comp` `toSkeletonFunctor` `fromSkeleton` `Functor.id` `fromSkeletonToSkeletonIso`	—	—
`skeletonEquivalence_functor` 📖	mathematical	—	`Equivalence.functor` `Skeleton` `instCategorySkeleton` `skeletonEquivalence` `fromSkeleton`	—	—
`skeletonEquivalence_inverse` 📖	mathematical	—	`Equivalence.inverse` `Skeleton` `instCategorySkeleton` `skeletonEquivalence` `toSkeletonFunctor`	—	—
`skeletonEquivalence_unitIso` 📖	mathematical	—	`Equivalence.unitIso` `Skeleton` `instCategorySkeleton` `skeletonEquivalence` `NatIso.ofComponents` `Functor.id` `Functor.comp` `fromSkeleton` `toSkeletonFunctor` `InducedCategory.isoMk` `isIsomorphicSetoid` `Quotient.out` `Functor.obj` `Iso.symm` `Nonempty.some` `Iso`	—	—
`skeleton_isSkeleton` 📖	mathematical	—	`IsSkeletonOf` `Skeleton` `instCategorySkeleton` `fromSkeleton`	—	`skeleton_skeletal` `fromSkeleton.isEquivalence`
`skeleton_skeletal` 📖	mathematical	—	`Skeletal` `Skeleton` `instCategorySkeleton`	—	`Quotient.out_eq`
`toSkeletonFunctor_map_hom` 📖	mathematical	—	`InducedCategory.Hom.hom` `isIsomorphicSetoid` `Quotient.out` `toSkeleton` `Functor.map` `Skeleton` `instCategorySkeleton` `toSkeletonFunctor` `CategoryStruct.comp` `Category.toCategoryStruct` `Iso.hom` `Functor.obj` `fromSkeleton` `fromSkeletonToSkeletonIso` `Iso.inv`	—	—
`toSkeletonFunctor_obj` 📖	mathematical	—	`Functor.obj` `Skeleton` `instCategorySkeleton` `toSkeletonFunctor` `toSkeleton`	—	—
`toSkeleton_eq_iff` 📖	mathematical	—	`toSkeleton` `Iso` `Functor.obj` `Skeleton` `instCategorySkeleton` `fromSkeleton`	—	`Quotient.mk_eq_iff_out`
`toSkeleton_eq_toSkeleton_iff` 📖	mathematical	—	`toSkeleton` `Iso`	—	`Quotient.eq`
`toSkeleton_fromSkeleton_obj` 📖	mathematical	—	`toSkeleton` `Functor.obj` `Skeleton` `instCategorySkeleton` `fromSkeleton`	—	`Quotient.out_eq`
`toThinSkeleton_map` 📖	mathematical	—	`Functor.map` `ThinSkeleton` `Preorder.smallCategory` `ThinSkeleton.preorder` `toThinSkeleton` `homOfLE`	—	—
`toThinSkeleton_obj` 📖	mathematical	—	`Functor.obj` `ThinSkeleton` `Preorder.smallCategory` `ThinSkeleton.preorder` `toThinSkeleton`	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
`skeletonEquiv` 📖	CompOp	—
`thinSkeletonOrderIso` 📖	CompOp	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`mapSkeleton` 📖	CompOp	6 math math: `mapSkeleton_obj_toSkeleton`, `instFaithfulSkeletonMapSkeleton`, `instFullSkeletonMapSkeleton`, `instEssSurjSkeletonMapSkeleton`, `mapSkeleton_injective`, `mapSkeleton_surjective`
`toSkeletonFunctorCompMapSkeletonIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_iso` 📖	—	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Skeletal`	—	—	`ext`
`instEssSurjSkeletonMapSkeleton` 📖	mathematical	—	`EssSurj` `CategoryTheory.Skeleton` `CategoryTheory.instCategorySkeleton` `mapSkeleton`	—	`essSurj_comp` `CategoryTheory.Equivalence.essSurj_functor` `CategoryTheory.Equivalence.essSurj_inverse`
`instFaithfulSkeletonMapSkeleton` 📖	mathematical	—	`Faithful` `CategoryTheory.Skeleton` `CategoryTheory.instCategorySkeleton` `mapSkeleton`	—	`Faithful.comp` `CategoryTheory.Equivalence.faithful_functor` `CategoryTheory.Equivalence.faithful_inverse`
`instFullSkeletonMapSkeleton` 📖	mathematical	—	`Full` `CategoryTheory.Skeleton` `CategoryTheory.instCategorySkeleton` `mapSkeleton`	—	`Full.comp` `CategoryTheory.Equivalence.full_functor` `CategoryTheory.Equivalence.full_inverse`
`mapSkeleton_injective` 📖	mathematical	—	`CategoryTheory.Skeleton` `obj` `CategoryTheory.instCategorySkeleton` `mapSkeleton`	—	`CategoryTheory.skeleton_skeletal` `instFullSkeletonMapSkeleton` `instFaithfulSkeletonMapSkeleton`
`mapSkeleton_obj_toSkeleton` 📖	mathematical	—	`obj` `CategoryTheory.Skeleton` `CategoryTheory.instCategorySkeleton` `mapSkeleton` `CategoryTheory.toSkeleton`	—	`CategoryTheory.congr_toSkeleton_of_iso`
`mapSkeleton_surjective` 📖	mathematical	—	`CategoryTheory.Skeleton` `obj` `CategoryTheory.instCategorySkeleton` `mapSkeleton`	—	`EssSurj.mem_essImage` `instEssSurjSkeletonMapSkeleton` `CategoryTheory.skeleton_skeletal`

CategoryTheory.IsSkeletonOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eqv` 📖	mathematical	`CategoryTheory.IsSkeletonOf`	`CategoryTheory.Functor.IsEquivalence`	—	—
`skel` 📖	mathematical	`CategoryTheory.IsSkeletonOf`	`CategoryTheory.Skeletal`	—	—

CategoryTheory.Skeleton

Definitions

Name	Category	Theorems
`isoOfEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.isIsomorphicSetoid` `Quotient.out` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Skeleton` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategorySkeleton`	—	—
`comp_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quotient.out` `CategoryTheory.isIsomorphicSetoid` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.Skeleton` `CategoryTheory.instCategorySkeleton`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_hom`

CategoryTheory.ThinSkeleton

Definitions

Name	Category	Theorems
`equivalence` 📖	CompOp	—
`fromThinSkeleton` 📖	CompOp	4 math math: `fromThinSkeleton_isEquivalence`, `fromThinSkeleton_map`, `fromThinSkeleton_obj`, `thinSkeleton_isSkeleton`
`fromThinSkeletonCompToThinSkeletonIso` 📖	CompOp	—
`isSkeletonOfInhabited` 📖	CompOp	—
`lowerAdjunction` 📖	CompOp	—
`map` 📖	CompOp	6 math math: `map_map`, `map_obj`, `map_iso_eq`, `map_id_eq`, `map_comp_eq`, `comp_toThinSkeleton`
`mapCompFromThinSkeletonIso` 📖	CompOp	—
`mapNatTrans` 📖	CompOp	—
`map₂` 📖	CompOp	2 math math: `map₂_obj`, `map₂_map`
`map₂Functor` 📖	CompOp	1 math math: `map₂_obj`
`map₂NatTrans` 📖	CompOp	1 math math: `map₂_map`
`map₂ObjMap` 📖	CompOp	—
`mk` 📖	CompOp	—
`preorder` 📖	CompOp	21 math math: `CategoryTheory.Limits.hasLimitsOfSize_thinSkeleton`, `CategoryTheory.Limits.hasColimitsOfShape_thinSkeleton`, `map_map`, `fromThinSkeleton_isEquivalence`, `map_obj`, `fromThinSkeleton_map`, `CategoryTheory.Limits.hasColimitsOfSize_thinSkeleton`, `fromThinSkeleton_obj`, `thin`, `map₂_obj`, `CategoryTheory.Limits.hasLimitsOfShape_thinSkeleton`, `CategoryTheory.toThinSkeleton_map`, `CategoryTheory.Subobject.lower_comm`, `thinSkeleton_isSkeleton`, `map_id_eq`, `map₂_map`, `skeletal`, `CategoryTheory.toThinSkeleton_obj`, `map_comp_eq`, `comp_toThinSkeleton`, `toThinSkeleton_faithful`
`thinSkeletonPartialOrder` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_toThinSkeleton` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `CategoryTheory.toThinSkeleton` `map`	—	—
`equiv_of_both_ways` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.isIsomorphicSetoid`	—	—
`fromThinSkeleton_isEquivalence` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `fromThinSkeleton`	—	`CategoryTheory.Equivalence.isEquivalence_functor`
`fromThinSkeleton_map` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.map` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `fromThinSkeleton` `CategoryTheory.isIsomorphicSetoid` `CategoryTheory.CategoryStruct.comp` `Quotient.out` `CategoryTheory.Iso.hom` `Nonempty.some` `CategoryTheory.Iso` `Quiver.Hom` `CategoryTheory.Iso.inv`	—	—
`fromThinSkeleton_obj` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.obj` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `fromThinSkeleton` `Quotient.out` `CategoryTheory.isIsomorphicSetoid`	—	—
`map_comp_eq` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`map` `CategoryTheory.Functor.comp` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder`	—	`CategoryTheory.Functor.eq_of_iso` `thin` `skeletal` `CategoryTheory.subsingleton_iso`
`map_id_eq` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`map` `CategoryTheory.Functor.id` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder`	—	`CategoryTheory.Functor.eq_of_iso` `thin` `skeletal` `CategoryTheory.subsingleton_iso`
`map_iso_eq` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`map`	—	`CategoryTheory.Functor.eq_of_iso` `thin` `skeletal`
`map_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `map` `CategoryTheory.isIsomorphicSetoid` `CategoryTheory.homOfLE` `Quotient.map` `CategoryTheory.Functor.obj`	—	—
`map_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `map` `Quotient.map` `CategoryTheory.isIsomorphicSetoid`	—	—
`map₂_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `map₂` `map₂NatTrans`	—	—
`map₂_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `map₂` `map₂Functor`	—	—
`skeletal` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Skeletal` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder`	—	`LE.le.antisymm`
`thin` 📖	mathematical	—	`Quiver.IsThin` `CategoryTheory.ThinSkeleton` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `preorder`	—	—
`thinSkeleton_isSkeleton` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.IsSkeletonOf` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `fromThinSkeleton`	—	`skeletal` `fromThinSkeleton_isEquivalence`
`toThinSkeleton_faithful` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.Faithful` `CategoryTheory.ThinSkeleton` `Preorder.smallCategory` `preorder` `CategoryTheory.toThinSkeleton`	—	—

CategoryTheory.fromSkeleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEquivalence` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.Skeleton` `CategoryTheory.instCategorySkeleton` `CategoryTheory.fromSkeleton`	—	`CategoryTheory.instFaithfulSkeletonFromSkeleton` `CategoryTheory.instFullSkeletonFromSkeleton` `CategoryTheory.instEssSurjSkeletonFromSkeleton`

---

← Back to Index