Remove some obsolete lax functors of 2-categories

Removing the old definition lets us give some more sensible names to the
new strict 2-functors.

Author: phijor

GpdCont/ActionContainer/AsFamily.agda

@@ -10,7 +10,7 @@ open import GpdCont.Group.MapConjugator using (Conjugator)
 open import GpdCont.GroupAction.Base using (Action ; _⁺_)
 open import GpdCont.GroupAction.Equivariant using (isEquivariantMap[_][_,_])
 open import GpdCont.GroupAction.TwoCategory using (GroupAction ; isLocallyStrictGroupAction)
-open import GpdCont.GroupAction.Delooping as ActionDelooping renaming (Deloopingˢ to ActionDelooping)
+open import GpdCont.GroupAction.Delooping as ActionDelooping using (ActionDelooping)
 open import GpdCont.SetBundle.Base ℓ using (SetBundle)
 
 open import GpdCont.TwoCategory.Base using (TwoCategory)
@@ -150,14 +150,14 @@ module _ where
   open LocalFunctor Fam𝔹
 
   isLocallyFullyFaithfulFam𝔹 : isLocallyFullyFaithful
-  isLocallyFullyFaithfulFam𝔹 = Fam𝔹.isLocallyFullyFaithfulFam (isLocallyFullyFaithfulDelooping ℓ)
+  isLocallyFullyFaithfulFam𝔹 = Fam𝔹.isLocallyFullyFaithfulFam (ActionDelooping.isLocallyFullyFaithfulDelooping ℓ)
 
   module _ (choice : AxiomOfSetChoice ℓ ℓ) where
     isLocallyEssentiallySurjectiveFam𝔹 : isLocallyEssentiallySurjective
     isLocallyEssentiallySurjectiveFam𝔹 = Fam𝔹.isLocallyEssentiallySurjectiveFam
       choice
       (isLocallyStrictGroupAction ℓ)
-      (isEssentiallySurjectiveDelooping ℓ)
+      (ActionDelooping.isEssentiallySurjectiveDelooping ℓ)
 
     isLocallyWeakEquivalenceFam𝔹 : isLocallyWeakEquivalence
     isLocallyWeakEquivalenceFam𝔹 = isLocallyFullyFaithful×EssentiallySurjective→isLocallyWeakEquivalence

GpdCont/Delooping/Functor.agda

