Adjoint functor theorem in HoTT

[Ali Caglayan]

This is listed as an open problem on the HoTT wiki. I am interested in knowing what progress has been made and/or who is working on this at the moment.

What is the state of the art of the adjoint functor theorem in HoTT?

[Ali Caglayan]

Here is some more information on the problem:

Freyd's adjoint functor theorem (FAFT) is a fine thing when working classically
but at the same time a source of inconstructivity. It ensures that under
certain assumptions on a functor F : AA->BB all presheaves of the form
BB(F(-),B) or all covariant presheaves of the form BB(B,F(-)) are representable.
But for getting a right or left adjoint to F one has to CHOOSE for every B
a representing object R(B) or L(B), respectively, i.e. 
BB(F(-),B) \cong BB(-,R(B)) or BB(B,F(-)) \cong BB(L(B),_), resp.
Since BB typically will be large this requires GLOBAL CHOICE, i.e. choice
for classes. This principle is independent even from ZFC.

For example using FAFT G.Plotkin has shown that there exist free commutative
idempotent monoids in Domains, the so called Plotkin powerdomains. But to
explicitate representatives even for a restricted class of domains (SFP objects)
has required quite some additional effort and ingenuity.

In geometric topos theory it goes withut saying that a (finite limit preserving)
colimit preserving functor between Grothendieck toposes has always a right 
adjoint. The point is that the solution set condition follows from the assumption
that the involved toposes are Grothendieck and thus have small generating 
families. But for getting the right adjoints one has to use global choice. 

When working relative to a base topos SS one has to employ a fibred version
of FAFT for fibrations over SS. The fibred right adjoints will not be split
even if the original functors was split. That is one of the reasons why one 
works with fibrations and cartesian functors instead of split fibrations and
split cartesian functors. For proving fibred FAFT one hast to employ strong
choice principles on the meta-level, of course. 

It might be interesting to investigate how choice can be avoided in these
cases using the work of Ahrens, Kapulkin and Shulman on "Univalent Categories
and Rezk completion".

Thomas Streicher

[Michael Shulman]

A first note is that in type theory there is not really a notion of
"proper class" and thus not really a notion of "large category" --
almost without exception we work with a hierarchy of universes, so
that every category lives in *some* universe, e.g. the category of
sets-in-universe-i is a category in universe i+1. So in particular
the notion of "global choice" and its distinction from "local choice"
disappears.

Regarding the adjoint functor theorem, I don't know of anyone having
written down a complete proof, but one might say that the interesting
step (going from representability of each presheaf BB(F(-),B) in
Streicher's language to the existence of an actual functor right
adjoint to F) is contained in Theorem 9.5.9 and Lemma 9.5.10 in the
HoTT Book. Lemma 9.5.10 says that to give a right adjoint of F is
equivalent to giving an element of Pi(B:BB) Sigma(A:AA)
(representation of BB(F(-),B) by A). Note the untruncated Sigma --
here we are only using the "type-theoretic axiom of choice" which is
provable (i.e. the negative universal property of Sigma-types).
Theorem 9.5.9 then says that if A is a univalent category, then in
fact the type "Sigma(A:AA) (representation of BB(F(-),B) by A)" is a
propostion, and hence equivalent to the *truncated* Sigma-type "||
Sigma(A:AA) (representation of BB(F(-),B) by A) ||", i.e. "there
exists an A:AA and a representation of BB(F(-),B) by A" (the book uses
"there exists" to mean *untruncated* Sigma, but this seems to be
falling out of favor). So if we apply AFT methods to prove the
latter, we've also proven the former, and hence can deduce the
existence of an adjoint.

Mike

> --
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.