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: theory: type theory & logic

Topic: equalizers

CB Wells (Apr 23 2021 at 05:25):

I'm wondering how to formalize equalizers in a category with finite limits, in the simplest way possible. Mike led me to think that it is given by the subobject fibration having fibered equality, but I can't find what that actually looks like in inference rules.

CB Wells (Apr 23 2021 at 05:27):

writing it naively by the universal property:
formation $(\Gamma\vdash f,g:S) | (\Gamma\vdash eq(f,g):Prop)$

CB Wells (Apr 23 2021 at 05:27):

introduction $(\Delta \vdash t:\Gamma),(\Delta\vdash f(t)=g(t):S) | (\Delta \vdash e_t:eq(f,g))$

CB Wells (Apr 23 2021 at 05:27):

but for whatever reason I'm sure that introduction isn't right.

CB Wells (Apr 23 2021 at 05:28):

I want to know how to work out these rules for limits and colimits in the simplest systematic way.

Nathanael Arkor (Apr 23 2021 at 11:01):

Having finite limits corresponds to having dependent sums and extensional identity types, so you can restrict the usual rules for MLTT to those ones.

FH (Apr 23 2021 at 11:04):

I think you may want to take a look at Kock's paper on this

FH (Apr 23 2021 at 11:05):

Type theoretically you're probably better off working with dependent types and substitution (i.e. pullbacks) rather than a non-dependent language with equaliser types since that could probably get quite fiddly (having to verify domains and codomains, etc..).

FH (Apr 23 2021 at 11:06):

Pullbacks also give you products (via the dependent sum over the constant family) so you wont need separate rules for those.

Mike Shulman (Apr 23 2021 at 13:07):

The usual J-eliminator for identity types corresponds categorically to "Lawvere equality for a hyperdoctrine". I don't have time to write more now, but you could try that as keywords...

Mike Shulman (Apr 23 2021 at 15:23):

Any presentation of finite-limit logic, such as in Sketches of an Elephant, should give rules for an equality proposition.

Mike Shulman (Apr 23 2021 at 15:24):

For the benefit of others present, based on the other thread I think Christian really does want a logic over a non-dependent type theory here, because he also wants to add function-types to the underlying type theory in order to model a CCC with finite limits that is not LCCC.

Mike Shulman (Apr 23 2021 at 15:24):

Jacobs also has rules for an equality proposition.

Mike Shulman (Apr 23 2021 at 15:26):

Without dependent types, you can't use an equality proposition to construct an equalizer type. But the subobject fibration having equality propositions still corresponds to the category having finite limits.

Mike Shulman (Apr 23 2021 at 15:26):

The Lawvere reference is https://ncatlab.org/nlab/show/Equality+in+hyperdoctrines+and+comprehension+schema+as+an+adjoint+functor

FH (Apr 23 2021 at 15:37):

There's partial horn logic (I think by Palmgren & Vickers) which models also corresponds to finite limit categories and is simpler than Johnstone's presentation of Cartesian logic (since it avoids having to put a well-ordering on the partial operations).

CB Wells (Apr 23 2021 at 17:11):

thanks for all the help. I do want to stick with just CCCs+equalizers without getting fancier, partly for popular accessibility.

CB Wells (Apr 23 2021 at 17:13):

I'm wondering if I can just combine the syntax of generalized algebraic theories with that of STLC

CB Wells (Apr 23 2021 at 17:14):

I feel like that might be simplest on the reader.

CB Wells (Apr 23 2021 at 17:14):

I believe the GAT syntax has the Eq predicate built-in...

Nathanael Arkor (Apr 23 2021 at 17:15):

Christian Williams said:

I believe the GAT syntax has the Eq predicate built-in...

It does not. It has to be declared as an additional family of type constructors.

CB Wells (Apr 23 2021 at 17:15):

hm, okay

CB Wells (Apr 23 2021 at 17:16):

why is that?

Nathanael Arkor (Apr 23 2021 at 17:19):

Because the syntax of GATs does not allow equations to appear in the premiss of a rule, unlike in an essentially algebraic theory. So you have to add a type constructor for Eq, and equality reflection, to capture it.

Nathanael Arkor (Apr 23 2021 at 17:19):

Cartmell mentions this in one of the chapters of his paper.

CB Wells (Apr 23 2021 at 17:29):

yes, I see it in section 4

