Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: general

Topic: learning dependent type theory

Henri Tuhola (Jan 03 2023 at 17:28):

I am really interested about dependent types. However most of this still goes over my head.

Henri Tuhola (Jan 03 2023 at 17:33):

Mixing up terms and types would need some sort of an explanation.

Spencer Breiner (Jan 04 2023 at 00:57):

A good example is the space of parameters for the type of (ordinary, geometric) shapes.

For c=Circle: Shape, we might have $Param(c)\cong \R^2\times\R^+$, corresponding to center and radius, while for another element s=Square: Shape it could be $Param(s)\cong \R^2\times\R^+\times[0,\pi/2)$ for center, side length & orientation.

With dependent types, we can talk about a (type-safe) function that turns parameterized shapes into, e.g., svg code
$\sum_{x:Shape} Param(x) \to SVG$

Then we could write a function that takes a list of shapes and a default assignment of parameters for each shape, and use this to construct a larger SVG
$List(Shape)\times \prod_{x: Shape} Param(x) \to SVG$

Henri Tuhola (Jan 04 2023 at 02:27):

I mean that the theory goes over my head. I can use dependent types and understand your example very well. The problems come when it comes to theory.

For instance. How do fibrations exactly model the dependent types? Or if we take presheaves how do those work?

Josselin Poiret (Jan 04 2023 at 09:55):

the "basic" theory of dependent types isn't in any way linked to category theory, at least in the way it's usually presented. It's basically a multi-sorted algebraic theory! You can use some very categorical formulations of what those theories look like, through categories with families or even Awodey's natural models (the most concise formulation yet imho). The concept of fibrations is disjoint from the general theory of dependent types, but they provide a very important class of examples of such theories. The natural models paper is structured that way: first define what a dependent type theory is, then show that fibrations (or display maps) provide such a class of examples with such and such properties.

I personally look at it the other way around: dependent type theory is a language that you can use to reason about a bunch of different things, and fibrations are one of them! So if you are interested in fibrations, DTT lets you work with them syntactically.

Mike Shulman (Jan 04 2023 at 15:38):

Or, turning it around, anything that models dependent types behaves like a notion of "fibration"!

Henri Tuhola (Jan 04 2023 at 16:51):

Part of why I'm attracted to trying to understand some model for dependent types comes from universal constructions such as products and exponentials. How the reduction rules simply fall out from the definitions there.

I agree I probably won't need one if I just started using dependent types. I had not seen Awodey's natural models yet though.

Mike Shulman (Jan 04 2023 at 16:55):

What kind of background are you coming from?

Henri Tuhola (Jan 04 2023 at 17:07):

Hobbyist programmer for 25 years. I've used tons of different programming languages.

Mike Shulman (Jan 04 2023 at 17:08):

Do you understand categorical semantics of simple type theory?

Henri Tuhola (Jan 04 2023 at 17:14):

Unless I miss something, I do think so.

Mike Shulman (Jan 04 2023 at 17:23):

Good. I generally think it's best to start out thinking of dependent types as arbitrary maps, and then later observe that in the presence of higher identity types one wants them to be fibrations. We think of a dependent type $x:A \vdash B(x)$ as a family of objects $\{ B(x) \}_{x\in A}$, and represent it by the coproduct $\coprod_{x\in A} B(x)$ with its projection down to $A$. Conversely, any map $p:C\to A$ can be thought of as representing the family of all its fibers $p^{-1}(a)$, since $C \cong \coprod_{x\in A} p^{-1}(a)$.

Mike Shulman (Jan 04 2023 at 17:23):

I wrote a bit of an introduction to categorical semantics of dependent type theory in section 2 of the logic of space.

Josselin Poiret (Jan 04 2023 at 20:23):

regarding what I was saying above, I think it's better to only talk only about display maps first: they single out in the categorical model what arrows should model a proper type-on-type dependency through their fibers. In the case of a basic set model of let's say MLTT, seeing all arrows as defining dependent types works well enough, so you don't need to single out such a class. But if your intended semantics are groupoids, or spaces, etc., then you cannot just take all arrows: take $B = \{0\}$, $A = [0,1]$. There is an inclusion map $B \to A$, but you can see that the fiber-wise dependency on $[0,1]$ is not well-behaved when considering identity types: you cannot continuously transport elements over $0$ to elements over $1$! This means that you need a specific class of display maps, and here they would be Kan fibrations.

Jules Hedges (Jan 05 2023 at 15:07):

While trying to answer some tricky questions like this recently, I realised I don't know how to motivate Grothendieck fibrations specifically to someone coming from dependent type theory. It makes sense to me that dependent types behave like fibrations of spaces or groupoids or whatever undirected thing. Is there a neat way to motivate Grothendieck fibrations this way, or is that where the analogy stops?

Sam Speight (Jan 05 2023 at 16:02):

