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
walker has marked this topic as resolved.
walker has marked this topic as unresolved.
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).
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.
It is really unfortunate (for me) but thanks a lot for pointing out my available options.
I'm not sure you need much category theory for CwFs, they are quite anti-categorical in spirit (families are sets !)
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
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.
CwFs are just a particular encoding of TT that allows stratifying the syntax (i.e. you don't need higher-order syntax)
but apart from that it's literally just good old deBruijn type theory
you define it by layers : first the contexts (which have a category structure, and you call morphisms between them substitutions)
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(γ)
γ ∈ Γ
means that's a substitution matching Gamma
what does that mean? :sweat_smile:
is it:
a) γ : Γ -> Γ'
b) γ : Γ' -> Γ
sorry, spoke too quickly! That's the category of sets; contexts are the category's objects, aka sets.
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
(or rather, it "typechecks" — I'm not that sure where that example is going)
In general, have you considered something like Hofmann's PhD thesis? IIRC chapter 2 has a good summary of categories with families...
the paper defines a specific CwF, which is Sets (i.e. set is a model of type theory)
in this case contexts are sets, so it makes sense to write γ ∈ Γ
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"
oh this this γ has nothing to do with the usage of γ before which was for substitution (morphisms between Γs?) is that correct ?
I don't know the context, but I want to read the first equation as
If that's what it's meant to be, then it makes sense to me.
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
Okay, upon reading, I see that 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.
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
The use of 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 corresponds to a substitution . The latter is more general, because the expression only makes sense in the set model, while is a hom set in any CwF. The key word is global element.
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
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.
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.
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:
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.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.small survey of category theory libraries in Coq to (possibly) use: https://coq.discourse.group/t/survey-of-category-theory-in-coq/371
@Jason Rute I once tried the lectures by Milewski, and it felt too basic and the examples were not well motivated
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
I also liked the idea that there is zero notation abuse, it feels very very formal which makes things easier to understand
Re notation let me answer one subtle question
Also I cannot unerstand the difference between
a[γ]
anda(γ)
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