defn: equivalences over (#398)

Defines "equivalences over", or displayed equivalences, along with three
examples:

- an adjunction is an equivalence iff being invertible is equivalent to
itself over the Hom-equivalence;
- being a symmetric monoidal monad is equivalent to being a symmetric
monad strength over the equivalence between monoidal monads and
commutative monads;
- being a concrete abelian group is equivalent to being an abelian group
over the equivalence between concrete groups and groups.

## Checklist

Before submitting a merge request, please check the items below:

- [X] I've read [the contributing
guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md).
- [X] The imports of new modules have been sorted with
`support/sort-imports.hs` (or `nix run --experimental-features
nix-command -f . sort-imports`).
- [X] All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content,
and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title
with `chore:`.

Author: ncfavier

src/1Lab/Equiv/Fibrewise.lagda.md

@@ -1,11 +1,14 @@
 ---
 description: |
   We establish a correspondence between "fibrewise equivalences" and
-  equivalences of total spaces (Σ-types).
+  equivalences of total spaces (Σ-types), and define equivalences over.
 ---
 <!--
 ```agda
+open import 1Lab.Equiv.FromPath
 open import 1Lab.HLevel.Closure
+open import 1Lab.Type.Sigma
+open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
@@ -91,3 +94,62 @@ equiv→total always-eqv .is-eqv y =
     (total-fibres .snd)
     (always-eqv .is-eqv (y .snd))
 ```
+
+## Equivalences over {defines="equivalence-over"}
+
+We can generalise the notion of fibrewise equivalence to families
+$P : A \to \ty$, $Q : B \to \ty$ over *different* base types,
+provided we have an equivalence $e : A \simeq B$. In that case, we
+say that $P$ and $Q$ are **equivalent over** $e$ if $P(a) \simeq Q(b)$
+whenever $a : A$ and $b : B$ are identified [[over|path over]] $e$.
+
+Using univalence, we can see this as a special case of [[dependent paths]],
+where the base type is taken to be the universe and the type family sends
+a type $A$ to the type of type families over $A$. However, the
+following explicit definition is easier to work with.
+
+<!--
+```agda
+module _ {ℓa ℓb} {A : Type ℓa} {B : Type ℓb} where
+```
+-->
+
+```agda
+  _≃[_]_ : ∀ {ℓp ℓq} (P : A → Type ℓp) (e : A ≃ B) (Q : B → Type ℓq) → Type _
+  P ≃[ e ] Q = ∀ (a : A) (b : B) → e .fst a ≡ b → P a ≃ Q b
+```
+
+While this definition is convenient to *use*, we provide helpers that
+make it easier to *build* equivalences over.
+
+<!--
+```agda
+  module _ {ℓp ℓq} {P : A → Type ℓp} {Q : B → Type ℓq} (e : A ≃ B) where
+    private module e = Equiv e
+```
+-->
+
+```agda
+    over-left→over : (∀ (a : A) → P a ≃ Q (e.to a)) → P ≃[ e ] Q
+    over-left→over e' a b p = e' a ∙e line→equiv (λ i → Q (p i))
+
+    over-right→over : (∀ (b : B) → P (e.from b) ≃ Q b) → P ≃[ e ] Q
+    over-right→over e' a b p = line→equiv (λ i → P (e.adjunctl p i)) ∙e e' b
+
+    prop-over-ext
+      : (∀ {a} → is-prop (P a))
+      → (∀ {b} → is-prop (Q b))
+      → (∀ (a : A) → P a → Q (e.to a))
+      → (∀ (b : B) → Q b → P (e.from b))
+      → P ≃[ e ] Q
+    prop-over-ext propP propQ P→Q Q→P a b p = prop-ext propP propQ
+      (subst Q p ∘ P→Q a)
+      (subst P (sym (e.adjunctl p)) ∘ Q→P b)
+```
+
+An equivalence over $e$ induces an equivalence of total spaces:
+
+```agda
+    over→total : P ≃[ e ] Q → Σ A P ≃ Σ B Q
+    over→total e' = Σ-ap e λ a → e' a (e.to a) refl
+```

