3
$\begingroup$

I think I've been able to puzzle out the free Lawvere theory on a collection of function symbols ought to have maps being just tuples of the free monad.

In Coq

Inductive term {A} (X: A -> nat) B :=
| var (x: B)
| roll x (Fin.t (X x) -> term X B).

Definition Mor {S} (X: S -> nat) A B := Fin.t B -> term X (Fin.t A).

And you use regular monadic composition.

My actual code uses the vector type instead but let's be simple.

But this doesn't seem quite right to me. The "free Lawvere theory" ought to be adjoint to a forgetful functor. The free monad stuff sort of works but I can't figure out the formal way to think about this. Fully generally you want something silly like a free 2-functor $\text{Dis}(\text{FinSet}) \rightarrow \text{Cat}\setminus\text{FinSet}$. Not at all sure here.

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ By "free Lawvere theory", do you mean a theory generated by a sginature (A and X above), and no equations? That's just a W-type. Also, it would be better to have X : A -> Type, i.e., replace the number with the type of that cardinality. Then, in concrete cases you ca set X a = Fin (f n) for some f : X -> nat. This might help. $\endgroup$
    – Andrej Bauer
    Jun 20 at 5:07
  • $\begingroup$ @AndrejBauer thanks that looks interesting. I'm still going to need to restrict to finite arities because I'm planning on doing some first order logic stuff with this. I'm also not sure what you mean by the theory being just the W-type. It sort of makes sense to me but I don't see how you can mechanically introspect it for doing logic stuff? Not sure what the proper name and definition for the finite version is. $\endgroup$
    – Molossus Spondee
    Jun 20 at 18:15
  • 2
    $\begingroup$ You should not restrict to finite arities until much later. If you compare your proofs with mine, you will see that the more general arities are clearly easier to formalize. In specific cases, such as first-order logic, you can then specialize to finite arities. But that comes much later. $\endgroup$
    – Andrej Bauer
    Jun 21 at 6:06
  • 1
    $\begingroup$ By the way, what is your question? $\endgroup$
    – Andrej Bauer
    Jun 21 at 6:08

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.