|
| 1 | +<!-- |
| 2 | +```agda |
| 3 | +open import Cat.Prelude |
| 4 | +open import Cat.Functor.Base |
| 5 | +open import Cat.Functor.Compose |
| 6 | +open import Cat.Functor.Naturality |
| 7 | +open import Cat.Instances.Functor |
| 8 | +open import Cat.Functor.Adjoint |
| 9 | +open import Cat.Diagram.Limit.Base |
| 10 | +open import Cat.Diagram.Colimit.Base |
| 11 | +open import Cat.Diagram.Duals |
| 12 | +open import Cat.Functor.Adjoint.AFT |
| 13 | +open import Cat.Functor.Adjoint.Continuous |
| 14 | +open import Cat.Functor.Adjoint.Reflective |
| 15 | +``` |
| 16 | +--> |
| 17 | + |
| 18 | +```agda |
| 19 | +module Cat.Total {o ℓ} (C : Precategory o ℓ) where |
| 20 | +open import Cat.Functor.Hom C |
| 21 | +open import Cat.Instances.Presheaf.Colimits |
| 22 | +``` |
| 23 | +<!-- |
| 24 | +```agda |
| 25 | +private |
| 26 | + open module C = Precategory C |
| 27 | + variable |
| 28 | + o' ℓ' : Level |
| 29 | +``` |
| 30 | +--> |
| 31 | + |
| 32 | +# Total precategories {defines="total-precategory"} |
| 33 | + |
| 34 | +A precategory is **total** if its yoneda embedding has a left adjoint. |
| 35 | + |
| 36 | +```agda |
| 37 | +record is-total : Type (o ⊔ lsuc ℓ) where |
| 38 | + field |
| 39 | + {れ} : Functor Cat[ C ^op , Sets ℓ ] C |
| 40 | + has-よ-adj : れ ⊣ よ |
| 41 | +``` |
| 42 | +<!-- |
| 43 | +```agda |
| 44 | +module _ (C-total : is-total) where |
| 45 | + open module C-total = is-total C-total |
| 46 | +``` |
| 47 | +--> |
| 48 | + |
| 49 | +## Cocompleteness |
| 50 | + |
| 51 | +All total categories are [[cocomplete]]. |
| 52 | + |
| 53 | +```agda |
| 54 | + total→cocomplete : is-cocomplete ℓ ℓ C |
| 55 | + total→cocomplete F = natural-iso→colimit ni $ left-adjoint-colimit has-よ-adj $ Psh-cocomplete ℓ C (よ F∘ F) |
| 56 | + where ni : れ F∘ よ F∘ F ≅ⁿ F |
| 57 | + ni = ni-assoc ∙ni |
| 58 | + (is-reflective→counit-iso has-よ-adj よ-is-fully-faithful ◂ni F) ∙ni |
| 59 | + path→iso F∘-idl |
| 60 | +``` |
| 61 | + |
| 62 | +## The adjoint functor property |
| 63 | + |
| 64 | +Total precategories satisfy a particularly nice [[adjoint functor theorem]]. In |
| 65 | +particular, every [[continuous functor]] $F$ has a [[left adjoint]]. |
| 66 | + |
| 67 | + |
| 68 | + |
| 69 | +```agda |
| 70 | + cocontinuous→right-adjoint : ∀ {D : Precategory ℓ ℓ} |
| 71 | + (F : Functor C D) → is-cocontinuous ℓ ℓ F → Σ[ G ∈ Functor D C ] F ⊣ G |
| 72 | + cocontinuous→right-adjoint {D = D} F F-is-cocont = G , opposite-adjunction Gᵒᵖ⊣Fᵒᵖ |
| 73 | + where module F = Functor F |
| 74 | + module D = Precategory D |
| 75 | + open import Cat.Functor.Hom D using () renaming (Hom-into to Hom-intoᴰ; よ to よᴰ ) |
| 76 | +
|
| 77 | + my-silly-presheaf : D.Ob → ⌞ PSh ℓ C ⌟ |
| 78 | + my-silly-presheaf y = Hom-intoᴰ y F∘ F.op |
| 79 | +
|
| 80 | + my-silly-functor : Functor D C |
| 81 | + my-silly-functor = れ F∘ precompose F.op F∘ よᴰ |
| 82 | + module my-silly-functor = Functor my-silly-functor |
| 83 | +
|
| 84 | + op-adj : Σ[ G ∈ Functor (D ^op) (C ^op) ] G ⊣ F.op |
| 85 | + op-adj = solution-set→left-adjoint F.op (is-cocomplete→co-is-complete total→cocomplete) (is-cocontinuous→co-is-continuous F-is-cocont) λ y → |
| 86 | + record { index = Lift _ ⊤ |
| 87 | + ; has-is-set = hlevel 2 |
| 88 | + ; dom = λ _ → my-silly-functor.₀ y |
| 89 | + ; map = λ _ → {! !} |
| 90 | + ; factor = λ h → do |
| 91 | + pure $ {! !} , {! !} , {! !} |
| 92 | + } |
| 93 | + G = Functor.op $ op-adj .fst |
| 94 | + Gᵒᵖ⊣Fᵒᵖ = op-adj .snd |
| 95 | +``` |
0 commit comments