Registry · Lemma VII.L31 conjectural formalized

VII.L31 — OR1+OR2 Narrowing

Yoneda + finite signature constrain F to finitely generated locally small category with full Yoneda property, forcing axiom candidates.

Book VII Part 2 Ch. 29

Dependency Graph

Depends on (1)

VII.D37

Lean Formalization

Module: TauLib.BookVII.Meta.Saturation

Symbol: Tau.BookVII.Meta.Saturation.or12_narrowing