There are directed type theories, with hom types (directed-path types), where dependent types behave like fibrations of (infinity-)categories. As I understand, these were specifically designed to be a language for such things, so the motivation usually goes the other way round. But given some motivation for generalising identity types to hom types (which I'm sure one could find), this could motivate the generalisation of fibrations of groupoids to fibrations of categories.

Henri Tuhola (Jan 05 2023 at 17:02):

Maybe if I take a simple example, I may finally understand it: If I take a type (2 -> set), I could treat it as a type (A+B) with a fiber (A+B -> 2), with a limitation that I cannot directly access either A or B.

Henri Tuhola (Jan 05 2023 at 17:06):

Now I could only pullback with either Inl or Inr. Consider pullback with Inl. It would 'select' A and bring the fiber (A -> 1), giving the access to A.

Henri Tuhola (Jan 05 2023 at 17:07):

Ok, now I read the dao of FP again and see if I get further with it.

Henri Tuhola (Jan 05 2023 at 18:22):

Another way I can start to unravel this is to consider (a : set) -> a as a fibration.

Henri Tuhola (Jan 06 2023 at 08:32):

I think I'm on the edge of understanding this. I need to understand base change functor, a bit about slice categories and pullbacks.

Henri Tuhola (Jan 06 2023 at 08:35):

The a:set - case brings up an universe level, so it's probably not a good starting point. But the simple a+b case seem to work.

Josselin Poiret (Jan 06 2023 at 08:41):

Henri Tuhola said:

Another way I can start to unravel this is to consider (a : set) -> a as a fibration.

Yes, this is the universal fibration. If you want to see the semantics a bit more clearly, you need to use Tarski-style universes, so the function type is actually (a : Set) → El a, which is given by a universe in the semantics $El : Ũ → U$. $U$-small types are exactly those whose name come from $Set$, ie. pullbacks of the universe fibration. The example $A + B$ is not great imo, as $A + B$ is not directly a dependent type, just a sum of two closed types. Maybe you would want to consider $n : \mathbb{N} \vdash Fin(n)$ as a simple example instead, or to make a definition of your example more explicit you could define $K : Bool → Set$ by $K false = A$ and $K true = B$, and then you do have the dependent type you're looking for

Henri Tuhola (Jan 08 2023 at 15:53):

16731929930417209198029531058890.jpg

It almost makes sense. There are things that confuse me though.

Henri Tuhola (Jan 08 2023 at 16:06):

I tried to draw the adjunctions for dependent product and sum. I should get Unit and counit right? I am confused what the signature of counit turns out to be in product.

Eduardo Ochs (Jan 09 2023 at 04:24):

I would draw that diagram as this:

Eduardo Ochs (Jan 09 2023 at 04:24):

d.jpg

Eduardo Ochs (Jan 09 2023 at 04:27):

The details of the conventions that I use are here:
http://angg.twu.net/math-b.html#2022-md
Take a look at its section 8.12! =)

Notification Bot (Jan 09 2023 at 18:52):

28 messages were moved here from #general > learning CT by Matteo Capucci (he/him).

Henri Tuhola (Jan 10 2023 at 12:11):

In pullback/base change, is 'f' in itself a fiber/bundle? If so then that'd make a lots of sense.

Spencer Breiner (Jan 10 2023 at 12:17):

It can be, but not necessarily. It's better to think of f as a term that is being substituted into the definition of the dependent type.

Henri Tuhola (Jan 10 2023 at 12:20):

But why it ends up being defined before there is anything to substitute? In the introduction of the dependent function?

Henri Tuhola (Jan 10 2023 at 12:34):

I'm reading through "Topoi, the Categorial Analysis of Logic." it has helped me to understand these concepts.

Henri Tuhola (Jan 10 2023 at 13:01):

But had to take a break. Maybe I'll just be silent until I've read through.

Spencer Breiner (Jan 10 2023 at 13:18):

This is the picture that helped me
PXL_20230110_131528353~2.jpg

Spencer Breiner (Jan 10 2023 at 13:19):

But the picture on the right is just an elaborate way to construct a commutative triangle
PXL_20230110_131918726~2.jpg

Josselin Poiret (Jan 10 2023 at 13:34):

Spencer Breiner said:

This is the picture that helped me
PXL_20230110_131528353~2.jpg

what do those things correspond to? is this a construction, if so, of what starting from what?

Spencer Breiner (Jan 10 2023 at 13:46):

On the left we have three declarations, and on the right the associated categorical structure. In particular, the pullback is used to interpret the substitution of f into A, which is needed to give the type of a.

Spencer Breiner (Jan 10 2023 at 13:51):

From the diagrammatic perspective it's a bit roundabout because it's not easy to talk about a term that depends on one context in a type that depends on another. For me, it's easier to think about the partial section $Y\to A$ directly, and the (total) section of the pullback is just a device to fit it into type theory.

Spencer Breiner (Jan 10 2023 at 13:51):

Obviously a very important device...

Henri Tuhola (Jan 14 2023 at 13:52):

I finished with reading the book but didn't gain more insight into base change functor & it's adjoints. I guess I'm stuck with partial understanding. I've moved on... For now.