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: Sub-types in Dependent Type Theory

Avi Craimer (Sep 13 2020 at 05:31):

I am reading David Corfield's book Modal Homotopy Type Theory. The chapter on Dependent Types is great, helping me wrap my head around intuitive use cases for dependent types in philosophy and programming. In section 2.6, he discusses the question of whether a philosophical type theory should posit a single master type for individuals (e.g., Entity) or rather have several basic types such as (Object, Event, Agent, etc). In the course of this discussion he references the idea of building up sub-types from more basic types. However, I am a bit confused about how the construction of sub-types using dependent types is supposed to work.

I understand how to construct a proposition like "Fluffy is a Cat" from a given element Fluffy of type Animal as a truncated dependent pair type.

||Sigma( Fluffy: Animal, isCat(Fluffy) )||

But this doesn't give me Cat as a Type, nor an element c : Cat. So I am wondering if there is a way using DTT (or perhaps full blown HoTT) to actually construct the sub-type object and it's elements. Maybe another way of asking this question is that I'd like to know what is the type theoretic analogue to the category theory method of using a pullback from the sub-object classifier to define a sub-object.

In the book I've only made it to the start of Chapter 3, so it is possible that the author discusses this at a later point.

Dan Doel (Sep 13 2020 at 05:47):

It seem to me that "Fluffy is a Cat" is $\mathsf{isCat}(\mathsf{Fluffy})$ . That's referring to a specific $\mathsf{Fluffy}$ . The truncated type is more like $∃ c. \mathsf{isCat}(c)$ . I know mathematicians often interchange existential propositions and specific constructions, but I think it's arguably bad practice, and might be one of the things the book is trying to address (although I haven't read it).

Dan Doel (Sep 13 2020 at 05:49):

Also you could perhaps define the $\mathsf{Cat}$ type to be $Σ \mathsf{Animal}\ \mathsf{isCat}$ , since it is the type of animals together with a proof that they are cats. Without the truncation, you are not removing the distinction between different cats.

Dan Doel (Sep 13 2020 at 05:52):

This type is a pullback along $\mathsf{isCat} : \mathsf{Animal} → Ω$ . The first projection is the monomorphism into $\mathsf{Animal}$ .

Dan Doel (Sep 13 2020 at 05:55):

Or at least, it could be, depending on the details of how everything is arranged.

Henry Story (Sep 13 2020 at 07:08):

I asked a similar question on the HoTT Café Mailing list 4 years ago: on the mortality of Socrates. So there may be some good answers to glean from there.

Avi Craimer (Sep 13 2020 at 15:57):

Dan Doel said:

It seem to me that "Fluffy is a Cat" is $\mathsf{isCat}(\mathsf{Fluffy})$ . That's referring to a specific $\mathsf{Fluffy}$ . The truncated type is more like $∃ c. \mathsf{isCat}(c)$ .

Yes, that's right, my mistake. I guess the element of the (untruncated) sigma type would be an element of "Fluffy as Cat" (sort of like type casting in programming). The truncated sigma type is the existential proposition, "there is a Cat".

Dan Doel said:

Also you could perhaps define the $\mathsf{Cat}$ type to be $Σ \mathsf{Animal}\ \mathsf{isCat}$ , since it is the type of animals together with a proof that they are cats. Without the truncation, you are not removing the distinction between different cats.

I'm not clear what you mean by forming a sigma type with Animal as the first element of the pair. That would be saying something like, "The abstract category of animals is a Cat" which is plainly false. Animal : Type is not an animal much less a cat. Maybe I'm misunderstanding your suggestion.

Dan Doel said:

This type is a pullback along $\mathsf{isCat} : \mathsf{Animal} → Ω$ . The first projection is the monomorphism into $\mathsf{Animal}$ .

Right, this is how it would work in Topos theory. What I don't understand is what is the analogue to this in DTT or HoTT.

Avi Craimer (Sep 13 2020 at 16:31):

Henry Story said:

I asked a similar question on the HoTT Café Mailing list 4 years ago: on the mortality of Socrates. So there may be some good answers to glean from there.

Thanks for linking to that discussion. Very interesting although I didn't quite feel it answered the question. I'm left wondering if there is a disconnect between the type systems that make sense for mathematics and those that might make sense for philosophy and common-sense ontologies.

Dan Doel (Sep 13 2020 at 16:45):

Sorry. By $Σ A B$ I mean $Σ_{x:A} B(x)$ . This is sometimes how it might be written when there is sufficient machinery for $Σ$ to not have to act as a variable binder itself.

Dan Doel (Sep 13 2020 at 16:46):

Anyhow, what I wrote was all intended to be in type theory, not topos theory.

Dan Doel (Sep 13 2020 at 16:52):

I don't know exactly how the type theory is structured in the book you're reading, but it would go something like this...

Dan Doel (Sep 13 2020 at 17:02):

There is a type $Ω$ whose values are propositional types. This allows you to have $\mathsf{isCat} : \mathsf{Animal} → Ω$ act in a sort of double way. It's an arrow into the subobject classifier, but it's also a family of types. This happens a lot if you decide to make the type theory have types whose values are other types. $\mathsf{isCat}$ is both a map into the subobject classifier and a family of types, while in topos theory there is just a correspondence between these two things.

Dan Doel (Sep 13 2020 at 17:17):

Since $\mathsf{isCat}$ is a family of types indexed by $\mathsf{Animal}$ , we can form the sigma type $Σ_{a:\mathsf{Animal}} \mathsf{isCat}(a)$ . There are generally multiple ways to think about this. If you think about the family $B$ as primary, it's the disjoint union of all the fibers, or the sort of 'total space' of the family. In category theory you usually think of the family as already being the total space with a display map into the indexing type, but type theory prefers to present the family like it's mapping from the indexing type.

But, since the fibers of $\mathsf{isCat}$ are propositional, this can also be read like it's a subset of $\mathsf{Animal}$ , $\{c \in \mathsf{Animal} | \mathsf{isCat}(c) \}$ . The values of the sigma type are animals together with proofs that they are cats, but there is 'at most one' such proof (homotopically if you're doing that) for each animal. So the values of the sigma type are more structured than the elements of a subset are usually thought to be, but the structure is in some sense just acting as a filter.

