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: learning: questions

Topic: HoTT book

Jason Erbele (Feb 20 2021 at 02:10):

I have seen a bunch of stuff that has piqued my interest in Homotopy Type Theory, so I've made a few stabs at digging into the HoTT book. As I have no formal training in type theory, I've gotten bogged down in the details in chapter 1 every time. I am thinking about making another stab at it, so I have a pair of related questions:

1. How essential is it for me to understand the nitty gritty details of this intro to type theory in order to understand the remainder of the book? I'm pretty comfortable with things like $\lambda$ abstraction and currying, but I expect it doesn't bode well to have to refer back to the section on $\Pi$ types every few paragraphs (or sentences :grimacing:) before even getting to the section on $\Sigma$ types...
2. Is there a better resource to be using for this introductory material for someone who ultimately wants to understand HoTT?

I'm not sure I want to start a reading group just yet, but the type of answer I might give to that (implicit) question in the future may be dependent on the answers to the enumerated questions. :upside_down:

John Baez (Feb 20 2021 at 03:12):

I hope you know $\Pi$ is a fancy name for "cartesian product", which includes "and", while "$\Sigma$" means "sum" (= "coproduct" = "disjoint union") which includes "or".

John Baez (Feb 20 2021 at 03:14):

I think if you keep these things in mind, and go through some examples to make sure you understand why "and" is a product and "or" is a coproduct, you can nod and say "yeah, that makes sense" when the book says stuff about $\Pi$ types and $\Sigma$ types.

John Baez (Feb 20 2021 at 03:15):

I think feeling that stuff makes sense is probably enough at first; you don't need to worry too much about how a few basic axioms imply all the rest.

Jason Erbele (Feb 20 2021 at 04:12):

Those "fancy names" are what I have as my fallback intuitive understanding, but that doesn't seem to quite correspond to how the HoTT book defines $\Pi$ and $\Sigma$ types. There, $\Pi$ types are dependent function types, and $\Sigma$ types are dependent pair types. Product (cartesian product) and coproduct types are introduced after $\Pi$ and $\Sigma$ types, respectively. That might be part of what's contributing to my confusion.

Jason Erbele (Feb 20 2021 at 04:15):

The relation between and/or and product/coproduct is almost second-nature for me. Maybe I should give an example of the kind of thing I'm getting hung up on.

Joshua Meyers (Feb 20 2021 at 04:44):

If you could give an example, I could probably help. I read the first chapter of the HoTT book in December and it made sense to me.

Joshua Meyers (Feb 20 2021 at 04:47):

A conventional cartesian product $A_0\times A_1\times A_2$ is really just the set of dependent functions $f:\prod_{i\in 3} A_i$. A particular tuple $(a_0,a_1,a_2)$ corresponds to the dependent function sending $i\in 3$ to the element $a_i \in A_i$.

Joshua Meyers (Feb 20 2021 at 04:48):

Not sure if this addresses your confusion though...

Jason Erbele (Feb 20 2021 at 04:57):

Shortly after showing every element of a product type is equal to an ordered pair:

[...] we call the resulting function induction for product types: given $A,B : \mathcal{U}$ we have
$\mathsf{ind}_{A\times B} : \Pi_{C:A\times B \rightarrow \mathcal{U}} (\Pi_{(x:A)} \Pi_{(y:B)} C((x,y))) \rightarrow \Pi_{x:A\times B} C(x)$
with the defining equation
$\mathsf{ind}_{A\times B} (C,g,(a,b)) :\equiv g(a)(b)$

Checking that the type of the defining equation matches the type stated is making my head spin. And it doesn't help that the defining equation line is right after a pagebreak.

Jason Erbele (Feb 20 2021 at 04:59):

As I understand it, the scope of the first $\Pi$ extends all the way to the $C(x)$. My intuition for how the HoTT book explains $\Pi$ types is that we have a dependent function from something of the type $(A \times B \rightarrow \mathcal{U})$ to something of the type "everything after the $\Pi$", where $C$ is the variable that, when evaluated at a particular $c$, will set the type of the expression.
I'm guessing this isn't the best intuition, but it seems to fit the earlier, simpler examples, where $(\Pi_{x:A} B(x))(a)$ is the type $B(a)$. That is we get something where $a \mapsto B(a)$.

Jason Erbele (Feb 20 2021 at 05:03):

I figure I ought to be able to type check things so that when I actually go do stuff I can make that first sanity check that I might not be spewing nonsense.

Joshua Meyers (Feb 20 2021 at 05:08):

OK so here's an intuition for $\mathsf{ind}_{A\times B}$. You can think of it as a $(C:A\times B\to\mathcal{U})$-indexed family of functions of type $(\Pi_{(x:A)} \Pi_{(y:B)} C((x,y))) \rightarrow \Pi_{x:A\times B} C(x)$

Joshua Meyers (Feb 20 2021 at 05:09):

So we have $\mathsf{ind}_{A\times B}(C):(\Pi_{(x:A)} \Pi_{(y:B)} C((x,y))) \rightarrow \Pi_{x:A\times B} C(x)$.

