def T₀ : AInfinityTheory.KLRWCategory 3 ℤ

Equations

• T₀ = { positioning := 0 }

def T₁ : AInfinityTheory.KLRWCategory 3 ℤ

Equations

• T₁ = { positioning := 1 }

def T₂ : AInfinityTheory.KLRWCategory 3 ℤ

Equations

• T₂ = { positioning := 2 }

def T₃ : AInfinityTheory.KLRWCategory 3 ℤ

Equations

• T₃ = { positioning := 3 }

def X : ℤ → AInfinityTheory.AddKLRWCategory 3 ℤ

Equations

• X 0 = { toList := [T₀, T₁] }
• X 1 = { toList := [T₂, T₃] }
• X x✝ = 𝟎

def d (i : ℤ) : X i ⟶ X (i + 1)

Equations

• One or more equations did not get rendered due to their size.
• d x✝ = 0

def g (i : ℤ) : X i ⟶ X i

Equations

• One or more equations did not get rendered due to their size.
• g x✝ = 0

def A : AInfinityTheory.KLRWComplexCategory 3 ℤ

Equations

• A = BoundedCochainComplex.of X {0, 1} ⋯ d ⋯

def f : A ⟶ A

Equations

• f = BoundedCochainComplex.ofHom X {0, 1} d ⋯ ⋯ X {0, 1} d ⋯ ⋯ g ⋯