Trivial solution set for Adjoint functor theorem

[paulh123456]

Hello, i am interested in the proof in the Adjoint functor theorem in the library. The usual proof of AFT requires that the solution sets are indexed by a small sets. In the proof given in the library, no such requirement seems to exists.

Doesn't this make the entire solution set requirement moot? For example, the following compiles when appended to SolutionSet.agda.

trivial : SolutionSet′
trivial = record {
  S₀ = λ {A X} f → A ;
  S₁ = λ {A X} f → C.id {A} ;
  ϕ = λ f → f ;
  commute = λ f → D.Equiv.trans (∘-resp-≈ˡ F.identity ) D.identityˡ  
  }

Am I missing something?

[JacquesCarette]

Being a 'SolutionSet' is not, in an of itself, very interesting. It is much more interesting as a notion relative to a particular Adjoint Functor 'problem'. The above trivial solution set is, I believe, associated to the identity functor - so is indeed quite trivial.

The size issues are here dealt with via the levels. Set theory has a very crude way of measuring "size", while MLTT has a much more refined notion. If you look carefully at the proof of the AFT, you'll see that there is non-trivial "level yoga" going on (for example, exactly where Completeness is assume) that is crucial to make things work.

[paulh123456]

I believe the above trivial solution set works for any functor F.

Given f : X -> F A
Defining S1 f = C.id, ϕ  f = f
gives factorization  f = F (S1 f) ∘ ϕ f through F A

I mentioned compilation in SolutionSet.agda because it's scoped over an arbitrary functor F

Regarding the size issues. I don't entirely understand them either Set-theoretically or in Agda. I do know that the smallness condition usually prevents the use of the above trivial solution in Set-theory.

This doesn't make the AFT proof wrong of course. It's just odd to have non-small solution sets. Feel free to close.

[TOTBWF]

I am a bit suspicious of the size of completeness required; it seems like this would run afoul of https://ncatlab.org/nlab/show/complete+small+category

[tetrapharmakon]

I now realize that I haven't seen a MLTT analogue of Freyd's argument that if a locally small category is largely complete it is a poset. Can it be done, and if not constructively with the classical proof, can a different proof be found?

[TOTBWF]

See https://mathoverflow.net/questions/438333/small-complete-categories-in-hottlem/438568#438568

[JacquesCarette]

So, does this mean that the proof has a problem? Should Agda accept it? Pinging @HuStmpHrrr who did the original.

[TOTBWF]

The proof is fine, it’s just that the hypothesis are too strong to make it something you can actually use.

[HuStmpHrrr]

Is there a PR which simplifies the proof. I would like to take a look.