Joshua Meyers (Feb 20 2021 at 05:11):

What does $\mathsf{ind}_{A\times B}(C)$ do? It takes a curried function $x\mapsto (y\mapsto p(x,y))$ and outputs an uncurried function $(x,y)\mapsto p(x,y)$.

Joshua Meyers (Feb 20 2021 at 05:14):

Does this address your confusion?

Jason Erbele (Feb 20 2021 at 05:15):

So where did $p$ come from? Is it the uncurried version of $g$? And then why does the $\mathsf{ind}_{A\times B}$ defining equation end up with the curried function $g(a)(b)$?

Joshua Meyers (Feb 20 2021 at 05:16):

Yes $p$ is the uncurried version of $g$.

Joshua Meyers (Feb 20 2021 at 05:17):

The defining equation is uncurrying $g$. We can write $p\coloneqq \mathsf{ind}_{A\times B}(C,g)$. Then the defining equation becomes $p(a,b)=g(a)(b)$.

Jason Erbele (Feb 20 2021 at 05:19):

As stated in the HoTT book, $\mathsf{ind}_{A\times B}$ seems to be taking the following input: $C: A\times B \rightarrow \mathcal{U}$, the curried function $g$, and the ordered pair $(a,b)$, and outputs the curried function applied to $a$ and $b$.

Joshua Meyers (Feb 20 2021 at 05:19):

Well, the defining equation is saying that when we apply $\mathsf{ind}_{A\times B}(C)$ to uncurry $g$, the result must truly be an uncurrying of $g$. So when we plug $(a,b)$ into $\mathsf{ind}_{A\times B}(C)(g)$, the result must be the same as $p(a)(b)$.

Jason Erbele (Feb 20 2021 at 05:21):

I understand what you're saying, and why that would make sense, but I am not seeing that in what's in the book.

Joshua Meyers (Feb 20 2021 at 05:22):

That's one way of looking at it. But everything is automatically curried in HoTT, so a function taking the inputs $a$, $b$, and $c$ and outputting $s(a,b,c)$ where $s$ is some expression with 3 free variables in which I'm substituting in $a$, $b$, and $c$, could be equally considered a function taking just two inputs, $a$ and $b$, and outputting a function taking the third input $c$ and outputting $s(a,b,c)$.

Joshua Meyers (Feb 20 2021 at 05:23):

In this case, you can take the last input, the ordered pair $(a,b)$ and say that this is not actually an input: rather, it is the input to the function which is the output of the whole thing.

Joshua Meyers (Feb 20 2021 at 05:25):

So then the output would be the function that takes ordered pairs $(a,b)$ and applies the curried function to them.

Joshua Meyers (Feb 20 2021 at 05:25):

And the input would be just $C$ and $g$.

Jason Erbele (Feb 20 2021 at 05:25):

I haven't even gotten to the part of the book that is about HoTT yet. This is supposed to be ordinary type theory. Up to now the book has been careful to differentiate between curried and uncurried functions, saying that they'll be conflated much later.

Joshua Meyers (Feb 20 2021 at 05:26):

Sorry I think I'm conflating ordinary type theory and HoTT. In ordinary type theory, currying is the default way to have a function of multiple variables.

Joshua Meyers (Feb 20 2021 at 05:26):

I mean, you're already thinking this way when you say that $\mathsf{ind}_{A\times B}$ has multiple inputs.

Jason Erbele (Feb 20 2021 at 05:26):

Actually, I would be surprised if it wasn't the default way in both.

Joshua Meyers (Feb 20 2021 at 05:27):

If you were speaking entirely literally, you would say it has just one input, $C$, and a big complicated output.

Joshua Meyers (Feb 20 2021 at 05:29):

But actually if you like, we can speak literally here. $\mathsf{ind}_{A\times B}(C):(\Pi_{(x:A)} \Pi_{(y:B)} C((x,y))) \rightarrow \Pi_{x:A\times B} C(x)$ is a function which takes a curried function as input and gives an uncurried one as output.

Jason Erbele (Feb 20 2021 at 05:35):

[...] we call the resulting function induction for product types: given $A,B : \mathcal{U}$ we have
$\mathsf{ind}_{A\times B} : \Pi_{C:A\times B \rightarrow \mathcal{U}} (\Pi_{(x:A)} \Pi_{(y:B)} C((x,y))) \rightarrow \Pi_{x:A\times B} C(x)$
with the defining equation
$\mathsf{ind}_{A\times B} (C,g,(a,b)) :\equiv g(a)(b)$

Okay. Let's just put that here again so I don't have to keep scrolling up and down to read and reply. My eyeballs are telling me the defining equation of induction here is taking a triple of inputs and giving a curried function (on two variables, one at a time) as the output.

Joshua Meyers (Feb 20 2021 at 05:37):

If the authors were being entirely precise they would write:

$\mathsf{ind}_{A\times B} (C)(g)(a,b) :\equiv g(a)(b)$

Joshua Meyers (Feb 20 2021 at 05:37):

