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: Synthetic quasi-coherence in Cartesian cubical objects

Madeleine Birchfield (Jun 25 2025 at 11:15):

Gratzer, Weinberger, and Buchholtz say in Directed univalence in simplicial homotopy type theory that synthetic quasi-coherence for distributive lattices holds internally in Dedekind cubical objects, which are presheaves on the Lawvere theory of distributive lattices.

Does a similar synthetic quasi-coherence for sets with two elements holds internally in Cartesian cubical objects, which are presheaves on the Lawvere theory of sets with two elements?

daniel gratzer (Jun 25 2025 at 12:59):

I guess turning the crank on Bleschmidt's general result (which applies to all algebraic theories and, in fact, to Horn theories), one concludes that inside this topos, if we have a finitely-presented $\mathbb{I}$ algebra (where now an "algebra" is just an object with 0,1) then we get the duality-type isomorphism. Might be a bit boring though, since finitely-presented algebras are now $\mathbb{I}$ with finitely many points adjoined and subject to a finite number of equations.

Madeleine Birchfield (Jun 25 2025 at 17:38):

Is $\mathbb{I}$ equipped with its hom-sets $\mathrm{hom}_\mathbb{I}(i, j) \coloneqq \sum_{f:\mathbb{I} \to \mathbb{I}} (f(0) = i) \times (f(1) = j)$ still a poset in this presheaf topos from synthetic quasi-coherence?

Madeleine Birchfield (Jun 25 2025 at 18:34):

We have by synthetic quasi-coherence that the function type $\mathbb{I} \to \mathbb{I}$ is equivalent to the free $\mathbb{I}$-algebra $\mathbb{I}[x] \simeq \mathbb{I} + 1$ on one generator, with equivalence $\mathrm{eval}:\mathbb{I}[x] \simeq (\mathbb{I} \to \mathbb{I})$ such that $\mathrm{eval}(k) = \lambda i.k$ for the constants $k$ in $\mathbb{I} \subseteq \mathbb{I}[x]$ and $\mathrm{eval}(x) = \lambda i.i$ for the generator $x$.

Madeleine Birchfield (Jun 25 2025 at 18:41):

This implies that the only hom-sets that have elements are the reflexive hom-sets

$$(\lambda i.k, \mathrm{refl}_\mathbb{I}(k), \mathrm{refl}_\mathbb{I}(k)):\mathrm{hom}_\mathbb{I}(k, k)$$

and the hom-set from $0$ to $1$

$$(\mathrm{id}_\mathbb{I}, \mathrm{refl}_\mathbb{I}(0), \mathrm{refl}_\mathbb{I}(1)):\mathrm{hom}_\mathbb{I}(0, 1)$$

and furthermore, by the equivalence $(\mathbb{I} \to \mathbb{I}) \simeq \mathbb{I} + 1$, these are the only such elements of the hom-sets.

Madeleine Birchfield (Jun 25 2025 at 18:45):

From, this, one can show that, $\mathrm{hom}_\mathbb{I}(i, j)$ is a subsingleton for each $i$ and $j$ in $\mathbb{I}$ and reflexive, transitive, and antisymmetric, making $\mathbb{I}$ into a poset. We can define the partial order as $i \leq j \coloneqq \mathrm{hom}_\mathbb{I}(i, j)$.

Madeleine Birchfield (Jun 25 2025 at 23:21):

Now, defining the 2-simplex $\Delta^2 \coloneqq \sum_{i, j:\mathbb{I}} \mathrm{hom}_\mathbb{I}(i, j)$ as the fibred hom-set of the interval, do we have $\Delta^2 \simeq \mathbb{I} \to \mathbb{I}$? Yes, because both are equivalent to $\mathbb{I}[x] \simeq \mathbb{I} + 1$. For $\Delta^2$, we have for all $k$ in $\mathbb{I} \subseteq \mathbb{I}[x]$ the elements

$$(k, k, \lambda i.k, \mathrm{refl}_\mathbb{I}(k), \mathrm{refl}_\mathbb{I}(k)):\Delta^2$$

and for the generator $x$ in $1 \subseteq \mathbb{I}[x]$ we have

$$(0, 1, \lambda i.i, \mathrm{refl}_\mathbb{I}(0), \mathrm{refl}_\mathbb{I}(1)):\Delta^2$$

As a result, by synthetic quasi-coherence, we have, for all functions $f:\mathbb{I} \to \mathbb{I}$, an element

$$(f(0), f(1), f, \mathrm{refl}_\mathbb{I}(f(0)), \mathrm{refl}_\mathbb{I}(f(1))):\Delta^2$$

The quasi-inverse function is given by the third projection function of $\Delta^2$ as a record type, and since both $\Delta^2$ and $\mathbb{I}[x]$ are sets, quasi-invertibility is sufficient to establish this as an equivalence. Since $\mathrm{hom}_\mathbb{I}(i, j)$ is a subsingleton for all $i$ and $j$, evaluation of functions at $0$ and $1$, $(\mathbb{I} \to \mathbb{I}) \to (\mathbb{I} \times \mathbb{I})$ is an embedding, given by composing the equivalence $(\mathbb{I} \to \mathbb{I}) \simeq \Delta^2$ with the projection function $\Delta^2 \to (\mathbb{I} \times \mathbb{I})$.

Madeleine Birchfield (Jun 26 2025 at 11:47):

We also have that $\Delta^2$ is equivalent to the set of monotonic functions from the booleans $\mathbb{2} \to \mathbb{I}$ by recursion on the booleans.

$\Delta^2 \simeq \sum_{f:\mathbb{2} \to \mathbb{I}} \mathrm{hom}_\mathbb{I}(f(0), f(1))$

Madeleine Birchfield (Jun 26 2025 at 12:03):

By induction on the natural numbers one can show that $n$-ary operations on $\mathbb{I}$ are equivalent to monotonic $n$-ary functions from the booleans to $\mathbb{I}$.