Algebraic theories with contexts, in cubical Agda

Practical remarks

For now, we use agda v2.6.2.

For the cubical library, we have a submodule. To clone, use

git clone --recurse-submodules

Further reading

See related links on my homepage.

General setup

Multisorted algebraic theories

In Mat, we define MATs (multisorted algebraic theories).

• Mat.Signature defines the "signature" of a MAT presentation, which is just a set of sorts.
• Mat.Free.Presentation defines the presentation of a free MAT, which is a sort-indexed container, and the corresponding functor Term1.
• Mat.Free.Term defines the free monad TermF.
• Mat.Free.Model defines the isomorphic categories catModel1 of algebras for Term1 and catModelF of Eilenberg-Moore algebras for TermF.
• Mat.Presentation defines the presentation of a MAT, which is a free MAT equipped with an equational theory.
• Mat.Term defines the monad TermQ.
• Mat.Model defines the isomorphic categories
  • catModel1Eq of algebras for Term1 that respect the equational theory,
  • catModelFEq of Eilenberg-Moore algebras for TermF that respect the equational theory,
  • catModel of Eilenberg-Moore algebras for TermQ.

Contextual multisorted algebraic theories

In Cmat, we define CMATs (contextual multisorted algebraic theories), as well as a few translations:

• The settling translation translates CMATs to MATs. It comes in two flavours:

  • The cold translation, which translates a free CMAT to a MAT with no substitution operations other than substitution composition,
  • The hot translation, which translates a free CMAT to a MAT with substitution operations. It extends to a translation from non-free CMATs to MATs.

  Both flavours have the same signature, and are indexed by a CMAT foundation, which determines what are the contexts of the resulting language.

• The levitating translation is actually a special case of the settling translations, which is indexed by a mode m0. To levitate a CMAT is to settle it on the foundation whose contexts at mode m are really junctors from m0 to m.

Different parts are added in different places. The following table gives a bit of an overview. It should be read as follows:

• The bold lines are titles,

• Under every bold line we list the operations added there,

• Operations from the left and from above (and from the upper-left) are also inherited,

• "Custom" stands for operations custom to the specific theory at hand.

  Custom	CMAT	Cold	Hot
  Signature	cmatsig	matsigSettled	matsigSettled
  Operations	fcmat	fmatCold	fmatHot
  Custom	id-jhom	idsub
  		gensub =	gensub =
  	comp-jhom	compsub	tmsub
  	whiskerL	mixWhiskerL
  	whiskerR	mixWhiskerR
  Equations		matCold	matHot
  			tmsub-inctx
  		compsub-lunit
  		compsub-runit	tmsub-runit
  		compsub-assoc	tmsub-assoc
  		Mixed whiskering
  		except 1 law
  Equational theory	cmat		matHotEq
  Custom	Whiskering		1 mixed wh law

The setup is as follows:

• Cmat.Signature defines

  • the signature of a CMAT presentation, consisting of:
    • a category of modes and junctors
    • custom right-hand-sides (to which we add the native RHSs for substitutions and junctor morphisms)
  • CMAT foundations, consisting of:
    • a covariant presheaf of contexts over the category of modes and junctors.
      • The translation is called settled in general,
      • The translation is called levitated if the presheaf of contexts is representable, meaning that junctors from the representing mode m0 serve as contexts.
  • the common MAT signature matsigSettled of the cold/hot translation.

• Cmat.Free.Presentation defines the presentation of a free CMAT, which is almost a RHS-indexed container, only we get to specify a junctor for every argument of every operator. It also defines the settling translation, indexed by a "temperature" (hot/cold):

  • The general settling translation: fmatSettled, matSettled
  • The cold translation: fmatCold, matCold
  • The hot translation: fmatHot, matHot

TBD