src/1Lab/Path.lagda.md

@@ -165,7 +165,7 @@ module _ {ℓ} {A : Type ℓ} {a b : A} {p : a ≡ b} where private
   right-endpoint = refl
 ```
 
-## Dependent paths
+## Dependent paths {defines="dependent-path path-over"}
 
 Since we're working in dependent type theory, a sensible question to ask
 is whether we can extend the idea that paths are functions $\bI \to A$

src/1Lab/Prelude.agda

@@ -33,7 +33,9 @@ open import 1Lab.Equiv.HalfAdjoint public
 open import 1Lab.Function.Surjection public
 
 open import 1Lab.Univalence public
-open import 1Lab.Univalence.SIP public
+open import 1Lab.Univalence.SIP
+  renaming (_≃[_]_ to _≃[_]s_)
+  public
 
 open import 1Lab.Type.Pi public
 open import 1Lab.Type.Sigma public

src/1Lab/Reflection/HLevel.agda

@@ -2,6 +2,7 @@ open import 1Lab.Reflection.Signature
 open import 1Lab.Function.Embedding
 open import 1Lab.Reflection.Record
 open import 1Lab.Reflection.Subst
+open import 1Lab.Equiv.Fibrewise
 open import 1Lab.HLevel.Universe
 open import 1Lab.HLevel.Closure
 open import 1Lab.Reflection
@@ -235,6 +236,7 @@ private module _ {ℓ} {A : n-Type ℓ 2} {B : ∣ A ∣ → n-Type ℓ 3} where
 private variable
   ℓ ℓ' : Level
   A B C : Type ℓ
+  P Q : A → Type ℓ
 
 {-
 In addition to the top-level 'hlevel' entry point, there are quite a few
@@ -259,6 +261,15 @@ prop-ext!
   → A ≃ B
 prop-ext! = prop-ext (hlevel 1) (hlevel 1)
 
+prop-over-ext!
+  : (e : A ≃ B) (let module e = Equiv e)
+  → ⦃ ∀ {a} → H-Level (P a) 1 ⦄
+  → ⦃ ∀ {b} → H-Level (Q b) 1 ⦄
+  → (∀ (a : A) → P a → Q (e.to a))
+  → (∀ (b : B) → Q b → P (e.from b))
+  → P ≃[ e ] Q
+prop-over-ext! e = prop-over-ext e (hlevel 1) (hlevel 1)
+
 Σ-prop-path!
   : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
   → ⦃ bxprop : ∀ {x} → H-Level (B x) 1 ⦄

src/Algebra/Group/Ab.lagda.md

@@ -38,6 +38,9 @@ private variable
 
 Group-on-is-abelian : Group-on G → Type _
 Group-on-is-abelian G = ∀ x y → Group-on._⋆_ G x y ≡ Group-on._⋆_ G y x
+
+Group-on-is-abelian-is-prop : (g : Group-on G) → is-prop (Group-on-is-abelian g)
+Group-on-is-abelian-is-prop g = Π-is-hlevel² 1 λ _ _ → g .Group-on.has-is-set _ _
 ```
 -->
 
@@ -60,7 +63,7 @@ instance
   H-Level-is-abelian-group
     : ∀ {n} {* : G → G → G} → H-Level (is-abelian-group *) (suc n)
   H-Level-is-abelian-group = prop-instance $ Iso→is-hlevel 1 eqv $
