Notation

This file defines notation and abbreviations used throughout the library.

def HigherCategoryTheory.termω : Lean.ParserDescr

Notation for the top element of an order with top (Top.top). In our context, it represents the index of an $\omega$-category in ℕ∞.

Equations

• HigherCategoryTheory.termω = Lean.ParserDescr.node `HigherCategoryTheory.termω 1024 (Lean.ParserDescr.symbol "ω")

def HigherCategoryTheory.termFin : Lean.ParserDescr

Notation for the injection into a WithTop type (WithTop.some). In our context, it represents the index of an $n$-category in ℕ∞.

Equations

• HigherCategoryTheory.termFin = Lean.ParserDescr.node `HigherCategoryTheory.termFin 1024 (Lean.ParserDescr.symbol "fin")

@[reducible, inline]

abbrev HigherCategoryTheory.FinSucc (n : ℕ) : Type

Abbreviation for Fin (n + 1), used as the index type for $n$-categories in the many-sorted presentation.

Equations

• HigherCategoryTheory.FinSucc n = Fin (n + 1)

@[reducible, inline]

abbrev HigherCategoryTheory.TypeFamily (Index : Type) : Type (u + 1)

A family of types indexed by a preordered type, used as the carrier for many-sorted categories.

Equations

• HigherCategoryTheory.TypeFamily Index = (Index → Type ?u.7)

@[reducible, inline]

abbrev HigherCategoryTheory.NTypeFamily (n : ℕ) : Type (u + 1)

A family of types indexed by FinSucc n, used as the carrier for many-sorted $n$-categories.

Equations

• HigherCategoryTheory.NTypeFamily n = HigherCategoryTheory.TypeFamily (HigherCategoryTheory.FinSucc n)

@[reducible, inline]

abbrev HigherCategoryTheory.OmegaTypeFamily : Type (u + 1)

A family of types indexed by ℕ, used as the carrier for many-sorted $\omega$-categories.

Equations

• HigherCategoryTheory.OmegaTypeFamily = HigherCategoryTheory.TypeFamily ℕ

def HigherCategoryTheory.«term_≫_» : Lean.TrailingParserDescr

Notation for lt_trans, used to compose strict inequality proofs when passing index arguments to source, target, or composition operations in the many-sorted presentation. In any other context, prefer using lt_trans directly.

Equations

• One or more equations did not get rendered due to their size.