Stream: Miscellaneous

Topic: Category theory foundations?

walker (Mar 03 2023 at 12:34):

Is there a book like software foundations but for category theory?

I mean interactive proofs with coq, with assignments, and things like that ?
Edit: I wouldn't mind books that comes with third party formalization.

I am struggling to learn category theory (for the purposes of understanding categories with families model) and the hope is formal model will help me understand things more

Notification Bot (Mar 03 2023 at 12:34):

walker has marked this topic as resolved.

Notification Bot (Mar 03 2023 at 12:34):

walker has marked this topic as unresolved.

James Wood (Mar 03 2023 at 12:54):

My guess would be that there's not even enough material that such a book would be based upon. Last time I checked, agda-categories was the most extensive mechanised category theory library, and that's maybe only just big enough to be the basis of a small textbook (comparable to Benjamin Pierce's book, Basic Category Theory for Computer Scientists).

James Wood (Mar 03 2023 at 12:58):

A much smaller Agda option would be the relevant part of some year's Strathclyde CS410 (particularly the videoed year), and maybe there's a Coq equivalent.

walker (Mar 03 2023 at 13:16):

It is really unfortunate (for me) but thanks a lot for pointing out my available options.

Pierre-Marie Pédrot (Mar 03 2023 at 13:17):

I'm not sure you need much category theory for CwFs, they are quite anti-categorical in spirit (families are sets !)

walker (Mar 03 2023 at 13:20):

well, what I need to to understand them, which I cannot by just reading paper, I memorized the definition literally, in Internal Type theory paper, and the paper n unityped, simply typed, and dependently typed. and still the rest of the papers make no sense to me

walker (Mar 03 2023 at 13:26):

If anyone would be kind enough to spend time to explain to me (ideally over zoom) or guide me through understanding the papers on cwfs, they will earn my ever lasting gratitude

My current understanding of category theory is limited ((co-)products, cats, functors, and natural transformations on very basic level (definitions + basic examples))

My understanding of MLTT is enough to have formalization of MLTT in coq.

Pierre-Marie Pédrot (Mar 03 2023 at 13:27):

CwFs are just a particular encoding of TT that allows stratifying the syntax (i.e. you don't need higher-order syntax)

Pierre-Marie Pédrot (Mar 03 2023 at 13:28):

but apart from that it's literally just good old deBruijn type theory

Pierre-Marie Pédrot (Mar 03 2023 at 13:29):

you define it by layers : first the contexts (which have a category structure, and you call morphisms between them substitutions)

walker (Mar 03 2023 at 14:13):

That means that basically in the category of contexts every morphism will eventually lead to a small context right?
Also in the definition they say:

Functor T: C op ----> Fam Fam here is just the hierarchy of universe of types right ?

Also I am failing to comprehend some of the notations here:
image.png

from this paper: https://www.cse.chalmers.se/~peterd/papers/InternalTT.pdf
Γ |- A = Π ( γ ∈ Γ), A(γ)

In the paper, γ is given for substitutions but then i is not clear what it means to say γ ∈ Γ

But if you assume that γ is a type stored in Γ then A(γ) does not make sense to me

Also I cannot unerstand the difference betweena[γ] and a(γ)

Paolo Giarrusso (Mar 03 2023 at 14:14):

γ ∈ Γ means that's a substitution matching Gamma

walker (Mar 03 2023 at 14:15):

what does that mean? :sweat_smile:

is it:
a) γ : Γ -> Γ'
b) γ : Γ' -> Γ

Paolo Giarrusso (Mar 03 2023 at 14:17):

sorry, spoke too quickly! That's the category of sets; contexts are the category's objects, aka sets.

Paolo Giarrusso (Mar 03 2023 at 14:20):

and in this example A(γ) makes sense because A ∈ Type(Gamma), and Type(Gamma) contains families sets indexed by Gamma — A(y) applies the family to an index

Paolo Giarrusso (Mar 03 2023 at 14:23):

