UnderlyingCategory.lean`

86 declarations, 0 contain sorry, 0 declared as axioms

Categorification adjoint to the constructed Street nerve

Categorification uses cocompleteness of strict omega-categories: Ara--Maltsiniotis (2014), Section 5, before Proposition 5.1 (arXiv:1305.5086v3, p. 25). We construct the left adjoint by the pointwise left Kan extension of the actual oriental diagram.

class OAI.Thomason.Construction.StrictColimitsInput line 33
Source documentation
The small-colimit specialization of local presentability of strict omega-categories.
```
class StrictColimitsInput : Prop where
…
```
instance OAI.Thomason.Construction.NormalizedSimplexIdentities.(instance at line 40) line 40
def OAI.Thomason.Construction.NormalizedSimplexIdentities.categorification line 43
Source documentation
Categorification is the colimit of orientals indexed by all simplices.
```
noncomputable def categorification : SSet.{0} ⥤ StrictOmegaCategory.{0} :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.restrictedYonedaIso line 48
Source documentation
Removing the harmless universe lift identifies the restricted Yoneda functor of the Kan-extension theorem with the actual Street nerve.
```
noncomputable def restrictedYonedaIso :
    Presheaf.restrictedULiftYoneda.{0} h.cosimplicial ≅ h.streetNerve :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.categorificationAdjunction line 53
Source documentation
The defining adjunction, derived from the colimit universal property.
```
noncomputable def categorificationAdjunction : h.categorification ⊣ h.streetNerve :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.categorificationSimplexIso line 58
Source documentation
On standard simplices, categorification is naturally the given oriental.
```
noncomputable def categorificationSimplexIso :
    SSet.stdSimplex ⋙ h.categorification ≅ h.cosimplicial :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.categorificationObjIsoColimit line 63
Source documentation
An explicit identification with the simplex colimit, including degeneracies.
```
noncomputable def categorificationObjIsoColimit (K : SSet.{0}) :
    (h.categorification).obj K ≅
      colimit (CostructuredArrow.proj SSet.stdSimplex K ⋙ h.cosimplicial) :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonLeft line 69
Source documentation
The left adjoint in the stated Thomason adjunction.
```
noncomputable def thomasonLeft : SSet.{0} ⥤ StrictOmegaCategory.{0} :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonAdjunction line 74
Source documentation
Twice subdivision followed by categorification is genuinely adjoint to Ex² of the constructed Street nerve. No strict-category model structure is used.
```
noncomputable def thomasonAdjunction : h.thomasonLeft ⊣ h.thomasonRight :=
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.categorification_preservesColimits line 79
Source documentation
The colimit formula also provides every colimit-preservation fact needed when assembling a simplexwise relative prism.
```
theorem categorification_preservesColimits :
    PreservesColimitsOfSize.{0, 0} (h.categorification) :=
…
```
theorem OAI.Thomason.Construction.strictOmegaHasSmallColimits line 103
Source documentation
Every small diagram of small strict omega-categories has the constructed colimit.
```
theorem strictOmegaHasSmallColimits : HasColimitsOfSize.{0,0} StrictOmegaCategory.{0} where
…
```
instance OAI.Thomason.Construction.constructedStrictColimitsInput line 110
Source documentation
Strict omega-categories admit small colimits.
```
instance constructedStrictColimitsInput : StrictColimitsInput where
…
```
Mentions: OAI.Thomason.Construction.StrictColimitsInput
def OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexLeg line 133
Source documentation
The canonical oriental attached to a simplex of a simplicial set.
```
noncomputable def simplexLeg {K : SSet.{0}} {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ K) : h.object m.len ⟶ h.categorification.obj K :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexCocone line 138
Source documentation
The oriental presentation, including degenerate simplices.
```
noncomputable def simplexCocone (K : SSet.{0}) :
    Cocone (CostructuredArrow.proj SSet.stdSimplex K ⋙ h.cosimplicial) :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexCocone_isColimit line 146
