[agda] define model

[jonsterling]

• [ ] relative monads
• [ ] category of containers
• [x] telescopes
• [x] logical signature == container Valence :> Sort, with a distinguished sort jdg of judgments
• [ ] category of logical signatures
• [ ] functor J from a logical signature L to the set of L-judgments
• [ ] functor T from a logical signature L to the set of proof states for L
• [ ] show that T is a relative monad on J

[jonsterling]

Note: I have not yet convinced myself that the subst operation for dependent tactic trees actually obeys the (relative) monad laws. I hope it does, or if it doesn't, can be replaced with something that does.

[ghost]

So I've been thinking about adding relative monads to the groupoids library but haven't gotten around to it yet. We have monads now: here (see all the stuff above it for the context).

The way I was planning to do it was to define skew monoidal categories either as a separate structure or by modifying Monoidal to support both. However, in order to get the Kleisli extensions (bind) we also need a Closed structure (as in this) or some combined closed monoidal thing or just a direct formalization of extension systems. Should be pretty straightforward to do any of that, just a bit tedious.

The skew monoidal structures are essentially like the monoidal ones except the operations are only natural, not natural iso, if I remember right. Then you would define skew monoids on some functor, not necessarily on Endo. Uustalu describes the construction in one of his papers.

The category of containers (and of polynomials) is also something I was thinking about. The reason I added the fibration stuff recently was to be able to work with signatures and constructions on them as (lax monoidal) fibrations which is how some of the opetope stuff is described in the literature. I think it would be nicer to work with pseudofunctors and indexed monoidal categories for that but it would be good to have both approaches available.

[favonia]

FYI: the current code does not seem to compile under the development version of Agda, no matter I update the agda-prelude or not. I would actually suggest move the modeling to another repository because the testing needed for Agda code is very different from the main SML code.

[jonsterling]

@favonia I tend to keep little Agda sketches sometimes in the repository, without any expectation that it be tested or even continue to build over time. Probably it is better to delete it for now, as the agda code was written experimentally, as a way to figure out what this proof refinement structure should look like.

[jonsterling]

(The agda sketch is superseded by this paper: https://arxiv.org/abs/1703.05215)