Comonoids, duality, and related displayed tech

src/1Lab/Equiv.lagda.md

@@ -418,6 +418,29 @@ equiv→zag {f = f} eqv b =
 
 </details>
 
+We also show that the inverse of an equivalence is itself an 
+equivalence:
+
+```agda
+inverse-is-equiv : {f : A → B} (eqv : is-equiv f) → is-equiv (equiv→inverse eqv)
+inverse-is-equiv {f = f} eqv .is-eqv x .centre = record
+  { fst = f x ; snd = equiv→unit eqv x }
+inverse-is-equiv {A = A} {B = B} {f = f} eqv .is-eqv x .paths (y , p) = q where
+  g = equiv→inverse eqv
+  η = equiv→unit eqv
+  ε = equiv→counit eqv
+  zag = equiv→zag eqv
+
+  q : (f x , η x) ≡ (y , p)
+  q i .fst = (ap f (sym p) ∙ ε y) i
+  q i .snd j = hcomp (∂ i ∨ ∂ j) λ where
+    k (k = i0) → zag y j i
+    k (i = i0) → η (p k) (j ∧ k)
+    k (i = i1) → p (k ∧ j)
+    k (j = i0) → g (∙-filler' (ap f (sym p)) (ε y) k i)
+    k (j = i1) → η (p k) (i ∨ k)
+```
+
 Finally, it'll be convenient for us to package some of the theorems
 above into a proof that every equivalence is an isomorphism:
 