CB Wells (Apr 23 2021 at 17:30):

not sure what you mean by reflection though.

Nathanael Arkor (Apr 23 2021 at 17:35):

Equality reflection means having a rule:
$\frac{\Gamma \vdash e : \mathrm{Eq}_A(s, t)}{\Gamma \vdash s = t : A}$
so that the formal equality coincides with external equality.

CB Wells (Apr 23 2021 at 17:38):

also, I guess it's possible that just the default syntax of GATs, using pullbacks, is enough for what I need. I was just thinking "oh from a CCC I'm adding equalizers", but there's already a syntax for pullbacks and it's easy to add function types to that, like Fawzi was saying in the other thread. I guess I'm just surprised I haven't seen this combination before (though of course it's contained in higher-powered languages)

Nathanael Arkor (Apr 23 2021 at 17:44):

Note that you don't have all pullbacks in a GAT, only pullbacks of display maps.

FH (Apr 23 2021 at 18:57):

So what is the semantics of GAT? Because it's a little hard to pin down in the literature

Nathanael Arkor (Apr 23 2021 at 18:59):

A contextual category.

Mike Shulman (Apr 23 2021 at 19:10):

Remember that if there are dependent types and you have a function-type former $\to$ that can be applied in any context (as is usual for any type former in a dependent type theory), then the semantics becomes at least very close to locally cartesian closed even if you don't assert the usual sort of $\Pi$-types. I suppose you could put some restriction on the function-types to only be applicable to types defined in the empty context, but I think a logic over a simple type theory is really a better way to go.

Nathanael Arkor (Apr 23 2021 at 19:20):

@Mike Shulman: to clarify, are you saying that STLC + identity types must be modelled by something stronger than a finitely complete category with exponentials, or that finitely complete categories with exponentials are already very close to being fully locally cartesian closed?

Mike Shulman (Apr 23 2021 at 19:34):

If by "STLC + identity types" you mean a dependent type theory with "non-dependent function types" in arbitrary contexts:

$$\frac{\Gamma \vdash A \;\mathsf{type} \quad \Gamma \vdash B\; \mathsf{type}}{\Gamma \vdash A\to B \; \mathsf{type}}$$

then yes, this requires more than a finitely complete cartesian closed category. If you try to model it in the naive way where all morphisms are display maps, then it requires a locally cartesian closed category, because the above rule demans that each slice category is cartesian closed, which is an equivalent formulation of LCCC. If you have fewer display maps you may be able to get away with less, but you can't just use the simple fibration if you want to have identity types too.

Nathanael Arkor (Apr 23 2021 at 19:39):

Hmm. Is some kind of compatibility condition between exponentials and pullbacks the sort of thing you have in mind?

Mike Shulman (Apr 23 2021 at 19:40):

Not really, just the fact that all slice categories have exponentials.

Mike Shulman (Apr 23 2021 at 19:40):

Their compatibility with pullbacks is automatic.

Nathanael Arkor (Apr 23 2021 at 19:43):

I mean to identify the class of categories modelling (the dependent type theory) STLC + identity types.

Mike Shulman (Apr 23 2021 at 19:44):

I really object to calling it "simply typed lambda calculus with identity types" when it is dependently typed, not simply typed.

Nathanael Arkor (Apr 23 2021 at 19:45):

Ah, sorry :sweat_smile: "Lambda-calculus with identity types", then.

Mike Shulman (Apr 23 2021 at 19:45):

For a category $C$ with pullbacks, its codomain fibration models dependent type theory with identity types and non-dependent function types if and only if $C$ is locally cartesian closed.

Mike Shulman (Apr 23 2021 at 19:46):

There isn't going to be as simple a description of the class of general display-map categories that model this type theory, but there isn't any clear way to construct such a thing from a finitely complete cartesian closed category.

Evan Patterson (Apr 24 2021 at 02:20):

Lambek and Scott (Sec 0.5) gave an equational presentation of equalizers, which I transcribed into Catlab here. I don't find it particularly transparent, but it does have the virtue of being generalized algebraic/essentially algebraic.

A lot of this discussion is about equality/identity types, so I may be answering the wrong question.

Eduardo Ochs (Apr 25 2021 at 02:56):

I had to decypher section 0.5 of Lambek and Scott's book some months ago, too... here's a diagram that I drew to help it fit in my tiny brain. Hope it helps. sshot.png