{- Category Theory: - Natural Transformations; - Kan Extensions; - Limits; - Adjunctions. Copyright (c) Groupoid Infinity, 2017-2018. HoTT 9.3 Adjunctions. -} module adj where import cat import fun unitCat: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = unit Hom (A B: Ob): U = unit id (A: Ob): Hom A A = tt c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = tt HomSet (A B: Ob): isSet (Hom A B) = setUnit L (A B: Ob): (f: unit) -> Path unit (c A A B (id A) f) f = split tt -> tt R (A B: Ob): (f: unit) -> Path unit (c A B B f (id B)) f = split tt -> tt Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = refl unit tt isNaturalTrans (C D: precategory) (F G: catfunctor C D) (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)): U = (x y: carrier C) (h: hom C x y) -> Path (hom D (F.1 x) (G.1 y)) (compose D (F.1 x) (F.1 y) (G.1 y) (F.2.1 x y h) (eta y)) (compose D (F.1 x) (G.1 x) (G.1 y) (eta x) (G.2.1 x y h)) -- Awodey CT 7.6. Natural transformation -- Natural Transformation ntrans (C D: precategory) (F G: catfunctor C D): U = (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)) * (isNaturalTrans C D F G eta) -- Kan Extensions extension (A B C: precategory) (K: catfunctor A B) (G: catfunctor A C) : U = (F: catfunctor B C) * (counit: ntrans A C (compFunctor A B C K F) G) * unit -- Functor to Unit Category unitFunc (C: precategory): catfunctor C unitCat = undefined -- Cone as Kan Extension cone (J C: precategory) (D: catfunctor J C): U = extension J unitCat C (unitFunc J) D -- universality of Kan Extension universality (A B C: precategory) (K: catfunctor A B) (G: catfunctor A C) (s t: extension A B C K G) : U = undefined -- Right Kan Extension ran (A B C: precategory) (K: catfunctor A B) (G: catfunctor A C) : U = (x: extension A B C K G) * ((y: extension A B C K G) -> isContr (universality A B C K G x y)) -- Limit limit (J C: precategory) (D: catfunctor J C): U = ran J unitCat C (unitFunc J) D -- ExtUniv : Extension K G → Set _ -- ExtUniv (extension S (nt α _)) = Σ (S ⇒ F) λ { (nt β _) → (∀ X → ε X ∘ β (apply K X) ≡ α X) } ntransL (C D: precategory) (F G: catfunctor C D) (f: ntrans C D F G) (B: precategory) (H: catfunctor B C) : ntrans B D (compFunctor B C D H F) (compFunctor B C D H G) = (eta, p) where F': catfunctor B D = compFunctor B C D H F G': catfunctor B D = compFunctor B C D H G eta (x: carrier B): hom D (F'.1 x) (G'.1 x) = f.1 (H.1 x) p (x y: carrier B) (h: hom B x y): Path (hom D (F'.1 x) (G'.1 y)) (compose D (F'.1 x) (F'.1 y) (G'.1 y) (F'.2.1 x y h) (eta y)) (compose D (F'.1 x) (G'.1 x) (G'.1 y) (eta x) (G'.2.1 x y h)) = f.2 (H.1 x) (H.1 y) (H.2.1 x y h) ntransR (C D: precategory) (F G: catfunctor C D) (f: ntrans C D F G) (E: precategory) (H: catfunctor D E) : ntrans C E (compFunctor C D E F H) (compFunctor C D E G H) = (eta, p) where F': catfunctor C E = compFunctor C D E F H G': catfunctor C E = compFunctor C D E G H eta (x: carrier C): hom E (F'.1 x) (G'.1 x) = H.2.1 (F.1 x) (G.1 x) (f.1 x) p (x y: carrier C) (h: hom C x y): Path (hom E (F'.1 x) (G'.1 y)) (compose E (F'.1 x) (F'.1 y) (G'.1 y) (F'.2.1 x y h) (eta y)) (compose E (F'.1 x) (G'.1 x) (G'.1 y) (eta x) (G'.2.1 x y h)) = comp (<_> hom E (F'.1 x) (G'.1 y)) (H.2.1 (F.1 x) (G.1 y) (f.2 x y h @ i)) [ (i = 0) -> H.2.2.2 (F.1 x) (F.1 y) (G.1 y) (F.2.1 x y h) (f.1 y), (i = 1) -> H.2.2.2 (F.1 x) (G.1 x) (G.1 y) (f.1 x) (G.2.1 x y h) ] hom3 (C D: precategory) (F: catfunctor C D) (G: catfunctor C D) (left: ntrans C D F G) (right: ntrans C D F G): U = undefined -- Adjointness Property -- NOTE: Adjunction is a special case of signature class of 3-morphisms areAdjoint (C D: precategory) (F: catfunctor D C) (G: catfunctor C D) (unit: ntrans D D (idFunctor D) (compFunctor D C D F G)) (counit: ntrans C C (compFunctor C D C G F) (idFunctor C)): U = prod ((x: carrier C) -> Path (hom D (G.1 x) (G.1 x)) (path D (G.1 x)) (h0 x)) ((x: carrier D) -> Path (hom C (F.1 x) (F.1 x)) (path C (F.1 x)) (h1 x)) where h0 (x: carrier C) : hom D (G.1 x) (G.1 x) = compose D (G.1 x) (G.1 (F.1 (G.1 x))) (G.1 x) ((ntransL D D (idFunctor D) (compFunctor D C D F G) unit C G).1 x) ((ntransR C C (compFunctor C D C G F) (idFunctor C) counit D G).1 x) h1 (x: carrier D) : hom C (F.1 x) (F.1 x) = compose C (F.1 x) (F.1 (G.1 (F.1 x))) (F.1 x) ((ntransR D D (idFunctor D) (compFunctor D C D F G) unit C F).1 x) ((ntransL C C (compFunctor C D C G F) (idFunctor C) counit D F).1 x) -- Adjoint of two Natural Transformations adjoint (C D: precategory) (F: catfunctor D C) (G: catfunctor C D): U = (unit: ntrans D D (idFunctor D) (compFunctor D C D F G)) * (counit: ntrans C C (compFunctor C D C G F) (idFunctor C)) * areAdjoint C D F G unit counit