Category of groups, uniqness of adjunctions (#1065)

* - Introduced a new module `LeftAdjointUniqeUpToNatIso` for proving the uniqueness of left adjoints up to natural isomorphisms.
- Defined `AssocCong₂⋆L` and `AssocCong₂⋆R` helpers
- Defined `GroupCategory` as a category of groups, `Forget` functor , equivalence `GroupsCatIso≃GroupEquiv`, and univalence of Grp.

* uniqness of right adj

* minor cleanup

* more explicit definition to typecheck with agda 2.6.3

* Revert "minor cleanup"

This reverts commit 02bd5e2.

* Revert "more explicit definition to typecheck with agda 2.6.3"

This reverts commit 2e626b6.

Cubical/Categories/Adjoint.agda

@@ -3,9 +3,12 @@
 module Cubical.Categories.Adjoint where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+
 open import Cubical.Data.Sigma
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
+open import Cubical.Categories.Instances.Functors
 open import Cubical.Categories.NaturalTransformation
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
@@ -61,6 +64,125 @@ module UnitCounit {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Funct
       triangleIdentities : TriangleIdentities η ε
     open TriangleIdentities triangleIdentities public
 
+
+private
+  variable
+    C : Category ℓC ℓC'
+    D : Category ℓC ℓC'
+
+
+module _ {F : Functor C D} {G : Functor D C} where
+  open UnitCounit
+  open _⊣_
+  open NatTrans
+  open TriangleIdentities
+  opositeAdjunction : (F ⊣ G) → ((G ^opF) ⊣ (F ^opF))
+  N-ob (η (opositeAdjunction x)) = N-ob (ε x)
+  N-hom (η (opositeAdjunction x)) f = sym (N-hom (ε x) f)
+  N-ob (ε (opositeAdjunction x)) = N-ob (η x)
+  N-hom (ε (opositeAdjunction x)) f = sym (N-hom (η x) f)
+  Δ₁ (triangleIdentities (opositeAdjunction x)) =
+    Δ₂ (triangleIdentities x)
+  Δ₂ (triangleIdentities (opositeAdjunction x)) =
+   Δ₁ (triangleIdentities x)
+
+  Iso⊣^opF : Iso (F ⊣ G) ((G ^opF) ⊣ (F ^opF))
+  fun Iso⊣^opF = opositeAdjunction
+  inv Iso⊣^opF = _
+  rightInv Iso⊣^opF _ = refl
+  leftInv Iso⊣^opF _ = refl
+
+private
+  variable
+    F F' : Functor C D
+    G G' : Functor D C
+
+
+module AdjointUniqeUpToNatIso where
+ open UnitCounit
+ module Left
+          (F⊣G  : _⊣_ {D = D} F G)
+          (F'⊣G : F' ⊣ G) where
+  open NatTrans
+
+  private
+    variable
+      H H' : Functor C D
+
+  _D⋆_ = seq' D
+
+  m : (H⊣G : H ⊣ G) (H'⊣G : H' ⊣ G) →
+        ∀ {x} → D [ H ⟅ x ⟆ , H' ⟅ x ⟆ ]
+  m {H = H} H⊣G H'⊣G =
+    H ⟪ (H'⊣G .η) ⟦ _ ⟧ ⟫ ⋆⟨ D ⟩ (H⊣G .ε) ⟦ _ ⟧ where open _⊣_
+
+  private
+   s : (H⊣G : H ⊣ G) (H'⊣G : H' ⊣ G) → ∀ {x} →
+           seq' D (m H'⊣G H⊣G {x}) (m H⊣G H'⊣G {x})
+              ≡ D .id
+   s {H = H} {H' = H'} H⊣G H'⊣G = by-N-homs ∙ by-Δs
+     where
+      open _⊣_ H⊣G  using (η ; Δ₂)
+      open _⊣_ H'⊣G using (ε ; Δ₁)
+      by-N-homs =
+        AssocCong₂⋆R {C = D} _
+        (AssocCong₂⋆L {C = D} (sym (N-hom ε _)) _)
+          ∙ cong₂ _D⋆_
+               (sym (F-seq H' _ _)
+                ∙∙ cong (H' ⟪_⟫) ((sym (N-hom η  _)))
+                ∙∙ F-seq H' _ _)
+               (sym (N-hom ε _))
+
+      by-Δs =
+        ⋆Assoc D _ _ _
+        ∙∙ cong (H' ⟪ _ ⟫ D⋆_)
+             (sym (⋆Assoc D _ _ _)
+             ∙ cong (_D⋆ ε ⟦ _ ⟧)
+                 (  sym (F-seq H' _ _)
+                 ∙∙ cong (H' ⟪_⟫) (Δ₂ (H' ⟅ _ ⟆))
+                 ∙∙ F-id H')
+             ∙ ⋆IdL D _)
+        ∙∙ Δ₁ _
+
+  open NatIso
+  open isIso
+
+  F≅ᶜF' : F ≅ᶜ F'
+  N-ob (trans F≅ᶜF') _ = _
+  N-hom (trans F≅ᶜF') _ =
+       sym (⋆Assoc D _ _ _)
+    ∙∙ cong (_D⋆ (F⊣G .ε) ⟦ _ ⟧)
+         (sym (F-seq F _ _)
+         ∙∙ cong (F ⟪_⟫) (N-hom (F'⊣G .η) _)
+         ∙∙ (F-seq F _ _))
+    ∙∙ AssocCong₂⋆R {C = D} _ (N-hom (F⊣G .ε) _)
+   where open _⊣_
+  inv (nIso F≅ᶜF' _) = _
+  sec (nIso F≅ᶜF' _) = s F⊣G F'⊣G
+  ret (nIso F≅ᶜF' _) = s F'⊣G F⊣G
+
+  F≡F' : isUnivalent D → F ≡ F'
+  F≡F' univD =
+   isUnivalent.CatIsoToPath
+    (isUnivalentFUNCTOR _ _ univD)
+     (NatIso→FUNCTORIso _ _ F≅ᶜF')
+
+ module Right (F⊣G  : F UnitCounit.⊣ G)
+              (F⊣G' : F UnitCounit.⊣ G') where
+
+  G≅ᶜG' : G ≅ᶜ G'
+  G≅ᶜG' = Iso.inv congNatIso^opFiso
+    (Left.F≅ᶜF' (opositeAdjunction F⊣G')
+                (opositeAdjunction F⊣G))
+
+  open NatIso
+
+  G≡G' : isUnivalent _ → G ≡ G'
+  G≡G' univC =
+   isUnivalent.CatIsoToPath
+    (isUnivalentFUNCTOR _ _ univC)
+     (NatIso→FUNCTORIso _ _ G≅ᶜG')
+
 module NaturalBijection where
   -- Adjoint def 2: natural bijection
   record _⊣_ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
@@ -122,7 +244,7 @@ definition to the first.
 The second unnamed module does the reverse.
 -}
 
-module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) where
+module _ (F : Functor C D) (G : Functor D C) where
   open UnitCounit
   open NaturalBijection renaming (_⊣_ to _⊣²_)
   module _ (adj : F ⊣² G) where

Cubical/Categories/Category/Base.agda

@@ -136,7 +136,6 @@ _⋆_ (C ^op) f g      = g ⋆⟨ C ⟩ f
 ⋆Assoc (C ^op) f g h = sym (C .⋆Assoc _ _ _)
 isSetHom (C ^op)     = C .isSetHom
 
-
 ΣPropCat : (C : Category ℓ ℓ') (P : ℙ (ob C)) → Category ℓ ℓ'
 ob (ΣPropCat C P) = Σ[ x ∈ ob C ] x ∈ P
 Hom[_,_] (ΣPropCat C P) x y = C [ fst x , fst y ]

Cubical/Categories/Category/Properties.agda

@@ -91,3 +91,27 @@ module _ {C : Category ℓ ℓ'} where
                   → (r : PathP (λ i → C [ x , p i ]) f' f)
                   → f ⋆⟨ C ⟩ g ≡ seqP' {p = p} f' g
   rCatWhiskerP f' f g r = cong (λ v → v ⋆⟨ C ⟩ g) (sym (fromPathP r))
+
+
+  AssocCong₂⋆L : {x y' y z w : C .ob} →
+          {f' : C [ x , y' ]} {f : C [ x , y ]}
+          {g' : C [ y' , z ]} {g : C [ y , z ]}
+          → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g' → (h : C [ z , w ])
+          → f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ≡
+              f' ⋆⟨ C ⟩ (g' ⋆⟨ C ⟩ h)
+  AssocCong₂⋆L p h =
+    sym (⋆Assoc C _ _ h)
+      ∙∙ (λ i → p i ⋆⟨ C ⟩ h) ∙∙
+    ⋆Assoc C _ _ h
+
+  AssocCong₂⋆R : {x y z z' w : C .ob} →
+          (f : C [ x , y ])
+          {g' : C [ y , z' ]} {g : C [ y , z ]}
+          {h' : C [ z' , w ]} {h : C [ z , w ]}
+          → g ⋆⟨ C ⟩ h ≡ g' ⋆⟨ C ⟩ h'
+          → (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ≡
+              (f ⋆⟨ C ⟩ g') ⋆⟨ C ⟩ h'
+  AssocCong₂⋆R f p =
+    ⋆Assoc C f _ _
+      ∙∙ (λ i → f ⋆⟨ C ⟩ p i) ∙∙
+    sym (⋆Assoc C _ _ _)

Cubical/Categories/Functor/Base.agda

@@ -6,6 +6,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Powerset
+open import Cubical.Foundations.Isomorphism
 
 open import Cubical.Data.Sigma
 
@@ -142,12 +143,28 @@ funcCompOb≡ : ∀ (G : Functor D E) (F : Functor C D) (c : ob C)
             → funcComp G F .F-ob c ≡ G .F-ob (F .F-ob c)
 funcCompOb≡ G F c = refl
 
-_^opF : Functor C D → Functor (C ^op) (D ^op)
+
+_^opF  : Functor C D → Functor (C ^op) (D ^op)
 (F ^opF) .F-ob      = F .F-ob
 (F ^opF) .F-hom     = F .F-hom
 (F ^opF) .F-id      = F .F-id
 (F ^opF) .F-seq f g = F .F-seq g f
 
+open Iso
+Iso^opF : Iso (Functor C D) (Functor (C ^op) (D ^op))
+fun Iso^opF = _^opF
+inv Iso^opF = _^opF
+F-ob (rightInv Iso^opF b i) = F-ob b
+F-hom (rightInv Iso^opF b i) = F-hom b
+F-id (rightInv Iso^opF b i) = F-id b
+F-seq (rightInv Iso^opF b i) = F-seq b
+F-ob (leftInv Iso^opF a i) = F-ob a
+F-hom (leftInv Iso^opF a i) = F-hom a
+F-id (leftInv Iso^opF a i) = F-id a
+F-seq (leftInv Iso^opF a i) = F-seq a
+
+^opFEquiv : Functor C D ≃ Functor (C ^op) (D ^op)
+^opFEquiv = isoToEquiv Iso^opF
 
 -- Functoriality on full subcategories defined by propositions
 ΣPropCatFunc : {P : ℙ (ob C)} {Q : ℙ (ob D)} (F : Functor C D)

Cubical/Categories/Instances/Groups.agda

@@ -0,0 +1,75 @@
+-- The category Grp of groups
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Instances.Groups where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+
+open import Cubical.Categories.Category.Base renaming (isIso to isCatIso)
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Functor.Base
+
+open import Cubical.Data.Sigma
+
+module _ {ℓ : Level} where
+  open Category hiding (_∘_)
+
+  GroupCategory : Category (ℓ-suc ℓ) ℓ
+  GroupCategory .ob = Group ℓ
+  GroupCategory .Hom[_,_] = GroupHom
+  GroupCategory .id = idGroupHom
+  GroupCategory ._⋆_ = compGroupHom
+  GroupCategory .⋆IdL f = GroupHom≡ refl
+  GroupCategory .⋆IdR f = GroupHom≡ refl
+  GroupCategory .⋆Assoc f g h = GroupHom≡ refl
+  GroupCategory .isSetHom = isSetGroupHom
+
+  Forget : Functor GroupCategory (SET ℓ)
+  Functor.F-ob Forget G = fst G , GroupStr.is-set (snd G)
+  Functor.F-hom Forget = fst
+  Functor.F-id Forget = refl
+  Functor.F-seq Forget _ _ = refl
+
+  GroupsCatIso≃GroupEquiv : ∀ G G' →
+    CatIso GroupCategory G G' ≃
+     GroupEquiv G G'
+  GroupsCatIso≃GroupEquiv G G' =
+      Σ-cong-equiv-snd
+        (λ _ → propBiimpl→Equiv
+          (isPropIsIso _) (isPropIsEquiv _)
+           (isoToIsEquiv ∘ →iso) →ciso)
+       ∙ₑ Σ-assoc-swap-≃
+   where
+    open Iso
+    open isCatIso
+    →iso : ∀ {x} → isCatIso GroupCategory x → Iso _ _
+    fun (→iso ici) = _
+    inv (→iso ici) = fst (inv ici)
+    rightInv (→iso ici) b i = fst (sec ici i) b
+    leftInv (→iso ici) a i = fst (ret ici i) a
+
+    →ciso : ∀ {x} → isEquiv (fst x) → isCatIso GroupCategory x
+    fst (inv (→ciso is≃)) = _
+    snd (inv (→ciso {x} is≃)) =
+      isGroupHomInv ((_ , is≃) , (snd x))
+    sec (→ciso is≃) =
+     Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt (secEq (_ , is≃)))
+    ret (→ciso is≃) =
+     Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt (retEq (_ , is≃)))
+
+
+  isUnivalentGrp : isUnivalent {ℓ' = ℓ} GroupCategory
+  isUnivalent.univ isUnivalentGrp _ _ =
+   precomposesToId→Equiv _ _ (funExt
+               (Σ≡Prop isPropIsIso
+              ∘ Σ≡Prop (λ _ → isPropIsGroupHom _ _)
+              ∘ λ _ → transportRefl _))
+              (snd (GroupsCatIso≃GroupEquiv _ _ ∙ₑ GroupPath _ _))

Cubical/Categories/NaturalTransformation/Properties.agda

@@ -20,6 +20,9 @@ open import Cubical.Categories.NaturalTransformation.Base
 private
   variable
     ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+    C : Category ℓC ℓC'
+    D : Category ℓD ℓD'
+    F F' : Functor C D
 
 open isIsoC
 open NatIso
@@ -108,8 +111,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
 -- Natural isomorphism is path when the target category is univalent.
 
 module _
-  {C : Category ℓC ℓC'}
-  {D : Category ℓD ℓD'}(isUnivD : isUnivalent D)
+  (isUnivD : isUnivalent D)
   {F G : Functor C D} where
 
   open isUnivalent isUnivD
@@ -172,3 +174,22 @@ module _ {B : Category ℓB ℓB'}{C : Category ℓC ℓC'}{D : Category ℓD 
   CAT⋆Assoc F G H .trans .N-ob = idTrans ((H ∘F G) ∘F F) .N-ob
   CAT⋆Assoc F G H .trans .N-hom = idTrans ((H ∘F G) ∘F F) .N-hom
   CAT⋆Assoc F G H .nIso = idNatIso ((H ∘F G) ∘F F) .nIso
+
+
+
+⇒^opFiso : Iso (F ⇒ F') (_^opF {C = C} {D = D} F' ⇒ F ^opF )
+N-ob (fun ⇒^opFiso x) = N-ob x
+N-hom (fun ⇒^opFiso x) f = sym (N-hom x f)
+inv ⇒^opFiso = _
+rightInv ⇒^opFiso _ = refl
+leftInv ⇒^opFiso _ = refl
+
+congNatIso^opFiso : Iso (F ≅ᶜ F') (_^opF  {C = C} {D = D} F'  ≅ᶜ F ^opF )
+trans (fun congNatIso^opFiso x) = Iso.fun ⇒^opFiso (trans x)
+inv (nIso (fun congNatIso^opFiso x) x₁) = _
+sec (nIso (fun congNatIso^opFiso x) x₁) = ret (nIso x x₁)
+ret (nIso (fun congNatIso^opFiso x) x₁) = sec (nIso x x₁)
+inv congNatIso^opFiso = _
+rightInv congNatIso^opFiso _ = refl
+leftInv congNatIso^opFiso _ = refl
+

Cubical/Data/Sigma/Properties.agda

@@ -180,6 +180,15 @@ module _ {A : Type ℓ} {B : A → Type ℓ'} {C : ∀ a → B a → Type ℓ''}
 
   unquoteDecl Σ-Π-≃ = declStrictIsoToEquiv Σ-Π-≃ Σ-Π-Iso
 
+module _ {A : Type ℓ} {B : A → Type ℓ'} {B' : ∀ a → Type ℓ''} where
+  Σ-assoc-swap-Iso : Iso (Σ[ a ∈ Σ A B ] B' (fst a)) (Σ[ a ∈ Σ A B' ] B (fst a))
+  fun Σ-assoc-swap-Iso ((x , y) , z) = ((x , z) , y)
+  inv Σ-assoc-swap-Iso ((x , z) , y) = ((x , y) , z)
+  rightInv Σ-assoc-swap-Iso _ = refl
+  leftInv Σ-assoc-swap-Iso _  = refl
+
+  unquoteDecl Σ-assoc-swap-≃ = declStrictIsoToEquiv Σ-assoc-swap-≃ Σ-assoc-swap-Iso
+
 Σ-cong-iso-fst : (isom : Iso A A') → Iso (Σ A (B ∘ fun isom)) (Σ A' B)
 fun (Σ-cong-iso-fst isom) x = fun isom (x .fst) , x .snd
 inv (Σ-cong-iso-fst {B = B} isom) x = inv isom (x .fst) , subst B (sym (ε (x .fst))) (x .snd)