Univalent groupoids

src/1Lab/Equiv.lagda.md

@@ -1076,6 +1076,8 @@ instructive exercise to work these out for yourself!</summary>
 ```agda
 _ : ∘-closed is-equiv
 _ = ∘-is-equiv
+
+private module _ where private
 ```
 -->
 
@@ -1085,18 +1087,62 @@ Specialising these, any left- or right- inverse of an equivalence must
 be homotopic to the specified one, so that *it too* is an equivalence.
 
 ```agda
+  left-inverse→equiv
+    : {f : A → B} {g : B → A}
+    → is-left-inverse g f → is-equiv f → is-equiv g
+  left-inverse→equiv linv ef = equiv-cancelr ef
+    (subst is-equiv (sym (funext linv)) id-equiv)
+
+  right-inverse→equiv
+    : {f : A → B} {g : B → A}
+    → is-right-inverse g f → is-equiv f → is-equiv g
+  right-inverse→equiv rinv ef = equiv-cancell ef
+    (subst is-equiv (sym (funext rinv)) id-equiv)
+```
+
+<!--
+```agda
+-- The inverse maps produces by the previous proofs have transports
+-- introduced via the 'subst', so we provide specialized forms that
+-- do not involve transports.
+
+subst-is-equiv
+  : ∀ {f g : A → B}
+  → g ≡ f
+  → is-equiv f
+  → is-equiv g
+{-# INLINE subst-is-equiv #-}
+subst-is-equiv {f = f} {g = g} p f-eqv = record
+  { is-eqv = λ b → contr (f.from b , happly p (f.from b) ∙ f.ε b) λ fib i →
+      comp (λ j → fibre (p (~ j ∧ ~ i)) b) (∂ i) λ where
+        j (i = i0) → f.from b , ∙-filler' (happly p (f.from b)) (f.ε b) j
+        j (i = i1) → fib
+        j (j = i0) → fibre-line b fib i
+  }
+  where
+    module f = Equiv (_ , f-eqv)
+
+    fibre-line
+      : ∀ b (fib : fibre g b)
+      → PathP (λ i → fibre (p (~ i)) b) (f-eqv .is-eqv b .centre) fib
+    fibre-line b fib i = comp (λ j → fibre (p (~ i ∨ ~ j)) b) (∂ i) λ where
+      j (i = i0) → f-eqv .is-eqv b .centre
+      j (i = i1) → coe1→i (λ i → fibre (p (~ i)) b) j fib
+      j (j = i0) → f-eqv .is-eqv b .paths (coe1→0 (λ i → fibre (p (~ i)) b) fib) i
+
 left-inverse→equiv
   : {f : A → B} {g : B → A}
   → is-left-inverse g f → is-equiv f → is-equiv g
-left-inverse→equiv linv ef = equiv-cancelr ef
-  (subst is-equiv (sym (funext linv)) id-equiv)
+left-inverse→equiv linv ef =
+  equiv-cancelr ef (subst-is-equiv (funext linv) id-equiv)
 
 right-inverse→equiv
   : {f : A → B} {g : B → A}
   → is-right-inverse g f → is-equiv f → is-equiv g
-right-inverse→equiv rinv ef = equiv-cancell ef
-  (subst is-equiv (sym (funext rinv)) id-equiv)
+right-inverse→equiv rinv eg =
+  equiv-cancell eg (subst-is-equiv (funext rinv) id-equiv)
 ```
+-->
 
 ### Equivalence reasoning
 
