Loj

Loj is a category formed from Lojban syntax. Specifically, it is the poset (WP, nLab) whose:

  • objects are equivalence classes of closed well-formed bridi, and
  • arrows are implications from one bridi to another.

To read Metamath theorems as statements about Loj, encode:

  • objects as members of the {broda} series
  • arrows from X to Y as {ganai X gi Y}
  • pasting diagrams as applications of ax-mp
  • Isomorphisms from X to Y as {go X gi Y}

Note that while Loj is thin, its formal verification in Metamath is non-thin; there are multiple possible proofs for some statements. This is not a serious issue.

Category

Identity arrows exist. Composition is allowed, well-typed, and internalized.

NameStatement
idganai broda gi broda
sylganai broda gi brode & ganai brode gi brodiganai broda gi brodi
ganai-comp-lrganai ganai broda gi brode gi ganai ganai brode gi brodi gi ganai broda gi brodi
ganai-comp-rlganai ganai broda gi brode gi ganai ganai brodi gi broda gi ganai brodi gi brode

Initial Object

Trivial falsehood is the initial object.

NameStatement
gaiho-initganai gai'o gi broda

Terminal Object

Trivial truth is the terminal object.

NameStatement
ceihi-termganai broda gi cei'i

Products

Conjunction is the categorical product. Conjunction is a lower bound on the left and right, and indeed the least lower bound; in other words, all binary conjunctions exist. Conjunction is idempotent and commutes. In addition to the standard product, pointwise conjunctions of arrows are possible. Conjunction distributes over disjunction, making Loj into a distributive category.

NameStatement
ax-ge-leganai ge broda gi brode gi broda
ax-ge-reganai ge broda gi brode gi brode
ge-prodganai broda gi brode & ganai broda gi brodiganai broda gi ge brode gi brodi
ge-idemgo ge broda gi broda gi broda
ge-comgo ge broda gi brode gi ge brode gi broda
ge-pairganai broda gi brode & ganai brodi gi brodoganai ge broda gi brodi gi ge brode gi brodo
ge-dist-gago ge broda gi ga brode gi brodi gi ga ge broda gi brode gi ge broda gi brodi

Coproducts

Disjunction is the coproduct. Disjunction is an upper bound on the left and right, and indeed the greatest upper bound; in other words, all binary disjunctions exist. Disjunction is idempotent and commutes. In addition to the standard coproduct, pointwise disjunctions of arrows are possible. Disjunction distributes over conjunction, making Loj into a distributive lattice and therefore a distributive category.

NameStatement
ga-linganai broda gi ga broda gi brode
ga-ringanai broda gi ga brode gi broda
ga-sumganai broda gi brode & ganai brodi gi brodeganai ga broda gi brodi gi brode
ga-idemgo ga broda gi broda gi broda
ga-comgo ga broda gi brode gi ga brode gi broda
ga-pairganai broda gi brode & ganai brodi gi brodoganai ga broda gi brodi gi ga brode gi brodo
ga-dist-gego ga broda gi ge brode gi brodi gi ge ga broda gi brode gi ga broda gi brodi

Core

The core of a category is the groupoid which includes all of its isomorphisms. The core of Loj, written Core(Loj), is the groupoid whose:

  • objects are equivalence classes of bridi, and
  • arrows are bi-implications from one bridi to another.

To read Metamath theorems as statements about Core(Loj), encode:

  • objects as members of the {broda} series
  • arrows from X to Y as {go X gi Y}
  • pasting diagrams as applications of bi

The core is a category.

NameStatement
go-idgo broda gi broda
go-sylgo broda gi brode & go brode gi brodigo broda gi brodi

The core is a subcategory. The core is its own opposite category.

NameStatement
go-ganaigo broda gi brodeganai broda gi brode
go-comigo broda gi brodego brode gi broda

Because Loj is thin, there is an embedding from any pair of inverse arrows to the corresponding core arrow.

NameStatement
isoganai broda gi brode & ganai brode gi brodago broda gi brode

Double Negation

Negating a bridi twice, known as double negation (WP, nLab), is a functorial action which maps classical logic to intuitionistic logic. It can also be constructed as an endofunctor on intuitionistic logic, which yields a continuation monad. The functor's image yields a category whose:

  • objects are (equivalence classes of) refutations of supposed counterexamples to bridi, and
  • arrows are implications from one refutation-equipped bridi to another.

The functor is covariant.

NameStatement
nakunakuganai broda gi naku naku broda