Source documentation
This is the actual colimit presentation of categorification.
```
noncomputable def simplexCocone_isColimit (K : SSet.{0}) : IsColimit (h.simplexCocone K) := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexCocone_leg line 158

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexLeg_precomp line 162

Source documentation

Source naturality of a presentation leg.

theorem simplexLeg_precomp {K : SSet.{0}} {m n : SimplexCategory}
    (s : SSet.stdSimplex.obj n ⟶ K) (a : m ⟶ n) :
    h.cosimplicial.map a ≫ h.simplexLeg s =
      h.simplexLeg (SSet.stdSimplex.map a ≫ s) := by
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexLeg_postcomp line 180

Source documentation

Target naturality of a presentation leg.

theorem simplexLeg_postcomp {K L : SSet.{0}} {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ K) (f : K ⟶ L) :
    h.simplexLeg s ≫ h.categorification.map f = h.simplexLeg (s ≫ f) := by
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder line 191
Source documentation
A poset simplex as its monotone list of vertices.
```
def simplexOrder {E : Type} [PartialOrder E] {m : SimplexCategory}
    (s : (nerve E).obj (op m)) : Fin (m.len + 1) →o E where
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.orderSimplex line 197
Source documentation
The corresponding simplex of the ordinary nerve.
```
def orderSimplex {E : Type} [PartialOrder E] {m : ℕ}
    (s : Fin (m + 1) →o E) : (nerve E).obj (op (.mk m)) :=
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder_orderSimplex line 203
def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetLeg line 207
Source documentation
The oriental map specified by a monotone list of vertices in a poset.
```
noncomputable def posetLeg {E : Type} [PartialOrder E] {m : ℕ}
    (s : Fin (m + 1) →o E) : h.object m ⟶ h.categorification.obj (nerve E) :=
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetLeg_precomp line 212

Source documentation

All ordinal operators, including degeneracies, act on these canonical legs.

theorem posetLeg_precomp {E : Type} [PartialOrder E] {l m : ℕ}
    (s : Fin (m + 1) →o E) (a : Fin (l + 1) →o Fin (m + 1)) :
    h.map a ≫ h.posetLeg s = h.posetLeg (s.comp a) := by
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.orderSimplex_simplexOrder line 226
Source documentation
Recover a nerve simplex from its monotone vertex map.
```
theorem orderSimplex_simplexOrder {E : Type} [PartialOrder E] {m : SimplexCategory}
    (s : (nerve E).obj (op m)) : orderSimplex (simplexOrder s) = s :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities.orderSimplex, OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetLeg_simplexOrder line 231
Source documentation
Replacing a simplex by its vertex map does not change its presentation leg.
```
theorem posetLeg_simplexOrder {E : Type} [PartialOrder E] {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ nerve E) :
    h.posetLeg (simplexOrder (SSet.yonedaEquiv s)) = h.simplexLeg s := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder_precomp line 239

Source documentation

The vertex map of a simplex operator is ordinary precomposition.

theorem simplexOrder_precomp {E : Type} [PartialOrder E] {m n : SimplexCategory}
    (s : SSet.stdSimplex.obj n ⟶ nerve E) (a : m ⟶ n) :
    simplexOrder (SSet.yonedaEquiv (SSet.stdSimplex.map a ≫ s)) =
      (simplexOrder (SSet.yonedaEquiv s)).comp a.toOrderHom := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetLeg_postcomp line 249

Source documentation

Postcomposition by a monotone poset map is natural on canonical legs.

theorem posetLeg_postcomp {E F : Type} [PartialOrder E] [PartialOrder F] {m : ℕ}
    (s : Fin (m + 1) →o E) (b : E →o F) :
    h.posetLeg s ≫ h.categorification.map (nerveMap b.monotone.functor) =
      h.posetLeg (b.comp s) := by
…

