Hi, I'm interested in presenting languages in Coq. For example, the language of categories is given by sorts $A$ for arrows and $O$ for objects, constructors for source and target $s,t :A\to O$, with composition $\circ: t\times s\to A$ and identity $i: O\to A$, plus associativity and unitality equations. How can this presentation be given in Coq, so that we can reason in this language?

where `t \times s`

is really the pullback, right?

yes

For many languages the syntax can be described directly in Coq via inductives — but as usual, category theory is more challenging to formalize, e.g. this pullback is already trickier:

```
Inductive arrow : Set where
| identity : object -> arrow
| comp : arrow -> arrow -> arrow
with object : Set where
| src : arrow -> object
| dst : arrow -> object.
```

I hope somebody else has a smarter idea! It’d be nice to define this directly, but I think this would need induction-induction, which is not (yet) supported in Coq (?):

```
Inductive arrow : object -> object -> Set where
…
with object : Set where
…
```

hm, yes I see. thanks

I just noticed that someone asked the same question a few hours ago https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/New.20Stack.20Exchange.20question/near/250985540

```
Record Category := {
Ob : Type ;
Hom : Ob -> Ob -> Type ;
comp : forall {a b c}, Hom b c -> Hom a b -> Hom a c ;
id : forall {x}, Hom x x ;
Assoc :
forall a b c d (f : Hom c d) (g : Hom b c) (h : Hom a b),
comp f (comp g h) = comp (comp f g) h ;
LeftId : forall a b (f : Hom a b), comp id f = f ;
RightId : forall a b (f : Hom a b), comp f id = f ;
Truncated : forall a b (f g : Hom a b) (p q : f = g), p = q
}.
```

I suppose this method gets around the need for pullback? like the concept of generalized algebraic theory

If that's relevant, I was probably mislead by "presenting a language"; I thought you wanted to reason about the syntax of words in the language?

(this category theory library uses a similar approach: https://github.com/jwiegley/category-theory/blob/master/Theory/Category.v#L38)

in these examples, values of type `Category`

_are_ categories (or if you want, structures/models of that language); if that’s what you want, that’s alright

yes, I'm looking for a way to present categories with structure, such as "Theory(Cat)" as a category with finite limits, in such a way that we can reason about morphisms (terms) in the internal language of such a category.

well, for now I mainly care about the theory itself or the "free model". but yes, it would also be useful to reason about models as well.

what would be any alternative to that? sorry I'm not yet seeing what distinction we're making.

Ah, the distinction is exactly the one between “free model” and “all models”.

And the records above lets you reason about “all models” without letting you reason about the free model.

While using inductive types gives an immediate way to build free theories, but does not (immediately) account for equations…

hm, I see...

okay, I can see an idea, tho I’m sure it’s not the simplest. How much Coq are you already familiar with?

so you're saying inductive types are like free models, but they currently have limitations - no equations, no "forall", etc

oh okay. not much, just beginning

I just have a category theory background

some “forall” is there, depending on what you mean, but equations are trickier.

On top of inductives, one can use quotients to encode equations, or reason “explicitly” about the equalities.

okay

For instance, after writing my first snippet, and something like (untested):

```
Inductive eq_arrow : arrow -> arrow -> Set where
| id_l : forall a, eq_arrow (comp identity a) a
| id_r : forall a, eq_arrow (comp a identity) a
| assoc : forall a b c, eq_arrow (comp (comp a b) c) (comp a (comp b c)).
```

then the type `eq_arrow f g`

is a type containing the proofs (if any) that `f`

and `g`

are equal according to associativity and unitality.

hm, I see. so in the first snippet, you made a multisorted theory by first saying "arrow" and then later saying "with object" to give the sorts that arrow depends on. is that right?

then following that logic, we could also combine eq_arrow into that inductive type? eq_arrow depends on arrow depends on object

- something like that

- we don’t really need to combine
`eq_arrow`

into that (and it would fail)

but `Inductive`

does not exactly define “a theory”

it defines the two sorts, then adds “constructors” and gives their sorts.

alright, sure. so for some reasons it's good to keep the equational reasoning separate, okay.

and then do we somehow quotient arrow by eq_arrow? or something to that effect

This keeps them separate — there are ways, but trying to point you at them would be a didactic crime…

at least this early — there are many subtle differences between inductives and multisorted theory, so what I started was just a hint…

And as a technical correction, we need to add base elements:

```
Inductive arrow (A O : Set) : Set where
| base_arr : A -> arrow A O
| identity : object A O -> arrow A O
| comp : arrow A O -> arrow A O -> arrow A O
with object (A O : Set) : Set where
| base_ob : O -> Set
| src : arrow A O -> object A O
| dst : arrow A O -> object A O.
```

base elements? like generators?

yeah :-)

However: to make sense of this, I must direct you at some Coq introduction first (say, https://softwarefoundations.cis.upenn.edu/lf-current/toc.html); at least you should get to the point where `Inductive`

is presented.

sure, thanks

That book is more aimed at computer scientists than mathematicians or category theorists, but since you are interested in working with free models, that might be closer to what you need, and is a decent introduction to Coq anyway.

great! I can look at this and get back to you later

I appreciate your help.

FWIW, somebody else might have very different suggestions, and I’m curious about those :-)

Last updated: Jun 24 2024 at 01:01 UTC