Dan Doel (Sep 13 2020 at 18:02):

If you want to get really into the weeds, then there is an alternate way of presenting this. You have a type $Ω$ of propositions, and a family

$p : Ω ⊢ \mathsf{True}(p)\ \mathsf{type}$

of truth values. Pullback corresponds to substitution, so if you have

$a : \mathsf{Animal} ⊢ \mathsf{isCat}(a) : Ω$

then the substitution

$a : \mathsf{Animal} ⊢ \mathsf{True}(\mathsf{isCat}(a))\ \mathsf{type}$

is the family you get by pulling back the truth family along the arrow $\mathsf{isCat} : \mathsf{Animal} → Ω$ .

Dan Doel (Sep 13 2020 at 18:03):

Then you can use Σ to realize the total space of the family as a type in itself, rather than a family of types.

Dan Doel (Sep 13 2020 at 18:06):

This doesn't blur the lines of what you do in the category theory as much.

Avi Craimer (Sep 13 2020 at 18:07):

Thanks, I think I'm starting to understand better. One question about the sigma type.

Dan Doel said:

The values of the sigma type are animals together with proofs that they are cats...

So when you write, $Σ_{a:\mathsf{Animal}} \mathsf{isCat}(a)$ you mean for the a to range over all the terms in Animal. Is that what a sigma type is? I though you needed to give specific term to form a particular dependent pair type. i.e., I that the a:Animal was a concrete term (like Fluffy) rather than a term variable.

Dan Doel (Sep 13 2020 at 18:15):

Values of $Σ_{a:A} B(a)$ are pairs $(M,N)$ where $M : A$ and $N : B(M)$ .

This is very much like the existential quantifier. ∃ binds a variable in $∃ x:A. B(x)$ , and the variable ranges over $A$ . But to prove an existential statement, you give a particular value of $A$ and a proof that $B$ holds for that value. But for $∃$ we want to consider all proofs equivalent, which is what truncation does. If you don't truncate, there are potentially many distinct choices of $M : A$ .

Dan Doel (Sep 13 2020 at 18:19):

Also, you should be careful about saying the variable ranges over "terms". Those are syntactic expressions that denote something in the semantics. But the semantic values may not be the syntactic expressions.

Dan Doel (Sep 13 2020 at 18:23):

See e.g. here.

Avi Craimer (Sep 13 2020 at 18:26):

Dan Doel said:

Values of $Σ_{a:A} B(a)$ are pairs $(M,N)$ where $M : A$ and $N : B(M)$ .

Ok, so just to be sure I understand, as a simple example, if I have a type Bool with values true and false. Then the dependent sum type $Σ_{x:Bool} (B(x) : Prop)$ would have two possible values namely the pairs p1 = (true, warrant of B(true)) and p2 = (false, warrant of B(false) ). These would only be values of the sigma type insofar as B(true) and B(false) are true propositions.

Is this correct?

Dan Doel (Sep 13 2020 at 18:40):

Yes, that's correct.

Avi Craimer (Sep 13 2020 at 18:43):

Ok. So that was the root of my misunderstanding. Now I can see how the sigma type provides a sub-type. Thank you so much for your help. I'll go back through your explanations of the weedy parts to try to really map it out, but I think I get the basics now.

Dan Doel (Sep 13 2020 at 18:43):

Cool.

Henry Story (Sep 14 2020 at 09:37):

I think there is another way where Sigma types act as subtypes. I was looking at these in detail a year ago and wrote it up in a post Modal HoTT on the Web. I tried to illustrate carefully how Sigma Types arise out of an adjunction on slice categories.
So a $\sum_{x: A} D(x)$ is the result of mapping the object $g: D \to A$ in the slice category $\mathcal{C}/A$ to $\mathcal{C}$ using the left adjoint of $f*:=A \times (-)$ . The $D(x)$ is the type of the fiber over $x$ , thus a part of $D$ . On this view it looks like $D(x)$ really selects a subset of $D$ (thinking set theoretically), which would in a way be equivalent to a subclass of $D$ . It actually partitions the space, where subclasses in OO can be multi-layered. Somehow this does not appear that clearly in the HoTT definition of a sigma time. So I am not quite sure. Sigma Types as Adjunctions, explained in Modal HoTT on the Web blog post