-    Σ-is-hlevel 1 (hlevel 1) λ x → Π-is-hlevel' 1 λ _ → Π-is-hlevel' 1 λ _ →
+    Σ-is-hlevel 1 (hlevel 1) λ x → Π-is-hlevel²' 1 λ _ _ →
       is-group.has-is-set x _ _
 ```
 -->

src/Algebra/Group/Concrete.lagda.md

@@ -120,7 +120,7 @@ opaque
 S¹-concrete : ConcreteGroup lzero
 S¹-concrete .B = S¹∙
 S¹-concrete .has-is-connected = S¹-is-connected
-S¹-concrete .has-is-groupoid = hlevel 3
+S¹-concrete .has-is-groupoid = S¹-is-groupoid
 ```
 
 ## The category of concrete groups
@@ -409,7 +409,7 @@ need to bend the path into a `Square`{.Agda}:
   linv = funext∙ g≡f ptg≡ptf
 ```
 
-*Phew*. At last, `π₁F`{.Agda} is fully faithful.
+At last, `π₁F`{.Agda} is fully faithful.
 
 ```agda
 π₁F-is-ff : is-fully-faithful (π₁F {ℓ})
@@ -428,11 +428,11 @@ this lets us conclude with the desired equivalence.
   (λ {G} {H} → π₁F-is-ff {_} {G} {H})
   π₁F-is-split-eso
 
-π₁B-is-equiv : is-equiv (π₁B {ℓ})
-π₁B-is-equiv = is-cat-equivalence→equiv-on-objects
+Concrete≃Abstract : ConcreteGroup ℓ ≃ Group ℓ
+Concrete≃Abstract = _ , is-cat-equivalence→equiv-on-objects
   ConcreteGroups-is-category
   Groups-is-category
   π₁F-is-equivalence
 
-module Concrete≃Abstract {ℓ} = Equiv (_ , π₁B-is-equiv {ℓ})
+module Concrete≃Abstract {ℓ} = Equiv (Concrete≃Abstract {ℓ})
 ```

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

@@ -59,30 +59,27 @@ that has equal opposite sides.
     x
 ```
 
-Still unsurprisingly, the delooping of an abelian group is abelian.
+Still unsurprisingly, the properties of being a concrete abelian group
+and being an abelian group are [[equivalent over|equivalence over]]
+the equivalence between concrete and abstract groups.
 
 ```agda
-Deloop-abelian
-  : ∀ {ℓ} {G : Group ℓ}
-  → is-commutative-group G → is-concrete-abelian (Concrete G)
-Deloop-abelian G-ab = ∙-comm _ G-ab
+abelian≃abelian
+  : ∀ {ℓ}
+  → is-concrete-abelian ≃[ Concrete≃Abstract {ℓ} ] is-commutative-group
+abelian≃abelian = prop-over-ext Concrete≃Abstract
+  (λ {G} → is-concrete-abelian-is-prop G)
+  (λ {G} → Group-on-is-abelian-is-prop (G .snd))
+  (λ G G-ab → G-ab)
+  (λ G G-ab → ∙-comm _ G-ab)
 ```
 
-The circle is another example, being the delooping of $\mathbb{Z}$.
+For example, the circle is abelian, being the delooping of $\mathbb{Z}$.
 
 ```agda
-π₁-abelian→abelian
-  : ∀ {ℓ} {G : ConcreteGroup ℓ}
-  → is-commutative-group (π₁B G) → is-concrete-abelian G
-π₁-abelian→abelian {G = G} π₁G-ab = subst is-concrete-abelian
-  (Concrete≃Abstract.η G)
-  (Deloop-abelian π₁G-ab)
-
 S¹-concrete-abelian : is-concrete-abelian S¹-concrete
-S¹-concrete-abelian = π₁-abelian→abelian {G = S¹-concrete}
-  (subst is-commutative-group
-    (sym π₁S¹≡ℤ)
-    (Abelian→Group-on-abelian (ℤ-ab .snd)))
+S¹-concrete-abelian = Equiv.from (abelian≃abelian S¹-concrete ℤ π₁S¹≡ℤ)
+  (Abelian→Group-on-abelian (ℤ-ab .snd))
 ```
 
 ## First abelian group cohomology