(or rather, it "typechecks" — I'm not that sure where that example is going)

Paolo Giarrusso (Mar 03 2023 at 14:23):

In general, have you considered something like Hofmann's PhD thesis? IIRC chapter 2 has a good summary of categories with families...

Pierre-Marie Pédrot (Mar 03 2023 at 14:38):

the paper defines a specific CwF, which is Sets (i.e. set is a model of type theory)

Pierre-Marie Pédrot (Mar 03 2023 at 14:39):

in this case contexts are sets, so it makes sense to write γ ∈ Γ

Pierre-Marie Pédrot (Mar 03 2023 at 14:44):

the notation is parsed as (Γ ⊢ A) := (Π(γ ∈ Γ). A(γ)) i.e. we define "A is a dependent type in context Γ" to be "A is a dependent function from Γ to Set"

walker (Mar 03 2023 at 14:50):

oh this this γ has nothing to do with the usage of γ before which was for substitution (morphisms between Γs?) is that correct ?

James Wood (Mar 03 2023 at 14:51):

I don't know the context, but I want to read the first equation as

$$\llbracket \Gamma \vdash A \rrbracket = \prod_{\gamma \in \llbracket \Gamma \rrbracket} \llbracket A \rrbracket(\gamma)$$

If that's what it's meant to be, then it makes sense to me.

walker (Mar 03 2023 at 14:54):

I am not sure I am following, but I will try to read chapters 1,2 of hoffman's thesis and see If I no longer have notation confusion, then I will come back with more questions

James Wood (Mar 03 2023 at 14:59):

Okay, upon reading, I see that $\vdash$ is a notation given by the CwF definition, rather than the syntax of some type theory, so the semantic brackets don't make formal sense. The reader is probably supposed to have something like this in mind, though.

James Wood (Mar 03 2023 at 15:06):

I guess, are you familiar with what the simply typed version of this example would look like? You should end up with definitions that look like

$$\Gamma \vdash A = \Gamma \to A \\ [] = 1 \\ \Gamma; A = \Gamma \times A$$

James Wood (Mar 03 2023 at 15:13):

The use of $\gamma$ as the name of a substitution in the paragraph above seems like a bit of an odd choice, but I guess it's justifiable by the fact that a $\gamma \in \Gamma$ corresponds to a substitution $\gamma : [] \to \Gamma$. The latter is more general, because the expression $\gamma \in \Gamma$ only makes sense in the set model, while $[] \to \Gamma$ is a hom set in any CwF. The key word is global element.

Patrick Nicodemus (Mar 03 2023 at 22:27):

not formal, just rigorous math books:
there's Category Theory for Computing Sciences by Barr and Wells
also "Computational Category Theory" by Rydehead and Burstall
Probably "Introduction to Categories and Categorical Logic" by Samson Abramsky would be suitable

Patrick Nicodemus (Mar 03 2023 at 22:29):

I hope this is a useful hint: what category theorists call 'universal properties' are analogous to introduction and elimination rules in type theory coupled with the reduction rules that relate them.
There are some places where this analogy breaks down but it's probably helpful for basic examples.

Alexander Gryzlov (Mar 03 2023 at 23:02):

Category theory in general is notoriously hard to mechanize properly, the main reason is that the design space is quite large, and many small design decisions quickly snowball into big ergonomic issues.

Jason Rute (Mar 04 2023 at 03:22):

One project that might interest you is translating the examples from Category theory for programmers into Coq (from Haskell), or even just using Coq to do the exercises. All the proofs (or just those from the exercises) can be formalized as well, and it should be fairly natural since the definitions are already associated with functional code. Just to be clear, this would be a programmers version of category theory where one constructs things like (lawful) monads and other objects of interest to developers, and the main category of interest is Type (where the arrows are functions f : Type -> Type). For an example of the distinction, Lean's mathlib actually has two category theory libraries:

• The control library is programmer category theory with definitions like (lawful) monads. There are also theorems, but they are mostly practical results about lawful objects. This is similar to the way CTFP is taught.
• The category_theory library is about general categories and has different definitions, including of the same objects, like monads. The theorems are also more mathematical, e.g. the yoneda lemma.

Karl Palmskog (Mar 04 2023 at 06:12):

small survey of category theory libraries in Coq to (possibly) use: https://coq.discourse.group/t/survey-of-category-theory-in-coq/371

walker (Mar 04 2023 at 14:12):

@Jason Rute I once tried the lectures by Milewski, and it felt too basic and the examples were not well motivated

walker (Mar 04 2023 at 14:13):

in fact barr's book is what I am currently reading, I just wish I could close my eyes, open it again and find myself done with the book and all of the exercises

walker (Mar 04 2023 at 14:15):

I also liked the idea that there is zero notation abuse, it feels very very formal which makes things easier to understand

Paolo Giarrusso (Mar 04 2023 at 14:21):

Re notation let me answer one subtle question

Also I cannot unerstand the difference between a[γ] and a(γ)

James already answered (indirectly), but if you want, a[γ] is an operator that's part of the CwF "interface" — it's the action of substitution γ on term a, like + is part of the group "interface" (even if mathematicians would use different words). The ITT paper then shows how the "CwF of sets" _implements_ this operation, and that uses a(γ)

Last updated: Sep 25 2023 at 12:01 UTC