Open
Description
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?
Metadata
Metadata
Assignees
Labels
No labels