But at some point they said that $f(x,y,z)$ was an acceptable abbreviation for $f(x)(y)(z)$. Which is of course confusing in this context, because it is about the distinction between currying and non-currying.

Jason Erbele (Feb 20 2021 at 05:49):

Yeah... in section 1.2 they mention avoiding the proliferation of parentheses as a reason for writing $f(a,b)$ for $f(a)(b)$, even though there are no products involved. But in the section on product types (where this induction type is so introduced),

Thus, we introduce a new rule (the elimination rule for products), which says that for any such $g$, we can define a function $f : A \times B \rightarrow C$ by
$f((a,b)) :\equiv g(a)(b)$
We avoid writing $g(a,b)$ here, in order to emphasize that $g$ is not a function on a product. (However, later on in the book we will often write $g(a,b)$ both for functions on a product and for curried functions of two variables.)

I had figured that careful distinction would have applied to $\mathsf{ind}_{A\times B}$. So that at least addresses some of my confusion. I'll try rereading this definition with the understanding that the notation is shorthand currying.

Joshua Meyers (Feb 20 2021 at 05:53):

Yeah you can also see by the type of $\mathsf{ind}_{A\times B}$ that this must be shorthand currying, so you don't just have to believe me.

Jason Erbele (Feb 20 2021 at 05:57):

Well, that is what I was getting lost in trying to check in the first place, so it was not at all clear to me a priori that it must be shorthand currying. Thanks, though.

Mike Shulman (Feb 20 2021 at 08:51):

Joshua Meyers said:

If the authors were being entirely precise they would write:

$\mathsf{ind}_{A\times B} (C)(g)(a,b) :\equiv g(a)(b)$

Or, even better, $\mathsf{ind}_{A\times B} (C)(g)((a,b)) :\equiv g(a)(b)$. You could submit an issue or a pull request to the book repository suggesting a change like this. At the moment I don't see a downside of the more precise notation here, and it could help future students in your situation!

GhaS Shee (Feb 22 2021 at 15:00):

When I started reading HoTT book, I had finished almost all "Types and Programming Languages".
And then, I did not know Martin Loef Types very much.
I did not have background of homotopy theory and ∞-category then.
I had some knowledge of Algebraic Data Type ( F-Algebra ) .

Though I did not understand what was Π and Σ,
I could start reading the HoTT book Chapter 1, regarding Π as → (Hom) and Σ as × (Product).
For me, chapter 1 is essential since we cannot construct a concrete proof in Chapter 2 without it.
It was in Chapter 2 that I realized that path-induction (introduced in 1.12) was really in practice.

Gradually, I noticed that Π was the generalization of ∀ and Σ was of ∃ in logics, Coq like proof Assistants, or System F,
and that these are fibration(the generalization of Hom Space) and cofibration(the generalization of Product Space) in Quillen's Model (very soft geometry), thanks to Cisinski's Book (Higher categories and Homotopical Algebra) and some papers, slides and notes which were openly given by @Emily Riehl, @Mike Shulman and so many.

And recently I also noticed that they seem called "fundamental theorem of topoi" .
Π is right adjunction of pullback and Σ is left adjunction.

I have a question here,
Is the category where fundamental theorem of topoi occurs opposite to the ∞-category ?
Is the category of terms in HoTT opposite to the category where the resulting adjunction from fundamental theorem of topoi occurs ? It might be a mistake, but I could not relate them well without taking opposite. (Edited)
Do they fit to Loc and Frm ?

( Edited: I remembered that the category of Open sets of X in Pos is a frame.
I began to realize I might be mixing locales and frames in a bad manner. )

Morgan Rogers (he/him) (Feb 22 2021 at 15:10):

The result often referred to as the "fundamental theorem of topos theory" is that any slice (aka over-category) of a topos is a topos, and possibly the secondary result that if $f: X \to Y$ is a morphism in a topos $\mathcal{E}$ then $(\mathcal{E}/Y) / f \simeq \mathcal{E}/X$.
As such, any such $f$ gives a geometric morphism $\mathcal{E}/X \to \mathcal{E}/Y$ whose inverse image is the pullback along $f$, and this functor has $\Pi_f$ and $\Sigma_f$ as adjoints, as you mention, but this is not the content of the fundamental theorem.

Morgan Rogers (he/him) (Feb 22 2021 at 15:11):

But I don't really understand what your question is, I'm afraid.

GhaS Shee (Feb 22 2021 at 15:12):

Thanks, I did not know the main theorem at all!

GhaS Shee (Feb 22 2021 at 19:10):

I have been confused and taken $Π_f$ as $Π_(f : \mathbb{1} → \mathbb{F} )$ . ( I mistook $f$ as an index. )
Now, I see that $f:X \to Y$ just gives a "geometric" morphism ( i.e. a solid and structure-preserving morphism like a natural projection or a rng homomorphism and its adjunction is not indexed but the fibration itself in a particular situation ) and that $Y$ is the base . ($y : Y$ is the index )

Does anyone have similar experience bothered by this notation ?
( I have remebered someone was talking about this elsewhere. )