Henry Story (Sep 14 2020 at 09:39):

Somehow I also came to the conclusion that a sigma type is a pullback (shown in the illustration above). But I am not sure anymore where I got that from.

Henry Story (Sep 14 2020 at 10:56):

Actually, reading @Dan Doel 's example with animals and cats I think I got something wrong in my illustration (it was something that bothered me when I put the post together). I'll draw up an illustration for the Cat example above.

Henry Story (Sep 14 2020 at 11:34):

Here is my illustration of the isCat dependent sum as an adjunction on the base change functor for $f: \Omega \to 1$ .

Is this correct? I like the way the function is central. But I think the objects in the slice category $\mathcal{C}_{/\Omega}$ are called $\Omega$ -dependent, yet I thought one says that $\Sigma_{x: \text{Animal}} isCat(x)$ this type is animal dependent. :thinking:

DependentSum.Cat.jpg

Henry Story (Sep 14 2020 at 16:27):

Looking at the nlab page on dependent sum especially the section "relation to Type Theory" it seems indeed that the dependent sum arising from $x: A \dashv P(x)$ corresponded to the slice category over A.
(In a way it also corresponds better to the fibered view, where the fibers are over A).

So what I don't quite understand is

HoTT writes $A: \mathcal{U}$ and $P: A \to \mathcal{U}$ . But the morphisms in the slice category go from $P \to A$ . Admittedly P is known as a Type-family
that nlab defines the left adjoint functor as
$\sum_f \coloneqq f\circ (-) \colon \mathcal{C}_{/A} \to \mathcal{C}_{/I}$ . When $I$ is the final object of the category $1$ , then this equals simply $f$ which in the case above would have been just $f: B \to A$ , or in my last diagram $f: \text{Animals} \to \Omega$ . But why is it that the sum pairs have $A$ ( $\Omega$ ) first and $B$ ( $\text{Animals}$ ) second?

Henry Story (Sep 14 2020 at 20:00):

Also if I don't slice $\mathcal{C}$ over $\Omega$ but instead did it over $\text{Animals}$ as it seems I should according to nlab for @Dan Doel's $\Sigma_{x:\text{Animals}} isCat(x)$ example, we would have objects $\Omega \to \text{Animals}$ in the slice category. But that does not makes a lot less sense: would every such morphism select only one cat and one non-cat?

Dan Doel (Sep 14 2020 at 22:24):

The point of (sub)object classifiers is that there are correspondences between (certain) $P → A$ and $A → \mathcal U$ or $A → Ω$ . The 'in the weeds' presentation I talked about makes the fact that this is a correspondence more explicit, but other times they are presented as just being the same thing.

So, you could hypothesize a family

$a : \mathsf{Animal} ⊢ \mathsf{isCat}(a)\ \mathsf{prop}$

Meaning essentially that there is a monomorphism $\mathsf{isCat} : \mathsf{Cat} \rightarrowtail \mathsf{Animal}$ , which is also an object of the slice category over $\mathsf{Animal}$ . The obvious issue is that I have already invoked a type $\mathsf{Cat}$ because I don't know what else to call that part of the subobject.

$Ω$ being a subobject classifier means that there exists $\widetilde{\mathsf{isCat}} : \mathsf{Animal} → Ω$ , which forms part of a pullback square with $\mathsf{isCat} : \mathsf{Cat} \rightarrowtail \mathsf{Animal}$ . The other parts of the square are $\mathsf{true} : 1 \rightarrowtail Ω$ and $! : \mathsf{Cat} → 1$ . $\widetilde{\mathsf{isCat}}$ maps animals to the truth value that corresponds to their cat-hood.

In the more explicit notation I gave, the expectation is something like:

$a : \mathsf{Animal} ⊢ \mathsf{isCat}(a) = \mathsf{True}(\widetilde{\mathsf{isCat}}(a))$

which says that by pulling back 'truth' along $\widetilde{\mathsf{isCat}}$ , we get a subobject equivalent to $\mathsf{Cat}$ , and with the same indexing by $\mathsf{Animal}$ . If you want to recover the 'whole space' as a type, rather than an indexed family of types, then you can use the sigma type to get something indexed by $1$ instead of $\mathsf{Animal}$ . That would be a type equivalent to $\mathsf{Cat}$ .

You could also instead hypothesize $\mathsf{isCat} : \mathsf{Animal} → Ω$ , which doesn't demand you to also invent $\mathsf{Cat}$ directly, and instead allows you to define it. A lot of type theories arguably work this way, where everything is defined in terms of object classifiers (universes) whose values are implicitly usable as their corresponding types.

Dan Doel (Sep 14 2020 at 22:29):

I guess the point is that you aren't usually considering various families sliced over $Ω$ . You are reindexing from $\mathsf{true} : 1 \rightarrowtail Ω$ in the slice over $Ω$ along the classifying map $A → Ω$ .