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: natural model

Frank Tsai (Jul 27 2023 at 17:37):

Could someone explain the third equation? I understand the first two equations (they hold by definition), but I don't understand why you can push the substitution $p_{A}$ out of tilde.
It's Steve Awodey's natural model: https://arxiv.org/pdf/1406.3219.pdf (page 16)
image.png

Kevin Arlin (Jul 27 2023 at 18:10):

It'd be ideal to aim at StackExchange conventions of having your question be self-contained.

Frank Tsai (Jul 27 2023 at 18:52):

We want to show that a natural model $p : \widetilde{\mathcal{U}} \to \mathcal{U}$ equipped with two operations $\Pi$ and $\lambda$ satisfies the $\eta$-rule for $\Pi$-types.
image.png

$p_{A}$ and $q_{A}$ are defined as the legs of the pullback.
image.png

The first two equations hold by definition. Can someone explain why the substitution $p_{A}$ can be pulled out of the tilde in the third equation?
image.png

John Baez (Jul 28 2023 at 08:15):

Maybe @Steve Awodey can answer this.

Josselin Poiret (Jul 28 2023 at 08:55):

$p_A$ can be pulled out because of the unicity of the arrow in the definition of a pullback! $\tilde{fp_A}$ is built out of a pullback where both arms factor through $p_A$, so by unicity you get a factorization $\tilde{f}p_A$

Josselin Poiret (Jul 28 2023 at 09:10):

There's a change of POV you can make with natural models that give you equivalent definitions but much nicer reasoning imo, is instead of saying that there exists an operation $\lambda$ that makes the square into a pullback, you can ask for an operation $\lambda : \Sigma (A : U) \tilde{U}^A → T$ over $\Sigma (A : U) U^A$, where $T$ is the pullback of $Π$ and $p$, along with $app : T → \Sigma (A : U) \tilde{U}^A$. Then, asking for an equation $app \circ \lambda = id$ gives $Π$ types with only β, and if you also ask for $\lambda \circ app = id$ you get η as well. I found this approach clarifies most of the reasoning here.

Josselin Poiret (Jul 28 2023 at 09:19):

also, if you have already "bootstrapped" an interpretation of dependent type theory in presheaf categories, then this is all equivalent to
$\vdash Ty\text{ type}$
$A : Ty \vdash Tm A\text{ type}$ (natural model).
$A : Ty, B : Tm A → Ty \vdash \mathrm{pi} A B : Ty$ (type constructor)
$A : Ty, B : Tm A → Ty, f : (a : Tm A) → Tm (B a) \vdash abs f : Tm (\mathrm{pi} A B)$ (term constructor)
$A : Ty, B : Tm A → Ty, f : Tm (\mathrm{pi} A B) \vdash unabs : (a : Tm A) → Tm (B a)$ (term "reifier", it's not really an eliminator)
$A : Ty, B : Tm A → Ty, f : (a : Tm A) → Tm (B a) \vdash unabs (abs f) = f$ (β)
$A : Ty, B : Tm A → Ty, f : Tm (\mathrm{pi} A B) \vdash abs (unabs f) = f$ (η)

This was very illuminating to me! It's the basic idea behind 2LTT and variations!

Frank Tsai (Jul 28 2023 at 17:32):

Thanks. I'll try to figure out the details :+1: