Litters

In this file, we define litters, which are the parts of an indexed partition of the base type of our model. Each litter is indexed by an element of μ, as well as some parameters β and γ used for defining the fuzz map later.

structure ConNF.Litter [Params] : Type u

The type indexing the partition of the base type of our model. The field ν : μ is an index that enforces that there are μ litters. The fields β and γ are used in the definition of the fuzz map, which is an injection into the type of litters.

• ν : μ
• β : TypeIndex
• γ : Λ
• β_ne_γ : self.β ≠ ↑self.γ

instance ConNF.instNonemptyLitter [Params] : Nonempty Litter

The type of litters is nonempty.

def ConNF.litterEquiv [Params] : Litter ≃ { a : μ × TypeIndex × Λ // a.2.1 ≠ ↑a.2.2 }

Strips away the name of the type of litters, converting it into a combination of types well-known to mathlib.

Equations

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

@[simp]

theorem ConNF.card_litter [Params] : Cardinal.mk Litter = Cardinal.mk μ

There are precisely μ litters.

Notation typeclasses

We will use Lean's typeclasses to implement some custom notation, namely the superscripts ᴸ, ᴬ, ᴺ, ᵁ, which will be used for converting between various common types (such as litters). The meanings of the notations are type-dependent.

class ConNF.SuperL (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ᴸ notation. Used for converting to litters, or extracting the "litter part" of an object.

• superL : X → Y

class ConNF.SuperA (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ᴬ notation. Used for converting to atoms, or extracting the "atom part" of an object.

• superA : X → Y

class ConNF.SuperN (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ᴺ notation. Used for converting to near-litters, or extracting the "near-litter part" of an object.

• superN : X → Y

class ConNF.SuperU (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ᵁ notation. Used for forgetful operations.

• superU : X → Y

def ConNF.«term_ᴸ» : Lean.TrailingParserDescr

Equations

• ConNF.«term_ᴸ» = Lean.ParserDescr.trailingNode `ConNF.«term_ᴸ» 1024 1024 (Lean.ParserDescr.symbol "ᴸ")

def ConNF.«term_ᴬ» : Lean.TrailingParserDescr

Equations

• ConNF.«term_ᴬ» = Lean.ParserDescr.trailingNode `ConNF.«term_ᴬ» 1024 1024 (Lean.ParserDescr.symbol "ᴬ")

def ConNF.«term_ᴺ» : Lean.TrailingParserDescr

Equations

• ConNF.«term_ᴺ» = Lean.ParserDescr.trailingNode `ConNF.«term_ᴺ» 1024 1024 (Lean.ParserDescr.symbol "ᴺ")

def ConNF.«term_ᵁ» : Lean.TrailingParserDescr

Equations

• ConNF.«term_ᵁ» = Lean.ParserDescr.trailingNode `ConNF.«term_ᵁ» 1024 1024 (Lean.ParserDescr.symbol "ᵁ")