@@ -7,9 +7,7 @@ open import GpdCont.Group.MapConjugator using (Conjugator ; idConjugator ; compC
 open import GpdCont.Group.TwoCategory using (TwoGroup)
 
 open import GpdCont.TwoCategory.Base
-open import GpdCont.TwoCategory.LaxFunctor
 open import GpdCont.TwoCategory.StrictFunctor using (StrictFunctor)
-open import GpdCont.TwoCategory.Pseudofunctor
 open import GpdCont.TwoCategory.HomotopyGroupoid using (hGpdCat ; isLocallyGroupoidalHGpdCat)
 open import GpdCont.TwoCategory.LocalCategory using (LocalCategory)
 open import GpdCont.TwoCategory.StrictFunctor.LocalFunctor as LocalFunctor using (LocalFunctor)
@@ -204,130 +202,6 @@ module TwoFunc (ℓ : Level) where
   𝔹-rel-trans : (h₁ : TwoGroup.rel φ ψ) (h₂ : TwoGroup.rel ψ ρ) → 𝔹-rel (compConjugator h₁ h₂) ≡ 𝔹-rel h₁ ∙ 𝔹-rel h₂
   𝔹-rel-trans {φ} {ψ} {ρ} = Map.map≡-comp-∙ φ ψ ρ
 
-  private
-    𝔹-trans-lax : (φ : TwoGroup.hom G H) (ψ : TwoGroup.hom H K) → (𝔹-hom φ hGpdCat.∙₁ 𝔹-hom ψ) ≡ 𝔹-hom (φ TwoGroup.∙₁ ψ)
-    𝔹-trans-lax {G} {H} {K} φ ψ = funExt (𝔹G.elimSet isSetMotive refl λ g i j → 𝔹K.loop ((φ TwoGroup.∙₁ ψ) .fst g) i) where
-      module 𝔹G = Delooping G
-      module 𝔹K = Delooping K
-
-      isSetMotive : (x : Delooping.𝔹 G) → isSet ((𝔹-hom ψ $ 𝔹-hom φ x) ≡ (𝔹-hom (φ TwoGroup.∙₁ ψ) x))
-      isSetMotive x = 𝔹K.isGroupoid𝔹 _ _
-
-    𝔹-trans-lax-natural : {φ₁ φ₂ : TwoGroup.hom G H} {ψ₁ ψ₂ : TwoGroup.hom H K}
-      → (h : TwoGroup.rel φ₁ φ₂)
-      → (k : TwoGroup.rel ψ₁ ψ₂)
-      → ((𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k) ∙ 𝔹-trans-lax φ₂ ψ₂) ≡ (𝔹-trans-lax φ₁ ψ₁ ∙ 𝔹-rel (h TwoGroup.∙ₕ k))
-    𝔹-trans-lax-natural {G} {H} {K} {φ₁} {φ₂} {ψ₁} {ψ₂} h k = funExtSquare lax where
-      module K = GroupStr (str K)
-      module 𝔹G = Delooping G
-      module 𝔹H = Delooping H
-      module 𝔹K = Delooping K
-
-      open 𝔹G using (cong⋆ ; cong⋆-∙)
-
-      -- The meat of the proof: Horizontal composition computes to the correct loop at the point.
-      -- This is almost definitional, except that the LHS computes to the diagonal of a composite square,
-      -- in particular it is the diagonal that shows that the group element underlying `(h TwoGroup.∙ₕ k)`
-      -- is a conjugator of ψ₁ and ψ₂.
-      lemma : cong⋆ (𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k) ≡ 𝔹K.loop ((h TwoGroup.∙ₕ k) .fst)
-      lemma = Map.map≡-loopᵝ ψ₁ ψ₂ k (h .fst)
-
-      lax⋆ : cong⋆ (((𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k) ∙ 𝔹-trans-lax φ₂ ψ₂)) ≡ cong⋆ (𝔹-trans-lax φ₁ ψ₁ ∙ 𝔹-rel (h TwoGroup.∙ₕ k))
-      lax⋆ =
-        cong⋆ (((𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k) ∙ 𝔹-trans-lax φ₂ ψ₂))      ≡⟨ cong⋆-∙ (𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k) (𝔹-trans-lax φ₂ ψ₂) ⟩
-        cong⋆ (𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k) ∙ cong⋆ (𝔹-trans-lax φ₂ ψ₂)  ≡⟨⟩
-        cong⋆ (𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k) ∙ refl                       ≡⟨ sym $ GL.rUnit _ ⟩
-        cong⋆ (𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k)                              ≡⟨ lemma ⟩
-        𝔹K.loop ((h TwoGroup.∙ₕ k) .fst)                                ≡⟨⟩
-        cong⋆ (𝔹-rel (h TwoGroup.∙ₕ k))                                 ≡⟨ GL.lUnit _ ⟩
-        refl ∙ cong⋆ (𝔹-rel (h TwoGroup.∙ₕ k))                          ≡⟨⟩
-        cong⋆ (𝔹-trans-lax φ₁ ψ₁) ∙ cong⋆ (𝔹-rel (h TwoGroup.∙ₕ k))     ≡⟨ sym $ cong⋆-∙ (𝔹-trans-lax φ₁ ψ₁) (𝔹-rel (h TwoGroup.∙ₕ k)) ⟩
-        cong⋆ (𝔹-trans-lax φ₁ ψ₁ ∙ 𝔹-rel (h TwoGroup.∙ₕ k)) ∎
-
-      lax : (x : 𝔹G.𝔹) → (((𝔹-rel h hGpdCat.∙ₕ 𝔹-rel k) ∙ 𝔹-trans-lax φ₂ ψ₂) ≡$S x) ≡ (𝔹-trans-lax φ₁ ψ₁ ∙ 𝔹-rel (h TwoGroup.∙ₕ k) ≡$S x)
-      lax = 𝔹G.elimProp (λ x → 𝔹K.isGroupoid𝔹 _ _ _ _) lax⋆
-
-    𝔹-id-lax : (G : TwoGroup.ob) → hGpdCat.id-hom (𝔹-ob G) ≡ 𝔹-hom (TwoGroup.id-hom G)
-    𝔹-id-lax G = sym (Map.map-id G)
-
-    𝔹-assoc : (φ : TwoGroup.hom G H) (ψ : TwoGroup.hom H K) (ρ : TwoGroup.hom K L)
-      → Square
-        ((𝔹-trans-lax φ ψ hGpdCat.∙ₕ refl′ (𝔹-hom ρ)) ∙ 𝔹-trans-lax (φ TwoGroup.∙₁ ψ) ρ)
-        ((refl′ (𝔹-hom φ) hGpdCat.∙ₕ 𝔹-trans-lax ψ ρ) ∙ 𝔹-trans-lax φ (ψ TwoGroup.∙₁ ρ))
-        (refl′ ((𝔹-hom φ hGpdCat.∙₁ 𝔹-hom ψ) hGpdCat.∙₁ 𝔹-hom ρ))
-        (cong 𝔹-hom (TwoGroup.comp-hom-assoc φ ψ ρ))
-    𝔹-assoc {G} {H} {L} φ ψ ρ = funExtSquare assoc-ext where
-      module 𝔹G = Delooping G
-      module 𝔹L = Delooping L
-
-      open 𝔹G using (cong⋆ ; cong⋆-∙)
-
-      assoc-ext : (x : 𝔹G.𝔹) → Square
-        ((𝔹-trans-lax φ ψ hGpdCat.∙ₕ refl′ (𝔹-hom ρ)) ∙ 𝔹-trans-lax (φ TwoGroup.∙₁ ψ) ρ ≡$ x)
-        (((refl′ (𝔹-hom φ) hGpdCat.∙ₕ 𝔹-trans-lax ψ ρ) ∙ 𝔹-trans-lax φ (ψ TwoGroup.∙₁ ρ)) ≡$ x)
-        refl
-        (λ i → 𝔹-hom (TwoGroup.comp-hom-assoc φ ψ ρ i) x)
-      assoc-ext = 𝔹G.elimProp (λ x → 𝔹L.isPropDeloopingSquare) $
-        let
-          p = (𝔹-trans-lax φ ψ hGpdCat.∙ₕ refl′ (𝔹-hom ρ))
-          q = (𝔹-trans-lax (φ TwoGroup.∙₁ ψ) ρ)
-          r = (refl′ (𝔹-hom φ) hGpdCat.∙ₕ 𝔹-trans-lax ψ ρ)
-          s = (𝔹-trans-lax φ (ψ TwoGroup.∙₁ ρ))
-        in
-        (cong⋆ $ p ∙ q)     ≡⟨ cong⋆-∙ p q ⟩
-        (cong⋆ p ∙ cong⋆ q) ≡⟨⟩
-        (refl ∙ refl)       ≡⟨ sym $ cong⋆-∙ r s ⟩
-        (cong⋆ $ r ∙ s)     ∎
-
-    𝔹-unit-left : (φ : TwoGroup.hom G H)
-      → Square
-        ((𝔹-id-lax G hGpdCat.∙ₕ refl′ (𝔹-hom φ)) hGpdCat.∙ᵥ 𝔹-trans-lax idGroupHom φ)
-        (refl′ (𝔹-hom φ))
-        (hGpdCat.comp-hom-unit-left (𝔹-hom φ))
-        (cong 𝔹-hom (TwoGroup.comp-hom-unit-left φ))
-    𝔹-unit-left {G} {H} φ = 𝔹-hom-Square unit-left⋆ where
-      module 𝔹G = Delooping G
-      module 𝔹H = Delooping H
-
-      p : (id ⟨ 𝔹-ob G ⟩) ⋆ (𝔹-hom φ) ≡ (𝔹-hom idGroupHom) ⋆ (𝔹-hom φ)
-      p = 𝔹-id-lax G hGpdCat.∙ₕ refl′ (𝔹-hom φ)
-
-      q : (𝔹-hom idGroupHom ⋆ 𝔹-hom φ) ≡ 𝔹-hom (idGroupHom TwoGroup.∙₁ φ)
-      q = 𝔹-trans-lax idGroupHom φ
-
-      unit-left⋆ : 𝔹G.cong⋆ (p ∙ q) ≡ refl′ 𝔹H.⋆
-      unit-left⋆ = 𝔹G.cong⋆-∙ p q ∙ sym compPathRefl
-
-    𝔹-unit-right : (φ : TwoGroup.hom G H)
-      → Square
-        ((refl′ (𝔹-hom φ) hGpdCat.∙ₕ 𝔹-id-lax H) hGpdCat.∙ᵥ 𝔹-trans-lax φ idGroupHom)
-        (refl′ (𝔹-hom φ))
-        (hGpdCat.comp-hom-unit-right (𝔹-hom φ))
-        (cong 𝔹-hom (TwoGroup.comp-hom-unit-right φ))
-    𝔹-unit-right {G} {H} φ = 𝔹-hom-Square unit-right⋆ where
-      module 𝔹G = Delooping G
-      module 𝔹H = Delooping H
-
-      p = refl′ (𝔹-hom φ) hGpdCat.∙ₕ 𝔹-id-lax H
-      q = 𝔹-trans-lax φ idGroupHom
-
-      -- Both p and q reduce to refl at the point:
-      unit-right⋆ : 𝔹G.cong⋆ (p ∙ q) ≡ refl′ 𝔹H.⋆
-      unit-right⋆ = 𝔹G.cong⋆-∙ p q ∙ sym compPathRefl
-
-  TwoDelooping : LaxFunctor (TwoGroup ℓ) (hGpdCat ℓ)
-  TwoDelooping .LaxFunctor.F-ob = 𝔹-ob
-  TwoDelooping .LaxFunctor.F-hom = 𝔹-hom
-  TwoDelooping .LaxFunctor.F-rel = 𝔹-rel
-  TwoDelooping .LaxFunctor.F-rel-id = 𝔹-rel-id
-  TwoDelooping .LaxFunctor.F-rel-trans = 𝔹-rel-trans
-  TwoDelooping .LaxFunctor.F-trans-lax = 𝔹-trans-lax
-  TwoDelooping .LaxFunctor.F-trans-lax-natural = 𝔹-trans-lax-natural
-  TwoDelooping .LaxFunctor.F-id-lax = 𝔹-id-lax
-  TwoDelooping .LaxFunctor.F-assoc = 𝔹-assoc
-  TwoDelooping .LaxFunctor.F-unit-left = 𝔹-unit-left
-  TwoDelooping .LaxFunctor.F-unit-right = 𝔹-unit-right
-
   private
     𝔹-hom-id : (G : TwoGroup.ob) → hGpdCat.id-hom (𝔹-ob G) ≡ 𝔹-hom (TwoGroup.id-hom G)
     𝔹-hom-id G = sym (Map.map-id G)
@@ -402,42 +276,42 @@ module TwoFunc (ℓ : Level) where
       unit-right = 𝔹-hom-Square (reflSquare 𝔹H.⋆)
 
 
-  TwoDeloopingˢ : StrictFunctor (TwoGroup ℓ) (hGpdCat ℓ)
-  TwoDeloopingˢ .StrictFunctor.F-ob = 𝔹-ob
-  TwoDeloopingˢ .StrictFunctor.F-hom = 𝔹-hom
-  TwoDeloopingˢ .StrictFunctor.F-rel = 𝔹-rel
-  TwoDeloopingˢ .StrictFunctor.F-rel-id = 𝔹-rel-id
-  TwoDeloopingˢ .StrictFunctor.F-rel-trans = 𝔹-rel-trans
-  TwoDeloopingˢ .StrictFunctor.F-hom-comp = 𝔹-hom-comp
-  TwoDeloopingˢ .StrictFunctor.F-hom-id = 𝔹-hom-id
-  TwoDeloopingˢ .StrictFunctor.F-assoc-filler-left = 𝔹-assoc.filler-left
-  TwoDeloopingˢ .StrictFunctor.F-assoc-filler-right = 𝔹-assoc.filler-right
-  TwoDeloopingˢ .StrictFunctor.F-assoc = 𝔹-assoc.assoc
-  TwoDeloopingˢ .StrictFunctor.F-unit-left-filler = 𝔹-unit-left.filler
-  TwoDeloopingˢ .StrictFunctor.F-unit-left = 𝔹-unit-left.unit-left
-  TwoDeloopingˢ .StrictFunctor.F-unit-right-filler = 𝔹-unit-right.filler
-  TwoDeloopingˢ .StrictFunctor.F-unit-right = 𝔹-unit-right.unit-right
+  𝔹 : StrictFunctor (TwoGroup ℓ) (hGpdCat ℓ)
+  𝔹 .StrictFunctor.F-ob = 𝔹-ob
+  𝔹 .StrictFunctor.F-hom = 𝔹-hom
+  𝔹 .StrictFunctor.F-rel = 𝔹-rel
+  𝔹 .StrictFunctor.F-rel-id = 𝔹-rel-id
+  𝔹 .StrictFunctor.F-rel-trans = 𝔹-rel-trans
+  𝔹 .StrictFunctor.F-hom-comp = 𝔹-hom-comp
+  𝔹 .StrictFunctor.F-hom-id = 𝔹-hom-id
+  𝔹 .StrictFunctor.F-assoc-filler-left = 𝔹-assoc.filler-left
+  𝔹 .StrictFunctor.F-assoc-filler-right = 𝔹-assoc.filler-right
+  𝔹 .StrictFunctor.F-assoc = 𝔹-assoc.assoc
+  𝔹 .StrictFunctor.F-unit-left-filler = 𝔹-unit-left.filler
+  𝔹 .StrictFunctor.F-unit-left = 𝔹-unit-left.unit-left
+  𝔹 .StrictFunctor.F-unit-right-filler = 𝔹-unit-right.filler
+  𝔹 .StrictFunctor.F-unit-right = 𝔹-unit-right.unit-right
 
   private
-    module TwoDeloopingˢ = StrictFunctor TwoDeloopingˢ
+    module 𝔹 = StrictFunctor 𝔹
 
-  isLocallyFullyFaithfulDelooping : LocalFunctor.isLocallyFullyFaithful TwoDeloopingˢ
+  isLocallyFullyFaithfulDelooping : LocalFunctor.isLocallyFullyFaithful 𝔹
   isLocallyFullyFaithfulDelooping G H = goal where module _ (φ ψ : TwoGroup.hom G H) where
     goal : isEquiv 𝔹-rel
     goal = equivIsEquiv (MapPathEquiv.map≡Equiv φ ψ)
 
   localDeloopingEmbedding : {G H : TwoGroup.ob} (φ ψ : TwoGroup.hom G H)
-    → TwoGroup.rel φ ψ ≃ hGpdCat.rel (TwoDeloopingˢ.₁ φ) (TwoDeloopingˢ.₁ ψ)
-  localDeloopingEmbedding = LocalFunctor.localEmbedding TwoDeloopingˢ isLocallyFullyFaithfulDelooping
+    → TwoGroup.rel φ ψ ≃ hGpdCat.rel (𝔹.₁ φ) (𝔹.₁ ψ)
+  localDeloopingEmbedding = LocalFunctor.localEmbedding 𝔹 isLocallyFullyFaithfulDelooping
 
-  isLocallyEssentiallySurjectiveDelooping : LocalFunctor.isLocallyEssentiallySurjective TwoDeloopingˢ
+  isLocallyEssentiallySurjectiveDelooping : LocalFunctor.isLocallyEssentiallySurjective 𝔹
   isLocallyEssentiallySurjectiveDelooping G H = goal where module _ (f : ⟨ 𝔹-ob G ⟩ → ⟨ 𝔹-ob H ⟩) where
     open import Cubical.HITs.PropositionalTruncation.Monad
     goal : ∃[ φ ∈ GroupHom G H ] CatIso (LocalCategory _ (𝔹-ob G) (𝔹-ob H)) (map φ) f
     goal = do
       (φ , section-f-mapφ) ← LocalInverse.isSurjection-map f
       ∃-intro φ $ pathToIso section-f-mapφ
 
-  isLocallyWeakEquivalenceDelooping : LocalFunctor.isLocallyWeakEquivalence TwoDeloopingˢ
+  isLocallyWeakEquivalenceDelooping : LocalFunctor.isLocallyWeakEquivalence 𝔹
   isLocallyWeakEquivalenceDelooping G H .isWeakEquivalence.fullfaith = isLocallyFullyFaithfulDelooping G H
   isLocallyWeakEquivalenceDelooping G H .isWeakEquivalence.esssurj = isLocallyEssentiallySurjectiveDelooping G H