diff --git a/src/Categories/Bicategory/Adjunction.agda b/src/Categories/Bicategory/Adjunction.agda new file mode 100644 index 000000000..f439bcc0f --- /dev/null +++ b/src/Categories/Bicategory/Adjunction.agda @@ -0,0 +1,56 @@ +{-# OPTIONS --without-K --safe #-} + +module Categories.Bicategory.Adjunction where + +open import Categories.Bicategory +import Categories.Bicategory.Extras as Extras +open import Categories.Category +open import Level + +private + variable + o β„“ e t : Level + +module _ (π’ž : Bicategory o β„“ e t) where + open Bicategory π’ž + + record Adjunction (A B : Obj) : Set (o βŠ” β„“ βŠ” e βŠ” t) where + private + module C = Extras π’ž + + field + L : A ⇒₁ B + R : B ⇒₁ A + + field + unit : id₁ β‡’β‚‚ R βŠšβ‚€ L + counit : L βŠšβ‚€ R β‡’β‚‚ id₁ + + private +{- + L 1 β†’ L (R L) β†’ (L R) L + ↓ L 1 + 1 ∘ L ~ ↓ + ↓ L + L +-} + l-triangle-l : L βŠšβ‚€ id₁ β‡’β‚‚ L + l-triangle-l = C.unitorΛ‘.from ∘α΅₯ (counit βŠšβ‚ idβ‚‚) ∘α΅₯ C.associator.to ∘α΅₯ (idβ‚‚ βŠšβ‚ unit) + + l-triangle-r : L βŠšβ‚€ id₁ β‡’β‚‚ L + l-triangle-r = C.unitorΚ³.from +{- + 1 R β†’ (R L) R β†’ R (L R) + ↓ L 1 + R ∘ id ~ ↓ + ↓ L + R +-} + r-triangle-l : id₁ βŠšβ‚€ R β‡’β‚‚ R + r-triangle-l = C.unitorΚ³.from ∘α΅₯ (idβ‚‚ βŠšβ‚ counit) ∘α΅₯ C.associator.from ∘α΅₯ (unit βŠšβ‚ idβ‚‚) + + r-triangle-r : id₁ βŠšβ‚€ R β‡’β‚‚ R + r-triangle-r = C.unitorΛ‘.from + field + l-triangle : l-triangle-l C.β‰ˆ l-triangle-r + r-triangle : r-triangle-l C.β‰ˆ r-triangle-r