@@ -228,6 +225,8 @@ module _ {ℓ}
     : H¹[ Concrete G , Concrete H ] ≃ Hom (Groups ℓ) G H
   first-abelian-group-cohomology =
     first-concrete-abelian-group-cohomology
-      (Concrete G) (Concrete H) (Deloop-abelian H-ab) e⁻¹
+      (Concrete G) (Concrete H)
+      (Equiv.from (abelian≃abelian (Concrete H) H (Concrete≃Abstract.ε H)) H-ab)
+      e⁻¹
     ∙e Deloop-hom-equiv
 ```

src/Cat/Functor/Adjoint.lagda.md

@@ -220,6 +220,9 @@ $\hom(La,b) \cong \hom(a,Rb)$.
   R-adjunct-is-equiv : ∀ {a b} → is-equiv (R-adjunct {a} {b})
   R-adjunct-is-equiv = is-iso→is-equiv
     (iso L-adjunct R-L-adjunct L-R-adjunct)
+
+  adjunct-hom-equiv : ∀ {a b} → D.Hom (L.₀ a) b ≃ C.Hom a (R.₀ b)
+  adjunct-hom-equiv = L-adjunct , L-adjunct-is-equiv
 ```
 
 <!--

src/Cat/Functor/Adjoint/Hom.lagda.md

@@ -182,7 +182,7 @@ module _ {o ℓ o'} {C : Precategory o ℓ} {D : Precategory o' ℓ}
     module R = Func R
 
     hom-equiv : ∀ {a b} → C.Hom (L.₀ a) b ≃ D.Hom a (R.₀ b)
-    hom-equiv = _ , L-adjunct-is-equiv adj
+    hom-equiv = adjunct-hom-equiv adj
 
   adjunct-hom-iso-from
     : ∀ a → Hom-from C (L.₀ a) ≅ⁿ Hom-from D a F∘ R

src/Cat/Functor/Equivalence.lagda.md

@@ -562,19 +562,6 @@ open is-equivalence
 open Precategory
 open _⊣_
 
-Id-is-equivalence : ∀ {o h} {C : Precategory o h} → is-equivalence {C = C} Id
-Id-is-equivalence {C = C} .F⁻¹ = Id
-Id-is-equivalence {C = C} .F⊣F⁻¹ .unit .η x = C .id
-Id-is-equivalence {C = C} .F⊣F⁻¹ .unit .is-natural x y f = C .idl _ ∙ sym (C .idr _)
-Id-is-equivalence {C = C} .F⊣F⁻¹ .counit .η x = C .id
-Id-is-equivalence {C = C} .F⊣F⁻¹ .counit .is-natural x y f = C .idl _ ∙ sym (C .idr _)
-Id-is-equivalence {C = C} .F⊣F⁻¹ .zig = C .idl _
-Id-is-equivalence {C = C} .F⊣F⁻¹ .zag = C .idl _
-Id-is-equivalence {C = C} .unit-iso x =
-  Cat.Reasoning.make-invertible C (C .id) (C .idl _) (C .idl _)
-Id-is-equivalence {C = C} .counit-iso x =
-  Cat.Reasoning.make-invertible C (C .id) (C .idl _) (C .idl _)
-
 unquoteDecl H-Level-is-precat-iso = declare-record-hlevel 1 H-Level-is-precat-iso (quote is-precat-iso)
 
 module
