Stream: Miscellaneous

Topic: Category theory foundations?


view this post on Zulip 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

view this post on Zulip Notification Bot (Mar 03 2023 at 12:34):

walker has marked this topic as resolved.

view this post on Zulip Notification Bot (Mar 03 2023 at 12:34):

walker has marked this topic as unresolved.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip walker (Mar 03 2023 at 13:16):

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

view this post on Zulip 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 !)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Mar 03 2023 at 13:28):

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

view this post on Zulip 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)

view this post on Zulip 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(γ)

view this post on Zulip Paolo Giarrusso (Mar 03 2023 at 14:14):

γ ∈ Γ means that's a substitution matching Gamma

view this post on Zulip walker (Mar 03 2023 at 14:15):

what does that mean? :sweat_smile:

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

view this post on Zulip 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.

view this post on Zulip 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 GammaA(y) applies the family to an index

view this post on Zulip Paolo Giarrusso (Mar 03 2023 at 14:23):

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

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Mar 03 2023 at 14:39):

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

view this post on Zulip 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"

view this post on Zulip 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 ?

view this post on Zulip James Wood (Mar 03 2023 at 14:51):

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

ΓA=γΓA(γ)\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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

ΓA=ΓA[]=1Γ;A=Γ×A\Gamma \vdash A = \Gamma \to A \\ [] = 1 \\ \Gamma; A = \Gamma \times A

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Jun 05 2023 at 10:01 UTC