def OAI.Thomason.Construction.subposetInclusion line 270
Source documentation
The monotone inclusion of a full subposet.
```
def subposetInclusion {E : Type} [PartialOrder E] (A : Set E) : A →o E where
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetMap line 278
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetMap_id line 282
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetMap_comp line 292
structure OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.Cell line 325
Source documentation
Compatible diagram cells sharing a finite dimension bound.
```
structure Cell where
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.Cell.ext line 334
def OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.Cell.face line 340
def OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.Cell.comp line 346
Source documentation
Matching families can be composed componentwise.
```
def comp (n : ℕ) (x y : Cell F) (he : face true n x = face false n y) : Cell F where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.Cell, OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.Cell.face
def OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.category line 369
Source documentation
The compatible bounded families satisfy all strict laws componentwise.
```
def category : StrictOmegaCategory.{0} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.projection line 427
Source documentation
Projection to an original diagram component.
```
def projection (j : J) : category F ⟶ F.obj j where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.category
def OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.cone line 433
Source documentation
The bounded compatible families form a cone on the original diagram.
```
def cone : Cone F where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.lift line 445
Source documentation
An original cone gives bounded families because each input cell has one dimension bound preserved by all the projection functors.
```
def lift (s : Cone F) : s.pt ⟶ category F where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.lift_fac line 456
Source documentation
Its projections are exactly those of the given cone.
```
theorem lift_fac (s : Cone F) (j : J) : lift F s ≫ projection F j = s.π.app j := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.lift, OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.projection
theorem OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.hom_ext line 461
Source documentation
Every map is determined by its diagram projections.
```
theorem hom_ext {D : StrictOmegaCategory.{0}} (f g : D ⟶ category F)
    (he : ∀ j, f ≫ projection F j = g ≫ projection F j) : f = g := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.category, OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.projection
def OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.isLimit line 470
Source documentation
This is the actual strict limit universal property.
```
def isLimit : IsLimit (cone F) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.LimitConstruction.cone
instance OAI.Thomason.Construction.strictOmegaHasFiniteLimits line 482
Source documentation
Strict omega-categories admit finite limits.
```
instance strictOmegaHasFiniteLimits : HasFiniteLimits StrictOmegaCategory.{0} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.opposite line 506
Source documentation
Reverse both boundaries and the order of every strict composition.
```
def opposite (C : StrictOmegaCategory.{0}) : StrictOmegaCategory.{0} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.oppositeMap line 524
Source documentation
Reversing all directions retains the underlying strict functor.
```
def oppositeMap {C D : StrictOmegaCategory.{0}} (f : C ⟶ D) : opposite C ⟶ opposite D where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.opposite
def OAI.Thomason.Construction.StrictOmegaCategory.oppositeFunctor line 530
Source documentation
Opposite is functorial without a change of universe.
```
def oppositeFunctor : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.doubleOppositeIso line 537
Source documentation
The double opposite has exactly the original strict cells.
```
def doubleOppositeIso (C : StrictOmegaCategory.{0}) : opposite (opposite C) ≅ C where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.opposite
def OAI.Thomason.Construction.StrictOmegaCategory.oppositeEquivalence line 550
Source documentation
Reversal is a genuine equivalence, allowing colimits to be transported.
```
def oppositeEquivalence : StrictOmegaCategory.{0} ≌ StrictOmegaCategory.{0} where
…
```
structure OAI.Thomason.Construction.StrictPoset.Cell line 585
theorem OAI.Thomason.Construction.StrictPoset.Cell.ext line 591
def OAI.Thomason.Construction.StrictPoset.identity line 601
def OAI.Thomason.Construction.StrictPoset.face line 603
theorem OAI.Thomason.Construction.StrictPoset.last_eq_first line 607
def OAI.Thomason.Construction.StrictPoset.comp line 610
def OAI.Thomason.Construction.StrictPoset.category line 616
Source documentation
The strict omega-category associated to a poset, truncated in dimension one.
```
def category (E : Type u) [Preorder E] : StrictOmegaCategory.{u} where
…
```
theorem OAI.Thomason.Construction.StrictPoset.category_isTruncated line 649
def OAI.Thomason.Construction.StrictPoset.map line 653
Source documentation
A monotone map induces the unique functor on the associated thin categories.
```
def map {F : Type v} [Preorder F] (f : E →o F) : (category E).Hom (category F) where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.StrictPoset.map_identity line 659
theorem OAI.Thomason.Construction.StrictPoset.map_id line 662
theorem OAI.Thomason.Construction.StrictPoset.map_comp line 667
def OAI.Thomason.Construction.StrictOmegaCategory.labelFiber line 696
Source documentation
The full subcategory on objects labelled by a fixed value.
```
def labelFiber (p : Hom C (StrictPoset.category E)) (e : E) : StrictOmegaCategory.{0} :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.fullCell_label_iff line 700
Source documentation
The full object fiber is precisely the fiber on all strict cells.
```
theorem fullCell_label_iff (p : Hom C (StrictPoset.category E)) (e : E) (x : C) :
    C.FullCell {z | p z = StrictPoset.identity e} x ↔ p x = StrictPoset.identity e := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity
def OAI.Thomason.Construction.StrictOmegaCategory.labelFiberInclusion line 721
Source documentation
The inclusion of a label fiber in its ambient strict category.
```
def labelFiberInclusion (p : Hom C (StrictPoset.category E)) (e : E) : labelFiber p e ⟶ C :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber
instance OAI.Thomason.Construction.StrictOmegaCategory.labelFiberInclusion_mono line 724
def OAI.Thomason.Construction.StrictOmegaCategory.labelFiberMap line 729
Source documentation
Every functor over the ordered label restricts to every fiber.
```
def labelFiberMap (p : Hom C (StrictPoset.category E)) (q : Hom D (StrictPoset.category E))
    (e : E) (f : Hom C D) (hf : Hom.comp f q = p) : labelFiber p e ⟶ labelFiber q e :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.Hom.comp, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber
def OAI.Thomason.Construction.StrictOmegaCategory.labelFiberFunctor line 735
Source documentation
Fiber formation is functorial on the actual slice category.
```
def labelFiberFunctor (E : Type) [Preorder E] (e : E) :
    Over (StrictPoset.category E) ⥤ StrictOmegaCategory.{0} where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.labelFiber_isTruncated line 749
Source documentation
Fibers have no higher cells than the ambient category.
```
theorem labelFiber_isTruncated (p : Hom C (StrictPoset.category E)) (e : E)
    {n : ℕ} (hC : C.IsTruncated n) : (labelFiber p e).IsTruncated n :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber, OAI.Thomason.Construction.StrictOmegaCategory.IsTruncated
def OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetSubcomplex line 773
Source documentation
A simplex is in the full subcomplex when all its cells are in the full subcategory.
```
def fullStreetSubcomplex (S : Set C) : (h.streetNerve.obj C).Subcomplex where
…
```

def OAI.Thomason.Construction.NormalizedSimplexIdentities.liftFullSimplex line 778

Source documentation

Lift a simplex all of whose cells belong to a full subcategory.

def liftFullSimplex (S : Set C) {m : SimplexCategory}
    (f : h.object m.len ⟶ C) (hf : ∀ x, C.FullCell S (f.toFun x)) :
    h.object m.len ⟶ C.fullOn S where
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetSubcomplex_eq_range line 786
Source documentation
The full subcomplex is exactly the image of the original full inclusion.
```
theorem fullStreetSubcomplex_eq_range (S : Set C) :
    h.fullStreetSubcomplex C S =
      SSet.Subcomplex.range (h.streetNerve.map (C.fullInclusion S)) := by
…
```
instance OAI.Thomason.Construction.NormalizedSimplexIdentities.streetNerve_fullInclusion_mono line 797
Source documentation
Full inclusions are injective on every Street simplex.
```
instance streetNerve_fullInclusion_mono (S : Set C) :
    Mono (h.streetNerve.map (C.fullInclusion S)) := by
…
```
instance OAI.Thomason.Construction.NormalizedSimplexIdentities.streetNerve_labelFiberInclusion_mono line 808
def OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetIso line 814
Source documentation
The nerve of a full subcategory is isomorphic to this actual subcomplex.
```
noncomputable def fullStreetIso (S : Set C) :
    h.streetNerve.obj (C.fullOn S) ≅ (h.fullStreetSubcomplex C S).toSSet :=
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetIso_hom_ι line 820
Source documentation
This isomorphism commutes with the original inclusion, without changing its image.
```
theorem fullStreetIso_hom_ι (S : Set C) :
    (h.fullStreetIso C S).hom ≫ (h.fullStreetSubcomplex C S).ι =
      h.streetNerve.map (C.fullInclusion S) := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetSubcomplex_inter line 826
Source documentation
Intersections of full subcategories are computed on the actual Street subcomplexes.
```
theorem fullStreetSubcomplex_inter (S T : Set C) :
    h.fullStreetSubcomplex C (S ∩ T) =
      h.fullStreetSubcomplex C S ⊓ h.fullStreetSubcomplex C T := by
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetSubcomplex_isPushout line 838

Source documentation

A cover by full Street subcomplexes gives its genuine simplicial pushout.

theorem fullStreetSubcomplex_isPushout (S T : Set C)
    (hc : h.fullStreetSubcomplex C S ⊔ h.fullStreetSubcomplex C T = ⊤) :
    IsPushout
      (SSet.Subcomplex.homOfLE (show h.fullStreetSubcomplex C (S ∩ T) ≤
        h.fullStreetSubcomplex C S from fun _ _ hf x => ⟨(hf x).1.1, (hf x).2.1⟩))
      (SSet.Subcomplex.homOfLE (show h.fullStreetSubcomplex C (S ∩ T) ≤
        h.fullStreetSubcomplex C T from fun _ _ hf x => ⟨(hf x).1.2, (hf x).2.2⟩))
      (h.fullStreetSubcomplex C S).ι (h.fullStreetSubcomplex C T).ι := by
…

def OAI.Thomason.Construction.StrictOmegaCategory.Objects line 873
def OAI.Thomason.Construction.StrictOmegaCategory.OneArrow line 875
def OAI.Thomason.Construction.StrictOmegaCategory.OneArrow.id line 880
def OAI.Thomason.Construction.StrictOmegaCategory.OneArrow.comp line 884
theorem OAI.Thomason.Construction.StrictOmegaCategory.OneArrow.id_comp line 892
theorem OAI.Thomason.Construction.StrictOmegaCategory.OneArrow.comp_id line 900
theorem OAI.Thomason.Construction.StrictOmegaCategory.OneArrow.assoc line 908
instance OAI.Thomason.Construction.StrictOmegaCategory.(instance at line 916) line 916
def OAI.Thomason.Construction.StrictOmegaCategory.Hom.toOneFunctor line 925
Source documentation
The object and 1-cell action of a strict functor is an ordinary functor.
```
def Hom.toOneFunctor {C D : StrictOmegaCategory} (f : Hom C D) : Objects C ⥤ Objects D where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory, OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.StrictOmegaCategory.Objects
def OAI.Thomason.Construction.StrictOmegaCategory.underlyingCategory line 937
Source documentation
Recovering objects and 1-cells is functorial in strict omega-categories.
```
def underlyingCategory : StrictOmegaCategory.{u} ⥤ Cat.{u, u} where
…
```