@@ -831,3 +818,93 @@ _∘Equivalence_ : Equivalence C D → Equivalence D E → Equivalence C E
 (F ∘Equivalence G) .Equivalence.To-equiv =
   is-equivalence-∘ (Equivalence.To-equiv G) (Equivalence.To-equiv F)
 ```
+
+Unsurprisingly, the identity functor is an equivalence.
+
+```agda
+Id-is-equivalence : ∀ {o h} {C : Precategory o h} → is-equivalence {C = C} Id
+Id-is-equivalence {C = C} .F⁻¹ = Id
+Id-is-equivalence {C = C} .F⊣F⁻¹ .unit .η x = C .id
+Id-is-equivalence {C = C} .F⊣F⁻¹ .unit .is-natural x y f = C .idl _ ∙ sym (C .idr _)
+Id-is-equivalence {C = C} .F⊣F⁻¹ .counit .η x = C .id
+Id-is-equivalence {C = C} .F⊣F⁻¹ .counit .is-natural x y f = C .idl _ ∙ sym (C .idr _)
+Id-is-equivalence {C = C} .F⊣F⁻¹ .zig = C .idl _
+Id-is-equivalence {C = C} .F⊣F⁻¹ .zag = C .idl _
+Id-is-equivalence {C = C} .unit-iso x =
+  Cat.Reasoning.make-invertible C (C .id) (C .idl _) (C .idl _)
+Id-is-equivalence {C = C} .counit-iso x =
+  Cat.Reasoning.make-invertible C (C .id) (C .idl _) (C .idl _)
+```
+
+### Preserving invertibility
+
+We can characterise equivalences as those adjunctions $L \vdash R$ that
+*preserve invertibility*, in the sense that the adjunct of an isomorphism
+$L(a) \cong b$ is an isomorphism $a \cong R(b)$ and vice versa;
+that is, the property of being invertible in $\cC$ is equivalent to
+the property of being invertible in $\cD$ [[over|equivalence over]]
+the adjunction's $\hom$-equivalence $(L(a) \to b) \simeq (a \to R(b))$.
+
+<!--
+```agda
+module
+  _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
+    {L : Functor C D} {R : Functor D C} (L⊣R : L ⊣ R)
+  where
+  private
+    module C = Cat.Reasoning C
+    module D = Cat.Reasoning D
+    module L = Fr L
+    module R = Fr R
+```
+-->
+
+```agda
+  preserves-invertibility : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ')
+  preserves-invertibility = ∀ {a b} →
+    D.is-invertible ≃[ adjunct-hom-equiv L⊣R {a} {b} ] C.is-invertible
+```
+
+Since the unit and counit of an adjunction are adjuncts of identities,
+it's not hard to see that they must be invertible if the adjunction
+preserves invertibility.
+
+```agda
+  preserves-invertibility→equivalence
+    : preserves-invertibility → is-equivalence L
+  preserves-invertibility→equivalence e .F⁻¹ = R
+  preserves-invertibility→equivalence e .F⊣F⁻¹ = L⊣R
+  preserves-invertibility→equivalence e .unit-iso c = C.invertible-cancelr
+    (R.F-map-invertible D.id-invertible)
+    (Equiv.to (e D.id _ refl) D.id-invertible)
+  preserves-invertibility→equivalence e .counit-iso d = D.invertible-cancell
+    (L.F-map-invertible C.id-invertible)
+    (Equiv.from (e _ _ (L-R-adjunct L⊣R _)) C.id-invertible)
+```
+
+The other direction is just as straightforward, since adjuncts are
+defined by composition with the (co)unit, and isomorphisms compose.
+
+<!--
+```agda
+module
+  _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
+    (F : Functor C D) (eqv : is-equivalence F)
+  where
+  private
+    module e = is-equivalence eqv
+    module C = Cat.Reasoning C
+    module D = Cat.Reasoning D
+    module F = Fr F
+    module F⁻¹ = Fr e.F⁻¹
+```
+-->
+
+```agda
+  equivalence→preserves-invertibility : preserves-invertibility e.F⊣F⁻¹
+  equivalence→preserves-invertibility = prop-over-ext
+    (adjunct-hom-equiv e.F⊣F⁻¹)
+    (hlevel 1) (hlevel 1)
+    (λ f inv → C.invertible-∘ (F⁻¹.F-map-invertible inv) (e.unit-iso _))
+    (λ f inv → D.invertible-∘ (e.counit-iso _) (F.F-map-invertible inv))
+```