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: Dependent Type Families in Topos Type Theory

Avi Craimer (Feb 16 2021 at 01:17):

I am working through the formal type rules for Topos Type Theory in @Maietti Maria Emilia , The Type Theory of Categorical Universes. I haven't found any rules in the system for introducing the dependent type family (although many rules presuppose that we have such a family). It's possible I've just missed this somewhere in the text. For example, on page 41 in the Indexed Sum Formation rule you require a type C(x) that depends on the variable x:B in the context. However, I'm failing to understand how C(x) could be constructed to be other than a constant function, since we can't express it as a lambda term of type B -> Type. Any help would be most welcome. Screen-Shot-2021-02-15-at-8.10.56-PM.png

Nathanael Arkor (Feb 16 2021 at 01:26):

$C(x)$ here stands for a metavariable parameterised by a single variable $x : B$. It's not part of the syntax itself: you can replace $C$ with any type containing a free variable $x : B$.

Avi Craimer (Feb 16 2021 at 02:19):

Thank you that helps somewhat. But I'm still unclear how the type itself can contain a free variable x:B.

Which type formation rule allows us to introduce arbitrary free variables into a type expression?

Dylan Braithwaite (Feb 16 2021 at 02:38):

The rule for introducing the equality type (combined with the var rule) does this

Mike Shulman (Feb 16 2021 at 04:54):

Another rule that leads to types dependent on variables is that for elements of a universe, $x:U \vdash \mathsf{el}(x) \; \mathsf{type}$. I don't have the paper you refer to so I don't know if it has this rule.

Matteo Capucci (he/him) (Feb 16 2021 at 08:46):

Avi Craimer said:

Thank you that helps somewhat. But I'm still unclear how the type itself can contain a free variable x:B.

Which type formation rule allows us to introduce arbitrary free variables into a type expression?

I don't have the paper at hand, but I've been taught TT by Milly so I assume it's the same ruleset. I remember that she puts a lot of emphasis on contexts, so that all introduction rules for types are under a context $\Gamma$.
Hence to introduce a type over $B$ you first build a context $- [ x \in B]$ and then you introduce the type you need under that context.

Avi Craimer (Feb 16 2021 at 15:03):

The paper I'm working from is:

tesi.pdf
It is available publicly in source code here (https://www.math.unipd.it/~maietti/papers/Maietti.ps.gz)

Dylan, thanks, I will have to think about how to apply equality rules to make types with free variables.

Matteo, thank you I understand how to build up contexts.

Mike, thank you. Do universes exist as types in the T-top theory (T-top is what the author calls the topos type theory in another paper), I thought this theory didn't have an explicit type universe?

An example would help. Suppose I wanted to use T-top to represent a pullback type. I guess I'd start by defining functions f :A->X and g:B->X. Then add variables of a:A and b:B to the context. Then introduce an equality type f(a) = g(b) : X. After that I'm a bit stuck.

Dylan Braithwaite (Feb 16 2021 at 15:29):

Avi Craimer said:

Dylan, thanks, I will have to think about how to apply equality rules to make types with free variables.

To clarify, I wasn't referring to the judgemental equality rules, but rather the type introduced by the "F-Eq" rule in that paper. This is an actual type, depending on two values (which can be free variables), which logically corresponds to the proposition of equality of the two terms on which it depends.

Avi Craimer (Feb 16 2021 at 15:50):

Thanks Dylan for the clarification. So can you introduce an equality type Eq(X, f(a), g(b)) [a:A,b:B] ?

Dylan Braithwaite (Feb 16 2021 at 16:07):

Yeah exactly. As long as you can derive $f(a) \in X [a \in A, b \in B]$ and $g(b) \in X [a \in A, b \in B]$

Avi Craimer (Feb 16 2021 at 16:13):

So then Eq(X, f(a), g(b)) [a:A, b:B, f:A->X, g:B->X] would be the general form of a pullback set for A, B, and X?

Dylan Braithwaite (Feb 16 2021 at 16:35):

I haven't looked at how the paper sets up the semantics for this language, but I think typically you want to abstract over the a and b with sigma types to get the pullback

Dylan Braithwaite (Feb 16 2021 at 16:37):

Yep, see proposition 4.4.3

Avi Craimer (Feb 16 2021 at 16:48):

Ah yes! Thank you that's great.