Stream: Coq users

Topic: presenting a language

Christian Williams (Aug 27 2021 at 22:00):

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?

Paolo Giarrusso (Aug 27 2021 at 22:25):

where t \times s is really the pullback, right?

Christian Williams (Aug 27 2021 at 22:28):

yes

Paolo Giarrusso (Aug 27 2021 at 22:29):

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.

Paolo Giarrusso (Aug 27 2021 at 22:31):

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
…

Christian Williams (Aug 27 2021 at 22:32):

hm, yes I see. thanks

Christian Williams (Aug 27 2021 at 22:33):

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

Christian Williams (Aug 27 2021 at 22:34):

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
}.

Christian Williams (Aug 27 2021 at 22:35):

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

Paolo Giarrusso (Aug 27 2021 at 22:35):

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?

Paolo Giarrusso (Aug 27 2021 at 22:35):

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

Paolo Giarrusso (Aug 27 2021 at 22:38):

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

Christian Williams (Aug 27 2021 at 22:38):

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.

Christian Williams (Aug 27 2021 at 22:40):

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.

Christian Williams (Aug 27 2021 at 22:40):

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

Paolo Giarrusso (Aug 27 2021 at 22:42):

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

Paolo Giarrusso (Aug 27 2021 at 22:42):

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

Paolo Giarrusso (Aug 27 2021 at 22:44):

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

Christian Williams (Aug 27 2021 at 22:53):

hm, I see...

Paolo Giarrusso (Aug 27 2021 at 22:54):

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

Christian Williams (Aug 27 2021 at 22:54):

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

Christian Williams (Aug 27 2021 at 22:54):

oh okay. not much, just beginning

Christian Williams (Aug 27 2021 at 22:54):

I just have a category theory background

Paolo Giarrusso (Aug 27 2021 at 22:55):

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

Paolo Giarrusso (Aug 27 2021 at 22:56):

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

Christian Williams (Aug 27 2021 at 22:59):

okay

Paolo Giarrusso (Aug 27 2021 at 23:00):

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.

Christian Williams (Aug 27 2021 at 23:02):

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?

Christian Williams (Aug 27 2021 at 23:03):

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

Paolo Giarrusso (Aug 27 2021 at 23:03):

1. something like that

Paolo Giarrusso (Aug 27 2021 at 23:03):

2. we don’t really need to combine eq_arrow into that (and it would fail)

Paolo Giarrusso (Aug 27 2021 at 23:04):

but Inductive does not exactly define “a theory”

Paolo Giarrusso (Aug 27 2021 at 23:04):

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

Christian Williams (Aug 27 2021 at 23:06):

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

Christian Williams (Aug 27 2021 at 23:07):

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

Paolo Giarrusso (Aug 27 2021 at 23:08):

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

Paolo Giarrusso (Aug 27 2021 at 23:09):

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

Paolo Giarrusso (Aug 27 2021 at 23:09):

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.

Christian Williams (Aug 27 2021 at 23:11):

base elements? like generators?

Paolo Giarrusso (Aug 27 2021 at 23:11):

yeah :-)

Paolo Giarrusso (Aug 27 2021 at 23:12):

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.

Christian Williams (Aug 27 2021 at 23:12):

sure, thanks

Paolo Giarrusso (Aug 27 2021 at 23:12):

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.

Christian Williams (Aug 27 2021 at 23:13):

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

Christian Williams (Aug 27 2021 at 23:13):

I appreciate your help.

Paolo Giarrusso (Aug 27 2021 at 23:13):

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

Last updated: Oct 03 2023 at 04:02 UTC