Registry · Definition I.D81 established formalized

I.D81 — CCC-Linear Dichotomy

CCC side has free diagonals, Lawvere barrier. Star-autonomous side has no free diagonals, no barrier.

Book I Part 18 Ch. 72

Dependency Graph

Depends on (3)

I.D78 I.T37 I.R19

Depended on by (2)

I.D89 I.T39

Lean Formalization

Module: TauLib.BookI.MetaLogic.StructuralExclusion

Symbol: CCCSide / StarAutonomousSide