@@ -1245,6 +1291,15 @@ is-equiv-join : (f : A → B) → (B → is-equiv f) → is-equiv f
 {-# INLINE is-equiv-join #-}
 is-equiv-join f fe = record { is-eqv = λ y → fe y .is-eqv y }
 
+Subtype-proj-is-equiv
+  : ∀ {ℓa} {A : Type ℓa} {B : A → Type ℓ}
+  → (∀ x → is-prop (B x))
+  → (∀ x → B x)
+  → is-equiv {A = Σ A B} fst
+Subtype-proj-is-equiv B-prop Bx .is-eqv a .centre = (a , Bx a) , refl
+Subtype-proj-is-equiv B-prop Bx .is-eqv a .paths ((a' , b') , p) i .fst = p (~ i) , is-prop→pathp (λ i → B-prop (p (~ i))) (Bx a) b' i
+Subtype-proj-is-equiv B-prop Bx .is-eqv a .paths ((a' , b') , p) i .snd j = p (~ i ∨ j)
+
 module _ {ℓ} {A : Type ℓ} {x y : A} {p q : x ≡ y} where
   ∨-square≃ : (p ≡ q) ≃ Square p q refl refl
   ∨-square≃ .fst = ∨-square

src/1Lab/Path/IdentitySystem.lagda.md

@@ -473,3 +473,19 @@ opaque
     (¬¬-stable-identity-system dec→dne)
     λ x y f g → funext λ h → absurd (g h)
 ```
+
+<!--
+```agda
+×-identity-system
+  : ∀ {ℓa ℓb ℓr ℓs} {A : Type ℓa} {B : Type ℓb}
+  → {R : A → A → Type ℓr} {S : B → B → Type ℓs}
+  → {r : ∀ a → R a a} {s : ∀ b → S b b}
+  → is-identity-system R r
+  → is-identity-system S s
+  → is-identity-system
+      (λ ab ab' → R (ab .fst) (ab' .fst) × S (ab .snd) (ab' .snd))
+      (λ ab → r (ab .fst) , s (snd ab))
+×-identity-system R-ids S-ids .to-path (r' , s') = R-ids .to-path r' ,ₚ S-ids .to-path s'
+×-identity-system R-ids S-ids .to-path-over (r' , s') = R-ids .to-path-over r' ,ₚ S-ids .to-path-over s'
+```
+-->

src/Cat/Functor/WideSubcategory.lagda.md

@@ -88,6 +88,8 @@ module _ {o h} {C : Precategory o h} where
   Wide-hom-path {sub = sub} {f = f} {g = g} p i .witness =
     is-prop→pathp (λ i → sub .P-prop (p i)) (f .witness) (g .witness) i
 
+  unquoteDecl Wide-hom-iso-Σ = declare-record-iso Wide-hom-iso-Σ (quote Wide-hom)
+
   instance
     Extensional-wide-hom
       : ∀ {ℓ ℓr} {sub : Wide-subcat C ℓ} {x y : C.Ob}
@@ -98,9 +100,15 @@ module _ {o h} {C : Precategory o h} where
     H-Level-Wide-hom
       : ∀ {sub : Wide-subcat C ℓ} {x y : C.Ob} {n}
       → H-Level (Wide-hom sub x y) (2 + n)
-    H-Level-Wide-hom {sub = sub} = basic-instance 2 $ Iso→is-hlevel 2 eqv $
+    H-Level-Wide-hom {sub = sub} = basic-instance 2 $ Iso→is-hlevel 2 Wide-hom-iso-Σ $
       Σ-is-hlevel 2 (C.Hom-set _ _) λ f → is-hlevel-suc 1 (sub .P-prop f)
-      where unquoteDecl eqv = declare-record-iso eqv (quote Wide-hom)
+
+  Wide-hom≃witness
+    : {sub : Wide-subcat C ℓ}
+    → {x y : C.Ob}
+    → Wide-hom sub x y
+    ≃ (Σ[ f ∈ C.Hom x y ] f ∈ sub)
+  Wide-hom≃witness = Iso→Equiv Wide-hom-iso-Σ
 ```
 -->
 

src/Cat/Groupoid.lagda.md

@@ -23,20 +23,113 @@ is-pregroupoid C = ∀ {x y} (f : Hom x y) → is-invertible f
 ```
 
 <!--
+```agda
+module _ {o ℓ} (C : Precategory o ℓ) (gpd : is-pregroupoid C) where
+```
+-->
+
+Of course, the [[opposite]] of a groupoid is a groupoid.
+
+```agda
+  ^op-pregroupoid : is-pregroupoid (C ^op)
+  ^op-pregroupoid f = invertible→co-invertible C (gpd f)
+```
+
+If $\cC$ is a pregroupoid, then the map $x \iso y \to \cC(x,y)$ that
+forgets the inverse is an [[equivalence]].
+
 ```agda
 module is-pregroupoid {o ℓ} (C : Precategory o ℓ) (gpd : is-pregroupoid C) where
   open Cat.Reasoning C
 
+  forget-iso-is-equiv : ∀ {x y} → is-equiv (λ (f : x ≅ y) → f .to)
+```
+
+First, recall that being invertible is a [[property]] of morphisms.
+This means that the first projection  `Σ[ f ∈ Hom x y ] is-invertible f → Hom x y`
+must be an equivalence, as all of the fibres are prop-valued
+and inhabited. Moreover, the type of isomorphisms $x \iso y$ is equivalent
+to the above sigma type, so 2-out-of-3 for equivalences gives us our desired
+result.
+
+```agda
+  forget-iso-is-equiv {x} {y} =
+    equiv-cancelr
+      (inverse-is-equiv (iso≃is-invertible .snd))
+      proj-is-equiv
+    where
+      proj-is-equiv : is-equiv {A = Σ[ f ∈ Hom x y ] is-invertible f} fst
+      proj-is-equiv = Subtype-proj-is-equiv (λ _ → hlevel 1) gpd
+```
+
+<!--
+```agda
   hom→iso : ∀ {x y} → Hom x y → x ≅ y
   hom→iso f = invertible→iso f (gpd f)
 
-module _ {o ℓ} (C : Precategory o ℓ) (gpd : is-pregroupoid C) where
+  hom≃iso : ∀ {x y} → Hom x y ≃ (x ≅ y)
+  hom≃iso .fst = hom→iso
+  hom≃iso .snd = inverse-is-equiv forget-iso-is-equiv
 ```
 -->
 
-Of course, the [[opposite]] of a groupoid is a groupoid.
+## Univalent groupoids
+
+:::{.definition #univalent-groupoid}
+A precategory $\cC$ is a **univalent groupoid** or **groupoid** if
+the type of morphisms of $\cC$ forms an [[identity system]] on $\cC$.
+:::
+
 
 ```agda
-  ^op-pregroupoid : is-pregroupoid (C ^op)
-  ^op-pregroupoid f = invertible→co-invertible C (gpd f)
+is-univalent-groupoid : ∀ {o ℓ} → Precategory o ℓ → Type _
+is-univalent-groupoid C = is-identity-system Hom λ x → id {x}
+  where open Precategory C
+```
+
+As the name suggests, every univalent groupoid is both a [[univalent category]] and a pregroupoid.
+
+```agda
+module is-univalent-groupoid {o ℓ} (C : Precategory o ℓ) (C-gpd : is-univalent-groupoid C) where
+  open Cat.Reasoning C
+
+  univalent : is-category C
+  pregroupoid : is-pregroupoid C
+```
+
+We shall start by showing that $\cC$ is a pregroupoid. Let
+$f : \cC(x,y)$ be a morphism of $\cC$: our goal is to show
+that it is invertible. However, $\cC(x,y)$ is an identity
+system, so we can contract $f$ down to $\id$, which is obviously
+invertible!
+
+```agda
+  pregroupoid = IdsJ C-gpd (λ y f → is-invertible f) id-invertible
+```
+
+By our previous result, we now know that the type of morphisms $\cC(x,y)$ is
+equivalent to type of isomorphisms $x \iso y$. Moreover, this equivalence
+sends the identity morphism to the identity isomorphism. This means that
+we can prove that $\cC$ is univalent by transferring the identity system on
+morphisms along this equivalence.
+
+```agda
+  open is-pregroupoid C pregroupoid public
+
+  univalent = transfer-identity-system C-gpd (λ x y → hom≃iso) λ x → ext refl
+```
+
+We can use a similar argument to establish that every univalent pregroupoid
+is a univalent groupoid.
+
+```agda
+is-univalent-pregroupoid→is-univalent-groupoid
+  : ∀ {o ℓ} {C : Precategory o ℓ}
+  → is-category C
+  → is-pregroupoid C
+  → is-univalent-groupoid C
+is-univalent-pregroupoid→is-univalent-groupoid {C = C} C-cat C-gpd =
+  transfer-identity-system C-cat (λ x y → hom≃iso e⁻¹) λ _ → refl
+  where
+    open is-pregroupoid C C-gpd
 ```

src/Cat/Instances/Core.lagda.md

@@ -47,15 +47,40 @@ private module Core {o ℓ} (C : Precategory o ℓ) = Cat.Reasoning (Core C)
 ```
 -->
 
+<!--
 ```agda
-Core-is-groupoid : ∀ {o ℓ} {C : Precategory o ℓ} → is-pregroupoid (Core C)
-Core-is-groupoid {C = C} f =
-  Core.make-invertible _ (wide f-inv.inv ((f .witness) C.invertible⁻¹))
-    (Wide-hom-path f-inv.invl)
-    (Wide-hom-path f-inv.invr)
-  where
+module _ {o ℓ} {C : Precategory o ℓ} where
+  private
     module C = Cat.Reasoning C
-    module f-inv = C.is-invertible (f .witness)
+```
+-->
+
+```agda
+  Core-is-groupoid : is-pregroupoid (Core C)
+  Core-is-groupoid f =
+    Core.make-invertible _ (wide f-inv.inv ((f .witness) C.invertible⁻¹))
+      (Wide-hom-path f-inv.invl)
+      (Wide-hom-path f-inv.invr)
+    where
+      module f-inv = C.is-invertible (f .witness)
+```
+
+Note that isomorphisms in $\cC$ are equivalent to morphisms in the core
+of $\cC$. This means that if $\cC$ is [[univalent|univalent-category]],
+then we can transfer the associated identity system on isomorphisms to
+an identity system on morphisms of the core, and thus the core
+must be a [[univalent groupoid]].
+
+```agda
+  iso≃Core-hom : ∀ {x y} → (x C.≅ y) ≃ Core.Hom C x y
+  iso≃Core-hom {x} {y} =
+    x C.≅ y                              ≃⟨ C.iso≃is-invertible ⟩
+    Σ[ f ∈ C.Hom x y ] C.is-invertible f ≃˘⟨ Wide-hom≃witness ⟩
+    Core.Hom C x y                       ≃∎
+
+  Core-is-univalent-groupoid : is-category C → is-univalent-groupoid (Core C)
+  Core-is-univalent-groupoid C-cat =
+    transfer-identity-system C-cat (λ _ _ → iso≃Core-hom) λ _ → ext refl
 ```
 
 We have mentioned that the core is the _maximal_ sub-groupoid of $\cC$:

src/Cat/Instances/Discrete.lagda.md

@@ -76,6 +76,9 @@ Disc-is-category .to-path-over {a = a} is with is .to in w
 
 Disc-is-groupoid : ∀ {A : Type ℓ} {A-grpd} → is-pregroupoid (Disc A A-grpd)
 Disc-is-groupoid p = make-invertible _ (symᵢ p) (∙ᵢ-invl p) (∙ᵢ-invr p)
+
+Disc-is-univalent-groupoid : ∀ {A : Type ℓ} {A-grpd} → is-univalent-groupoid (Disc A A-grpd)
+Disc-is-univalent-groupoid = Id-identity-system
 ```
 
 <!--

src/Cat/Instances/Product.lagda.md

@@ -1,6 +1,7 @@
 <!--
 ```agda
 open import Cat.Functor.Base
+open import Cat.Groupoid
 open import Cat.Prelude
 
 import Cat.Reasoning
@@ -168,3 +169,15 @@ module
       Σ-pathp (Univalent.Hom-pathp-reflr-iso c-cat (C.idr _))
               (Univalent.Hom-pathp-reflr-iso d-cat (D.idr _))
 ```
+
+<!--
+```agda
+module _
+  {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
+  (c-gpd : is-univalent-groupoid C) (d-gpd : is-univalent-groupoid D)
+  where
+
+  ×ᶜ-is-univalent-groupoid : is-univalent-groupoid (C ×ᶜ D)
+  ×ᶜ-is-univalent-groupoid = ×-identity-system c-gpd d-gpd
+```
+-->

src/Cat/Instances/Shape/Initial.lagda.md

@@ -2,6 +2,7 @@
 ```agda
 open import 1Lab.Prelude
 
+open import Cat.Groupoid
 open import Cat.Base
 ```
 -->
@@ -45,3 +46,10 @@ module _ {o h} {A : Precategory o h} where
   ¡nt ._=>_.η ()
   ¡nt ._=>_.is-natural ()
 ```
+
+The initial category is a [[univalent groupoid]].
+
+```agda
+⊥Cat-is-univalent-groupoid : is-univalent-groupoid ⊥Cat
+⊥Cat-is-univalent-groupoid = set-identity-system absurd absurd
+```

src/Cat/Instances/Shape/Terminal.lagda.md

@@ -5,6 +5,7 @@ open import 1Lab.Prelude
 open import Cat.Functor.Naturality
 open import Cat.Functor.Compose
 open import Cat.Functor.Base
+open import Cat.Univalent
 open import Cat.Groupoid
 open import Cat.Morphism
 open import Cat.Base
@@ -41,12 +42,23 @@ trivial morphisms.
 ```
 
 The only morphism in the terminal category is the identity, so the
-terminal category is a [[pregroupoid]].
+terminal category is a [[univalent groupoid]].
 
+```agda
+⊤Cat-is-univalent-groupoid : is-univalent-groupoid ⊤Cat
+⊤Cat-is-univalent-groupoid = set-identity-system (λ _ _ → hlevel 1) (λ _ → refl)
+```
+
+<!--
 ```agda
 ⊤Cat-is-pregroupoid : is-pregroupoid ⊤Cat
 ⊤Cat-is-pregroupoid _ = id-invertible ⊤Cat
+
+⊤Cat-is-category : is-category ⊤Cat
+⊤Cat-is-category .to-path _ = refl
+⊤Cat-is-category .to-path-over _ = ≅-path ⊤Cat refl
 ```
+-->
 
 <!--
 ```agda