UniAgda.Categories.Adjunctions

Table of Contents

1 Prelude

2 Definition

2.1 Sigma version

isLeftAdjoint-sig :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                    (Left : Functor A B)
                     Type (i  j  k  l)
isLeftAdjoint-sig {A = A} {B = B} Left =
  let module A = Precategory A in
  let module B = Precategory B in
  let module Left = Functor Left in
  Σ[ Right  (Functor B A) ] (
    Σ[ unit  (NaturalTransformation Idᶠ (Right oF Left)) ] (
      Σ[ counit  (NaturalTransformation (Left oF Right) Idᶠ) ](
        let module Right = Functor Right in
        let module unit = NaturalTransformation unit in
        let module counit = NaturalTransformation counit in
        Σ[ left-triangle  ( (a : A.ob)  B.comp (counit.α-ob (Left.₀ a)) (Left.₁ (unit.α-ob a))  B.Id {Left.₀ a}) ](
           (b : B.ob)  A.comp (Right.₁ (counit.α-ob b)) (unit.α-ob (Right.₀ b))  A.Id {Right.₀ b}))))

isLeftAdjoint-sig→rec :  {i j k l} {A : Precategory i j} {B : Precategory k l} {Left : Functor A B}
                         (adj : isLeftAdjoint-sig Left)
                          isLeftAdjoint Left
isLeftAdjoint.Right (isLeftAdjoint-sig→rec adj) = pr₁ adj
isLeftAdjoint.unit (isLeftAdjoint-sig→rec adj) = pr₁ (pr₂ adj)
isLeftAdjoint.counit (isLeftAdjoint-sig→rec adj) = pr₁ (pr₂ (pr₂ adj))
isLeftAdjoint.left-triangle (isLeftAdjoint-sig→rec adj) = pr₁ (pr₂ (pr₂ (pr₂ adj)))
isLeftAdjoint.right-triangle (isLeftAdjoint-sig→rec adj) =  pr₂ (pr₂ (pr₂ (pr₂ adj)))

isLeftAdjoint-rec→sig :  {i j k l} {A : Precategory i j} {B : Precategory k l} {Left : Functor A B}
                        (adj : isLeftAdjoint Left)
                         isLeftAdjoint-sig Left
isLeftAdjoint-rec→sig adj =
  let module adj = isLeftAdjoint adj in
  adj.Right ,
  adj.unit ,
  adj.counit ,
  adj.left-triangle ,
  adj.right-triangle

isLeftAdjoint-rec→sig→rec :  {i j k l} {A : Precategory i j} {B : Precategory k l} {Left : Functor A B}
                            (adj : isLeftAdjoint Left)
                             (isLeftAdjoint-sig→rec o isLeftAdjoint-rec→sig) adj  adj
isLeftAdjoint-rec→sig→rec adj = refl

isLeftAdjoint-sig→rec→sig :  {i j k l} {A : Precategory i j} {B : Precategory k l} {Left : Functor A B}
                            (adj : isLeftAdjoint-sig Left)
                             (isLeftAdjoint-rec→sig {Left = Left} o isLeftAdjoint-sig→rec) adj  adj
isLeftAdjoint-sig→rec→sig (Right , unit , counit , left-triangle , right-triangle) =
  path-equiv-sigma (refl ,
    path-equiv-sigma (refl ,
      (path-equiv-sigma (refl ,
        (path-equiv-sigma (refl ,
          refl))))))

isLeftAdjoint-sig-Equiv :  {i j k l} {A : Precategory i j} {B : Precategory k l} {Left : Functor A B}
                           isLeftAdjoint-sig Left  isLeftAdjoint Left
isLeftAdjoint-sig-Equiv {Left = Left} = equiv-adjointify
  (isLeftAdjoint-sig→rec ,
  isLeftAdjoint-rec→sig ,
  isLeftAdjoint-rec→sig→rec ,
  isLeftAdjoint-sig→rec→sig {Left = Left})

3 Properties

Author: James Leslie

Created: 2021-03-27 Sat 10:47