@@ -718,26 +741,10 @@ Iso→Equiv : Iso A B → A ≃ B
 Iso→Equiv (f , is-iso) = record { fst = f ; snd = is-iso→is-equiv is-iso }
 ```
 
-<!--
-```agda
-inverse-is-equiv : {f : A → B} (eqv : is-equiv f) → is-equiv (equiv→inverse eqv)
-inverse-is-equiv {f = f} eqv .is-eqv x .centre = record
-  { fst = f x ; snd = equiv→unit eqv x }
-inverse-is-equiv {A = A} {B = B} {f = f} eqv .is-eqv x .paths (y , p) = q where
-  g = equiv→inverse eqv
-  η = equiv→unit eqv
-  ε = equiv→counit eqv
-  zag = equiv→zag eqv
-
-  q : (f x , η x) ≡ (y , p)
-  q i .fst = (ap f (sym p) ∙ ε y) i
-  q i .snd j = hcomp (∂ i ∨ ∂ j) λ where
-    k (k = i0) → zag y j i
-    k (i = i0) → η (p k) (j ∧ k)
-    k (i = i1) → p (k ∧ j)
-    k (j = i0) → g (∙-filler' (ap f (sym p)) (ε y) k i)
-    k (j = i1) → η (p k) (i ∨ k)
+Finally, we provide two helper modules packaging useful data associated
+to equivalences and isomorphisms.
 
+```agda
 module Equiv {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A ≃ B) where
   to   = f .fst
   from = equiv→inverse (f .snd)
@@ -781,7 +788,10 @@ module Iso {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ((f , f-iso) : Iso A B) whe
 
   inverse : Iso B A
   inverse = from , inverse-iso
+```
 
+<!--
+```agda
 injectiveP
   : ∀ {ℓ ℓ'} {A : I → Type ℓ} {B : I → Type ℓ'} (f : ∀ i → Iso (A i) (B i)) {x y}
   → PathP (λ i → B i) (f i0 .fst x) (f i1 .fst y)

src/1Lab/Function/Embedding.lagda.md

@@ -35,7 +35,7 @@ private variable
 ```
 -->
 
-# Embeddings {defines="embedding"}
+# Embeddings {defines="embedding injective"}
 
 One of the most important observations leading to the development of
 categorical set theory is that injective maps _into_ a set $S$

src/1Lab/Path.lagda.md

@@ -1279,13 +1279,16 @@ partial element.
 ~~~
 
 Diagramatically, we'll depict extensions by drawing the relevant partial
-element in red, and the total element in black. In Agda, we write
+element in red, and the total element in black.[^dark] In Agda, we write
 extension types using the type former `_[_↦_]`{.Agda}, which is written
 mixfix as `A [ φ ↦ p ]`. We can formalise the red-black extensibility
 diagram above by defining the partial element `left-true`{.Agda}, and
 giving `refl`{.Agda} to `inS`{.Agda}, the constructor for
 `_[_↦_]`{.Agda}.
 
+[^dark]:
+    Or white, if you are using dark mode.
+
 ```agda
 private
   left-true : (i : I) → Partial (~ i) Bool

src/Cat/Base.lagda.md

@@ -181,20 +181,10 @@ opposite precategory $C\op$. What we have to show is - by the type of
 \circ_{op} h$. This computes into $(h \circ g) \circ f = h \circ (g
 \circ f)$ - which is exactly what `sym (assoc C h g f)` shows!
 
-```agda
-C^op^op≡C : ∀ {o ℓ} {C : Precategory o ℓ} → C ^op ^op ≡ C
-C^op^op≡C {C = C} i = precat i where
-  open Precategory
-  precat : C ^op ^op ≡ C
-  precat i .Ob = C .Ob
-  precat i .Hom = C .Hom
-  precat i .Hom-set = C .Hom-set
-  precat i .id = C .id
-  precat i ._∘_ = C ._∘_
-  precat i .idr = C .idr
-  precat i .idl = C .idl
-  precat i .assoc = C .assoc
-```
+For `_^op`{.Agda} to form a good basis for duality, it is important that
+the operation be _involutive_. This, and other aspects of duality of
+categories, is shown under [[duality of precategories]].
+
 
 ## The precategory of Sets {defines="category-of-sets"}
 
@@ -478,10 +468,10 @@ Natural transformations also dualise. The opposite of $\eta : F
     }
 ```
 
-<!--
+<details>
+<summary>We can also define `is-natural-transformation`{.Agda} as a 
+property of families of morphisms.</summary>
 ```agda
-{-# INLINE NT #-}
-
 is-natural-transformation
   : ∀ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
   → (F G : Functor C D)
@@ -491,6 +481,12 @@ is-natural-transformation {C = C} {D = D} F G η =
   ∀ x y (f : C .Precategory.Hom x y) → η y D.∘ F .F₁ f ≡ G .F₁ f D.∘ η x
   where module D = Precategory D
         open Functor
+```
+</details>
+
+<!--
+```agda
+{-# INLINE NT #-}
 
 infixr 30 _F∘_
 infix 20 _=>_

src/Cat/Bi/Instances/Displayed.lagda.md

@@ -114,8 +114,8 @@ as in the nondisplayed case.
       module C' {x} = Cat (Fibre C x)
 
       ni : make-natural-iso {D = Vf _ _} _ _
-      ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → D.to-pathp[] D.id-comm[] }
-      ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → D.to-pathp[] D.id-comm[] }
+      ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → D.to-pathp[] D.id-comm-sym[] }
+      ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → D.to-pathp[] D.id-comm-sym[] }
       ni .eta∘inv _ = ext λ _ → D'.idl _
       ni .inv∘eta _ = ext λ _ → D'.idl _
       ni .natural x y f = ext λ _ →
@@ -140,8 +140,8 @@ the structural isomorphisms being identities.
   Disp[] .unitor-l {B = B} = to-natural-iso ni where
     module B = Disp B
     ni : make-natural-iso {D = Vf _ _} _ _
-    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm[] }
-    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm[] }
+    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm-sym[] }
+    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm-sym[] }
     ni .eta∘inv _ = ext λ _ → Cat.idl (Fibre B _) _
     ni .inv∘eta _ = ext λ _ → Cat.idl (Fibre B _) _
     ni .natural x y f = ext λ _ → Cat.elimr (Fibre B _) refl ∙ Cat.id-comm (Fibre B _)
@@ -150,8 +150,8 @@ the structural isomorphisms being identities.
     module B' {x} = Cat (Fibre B x) using (_∘_ ; idl ; elimr)
 
     ni : make-natural-iso {D = Vf _ _} _ _
-    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm[] }
-    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm[] }
+    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm-sym[] }
+    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm-sym[] }
     ni .eta∘inv _ = ext λ _ → B'.idl _
     ni .inv∘eta _ = ext λ _ → B'.idl _
     ni .natural x y f = ext λ _ → B'.elimr refl ∙ ap₂ B'._∘_ (y .F-id') refl

src/Cat/Displayed/Base.lagda.md

@@ -16,15 +16,15 @@ open import Cat.Base
 module Cat.Displayed.Base where
 ```
 
-# Displayed categories {defines=displayed-category}
+# Displayed categories {defines="displayed-category base-category displayed-precategory"}
 
 The core idea behind displayed categories is that we want to capture the
 idea of being able to place extra structure over some sort of "base"
 category. For instance, we can think of categories of algebraic objects
 (monoids, groups, rings, etc) as being extra structure placed atop the
 objects of Set, and extra conditions placed atop the morphisms of Set.
 
-We start by defining a displayed category over a base category $\cB$
+We start by defining a displayed category over a **base category** $\cB$
 which will act as the category we add the extra structure to.
 
 ```agda

src/Cat/Displayed/Cartesian/Discrete.lagda.md

@@ -5,6 +5,7 @@ description: |
 ---
 <!--
 ```agda
+open import Cat.Displayed.Functor.Equivalence
 open import Cat.Displayed.Instances.Elements
 open import Cat.Displayed.Cartesian
 open import Cat.Displayed.Functor
@@ -432,7 +433,7 @@ is immediate.
 
 ```agda
     ∫≡dx : ∫ B (discrete→presheaf P p-disc) ≡ P
-    ∫≡dx = Displayed-path pieces (λ _ → id-equiv) (is-iso→is-equiv p) where
+    ∫≡dx = Displayed-path pieces $ iso[] (is-iso→is-equiv p) (λ _ → id-equiv) where
       p : ∀ {a b} {f : B.Hom a b} {a'} {b'} → is-iso (pieces .F₁' {f = f} {a'} {b'})
       p .from f = ap fst $ cart-lift _ _ .paths (_ , f)
       p .rinv p = from-pathp (ap snd (cart-lift _ _ .paths _))

src/Cat/Displayed/Cocartesian/Discrete.lagda.md

@@ -9,7 +9,6 @@ open import Cat.Displayed.Functor
 open import Cat.Instances.Functor
 open import Cat.Displayed.Fibre
 open import Cat.Displayed.Base
-open import Cat.Displayed.Path
 open import Cat.Prelude
 
 import Cat.Displayed.Reasoning