def: finite limits of concrete groups

src/1Lab/Type/Pointed.lagda.md

@@ -35,6 +35,8 @@ Those are called **pointed maps**.
 ```agda
 _→∙_ : Type∙ ℓ → Type∙ ℓ' → Type _
 (A , a) →∙ (B , b) = Σ[ f ∈ (A → B) ] (f a ≡ b)
+
+infixr 0 _→∙_
 ```
 
 Pointed maps compose in a straightforward way.
@@ -58,3 +60,18 @@ funext∙ : {f g : A →∙ B}
         → f ≡ g
 funext∙ h pth i = funext h i , pth i
 ```
+
+The product of two pointed types is again a pointed type.
+
+```agda
+_×∙_ : Type∙ ℓ → Type∙ ℓ' → Type∙ (ℓ ⊔ ℓ')
+(A , a) ×∙ (B , b) = A × B , a , b
+
+infixr 5 _×∙_
+
+fst∙ : A ×∙ B →∙ A
+fst∙ = fst , refl
+
+snd∙ : A ×∙ B →∙ B
+snd∙ = snd , refl
+```

src/Algebra/Group/Concrete/FinitelyComplete.lagda.md

@@ -0,0 +1,84 @@
+<!--
+```agda
+open import Algebra.Group.Cat.FinitelyComplete
+open import Algebra.Group.Cat.Base
+open import Algebra.Group.Concrete
+
+open import Cat.Functor.Equivalence.Path
+open import Cat.Diagram.Limit.Finite
+open import Cat.Diagram.Product
+open import Cat.Prelude
+
+open import Homotopy.Connectedness.Automation
+open import Homotopy.Connectedness
+
+open ConcreteGroup
+open is-product
+open Product
+```
+-->
+
+```agda
+module Algebra.Group.Concrete.FinitelyComplete {ℓ} where
+```
+
+# Finite limits of concrete groups
+
+Since the category of [[concrete groups]] is equivalent to the
+[[category of groups]], and the latter is [[finitely complete]], then
+so is the former.
+
+```agda
+ConcreteGroups-finitely-complete : Finitely-complete (ConcreteGroups ℓ)
+ConcreteGroups-finitely-complete = subst Finitely-complete
+  (sym (eqv→path ConcreteGroups-is-category Groups-is-category _ π₁F-is-equivalence))
+  Groups-finitely-complete
+```
+
+However, the construction of binary [[products]] of concrete groups
+(corresponding to the [[direct product of groups]]) is natural enough to
+spell out explicitly: one can simply take the product of the underlying
+groupoids!
+
+```agda
+Direct-product-concrete : ConcreteGroup ℓ → ConcreteGroup ℓ → ConcreteGroup ℓ
+Direct-product-concrete G H .B = B G ×∙ B H
+Direct-product-concrete G H .has-is-connected = is-connected→is-connected∙ $
+  ×-is-n-connected 2
+    (is-connected∙→is-connected (G .has-is-connected))
+    (is-connected∙→is-connected (H .has-is-connected))
+Direct-product-concrete G H .has-is-groupoid = ×-is-hlevel 3
+  (G .has-is-groupoid)
+  (H .has-is-groupoid)
+
+ConcreteGroups-products
+  : (X Y : ConcreteGroup ℓ) → Product (ConcreteGroups ℓ) X Y
+ConcreteGroups-products X Y = prod where
+  prod : Product (ConcreteGroups ℓ) X Y
+  prod .apex = Direct-product-concrete X Y
+  prod .π₁ = fst∙
+  prod .π₂ = snd∙
+  prod .has-is-product .⟨_,_⟩ f g .fst x = f # x , g # x
+  prod .has-is-product .⟨_,_⟩ f g .snd = f .snd ,ₚ g .snd
+  prod .has-is-product .π₁∘⟨⟩ = funext∙ (λ _ → refl) (∙-idr _)
+  prod .has-is-product .π₂∘⟨⟩ = funext∙ (λ _ → refl) (∙-idr _)
+  prod .has-is-product .unique {Q} {f} {g} {u} p1 p2 =
+    funext∙ (λ x → p1 #ₚ x ,ₚ p2 #ₚ x) (fix ◁ square)
+    where
+      square : Square
+        (p1 #ₚ pt Q ,ₚ p2 #ₚ pt Q) ((fst∙ ∘∙ u) .snd ,ₚ (snd∙ ∘∙ u) .snd)
+        (f .snd ,ₚ g .snd) refl
+      square i = p1 i .snd ,ₚ p2 i .snd
+
+      fix : u .snd ≡ ((fst∙ ∘∙ u) .snd ,ₚ (snd∙ ∘∙ u) .snd)
+      fix i = ∙-idr (ap fst (u .snd)) (~ i) ,ₚ ∙-idr (ap snd (u .snd)) (~ i)
+```
+
+Similarly, the [[terminal]] concrete group is just the unit type.
+
+```agda
+Terminal-concrete : ConcreteGroup ℓ
+Terminal-concrete .B = Lift _ ⊤ , _
+Terminal-concrete .has-is-connected = is-connected→is-connected∙ (n-connected 2)
+Terminal-concrete .has-is-groupoid = hlevel 3
+```

src/Cat/Functor/Equivalence/Path.lagda.md

@@ -246,24 +246,6 @@ Category-identity-system-pre =
     (fst , (Subset-proj-embedding (λ x → is-identity-system-is-prop)))
 ```
 
-<!--
-```agda
-module
-  _ {o o' ℓ ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
-    (F : Functor C D)
-    (eqv : is-equivalence F)
-  where
-
-  private
-    open is-equivalence eqv
-    module C = Cat.Reasoning C
-    module D = Cat.Reasoning D
-    module F = Functor F
-  open _=>_
-
-```
--->
-
 Then, since the spaces of equivalences $\cC \cong \cD$ and
 isomorphisms $\cC \to \cD$ are both defined as the total space of
 a predicate on the same types, it suffices to show that the predicates
@@ -317,3 +299,17 @@ the necessary paths for showing that $F_0$ is an equivalence of types.
         .is-iso.rinv x → dcat .to-path       $ isoⁿ→iso (F∘F⁻¹≅Id eqv) _
         .is-iso.linv x → sym $ ccat .to-path $ isoⁿ→iso (Id≅F⁻¹∘F eqv) _
 ```
+
+<!--
+```agda
+module
+  _ {o ℓ} {C : Precategory o ℓ} {D : Precategory o ℓ}
+    (ccat : is-category C) (dcat : is-category D)
+    (F : Functor C D)
+    (eqv : is-equivalence F)
+  where
+
+  eqv→path : C ≡ D
+  eqv→path = ap fst (Category-identity-system .to-path {C , ccat} {D , dcat} (F , eqv))
+```
+-->

src/Homotopy/Connectedness.lagda.md

@@ -215,6 +215,15 @@ retract→is-n-connected (suc (suc n)) f g h a-conn =
     (is-n-connected-Tr (suc n) a-conn)
 ```
 
+<!--
+```agda
+is-n-connected-≃
+  : (n : Nat) (e : A ≃ B)
+  → is-n-connected A n → is-n-connected B n
+is-n-connected-≃ n e = retract→is-n-connected n (e .fst) _ (Equiv.ε e)
+```
+-->
+
 Since the truncation operator $\| - \|_n$ also preserves products, a
 remarkably similar argument shows that if $A$ and $B$ are $n$-connected,
 then so is $A \times B$.

src/Homotopy/Connectedness/Automation.lagda.md

@@ -77,4 +77,11 @@ instance
     → Connected (Path A x y) n
   Connected-Path {n = n} ⦃ conn-instance ac ⦄ = conn-instance
     (Path-is-connected n ac)
+
+  Connected-Lift
+    : ∀ {ℓ ℓ'} {A : Type ℓ} {n}
+    → ⦃ Connected A n ⦄
+    → Connected (Lift ℓ' A) n
+  Connected-Lift {n = n} ⦃ conn-instance ac ⦄ = conn-instance
+    (is-n-connected-≃ n (Lift-≃ e⁻¹) ac)
 ```