Sets is not self-dual (#314)

This PR contains a proof that `Sets` is not self-dual, which is placed
in the new `Cat/Instances/Sets/Counterxamples/` folder. To use in this
proof, it also defines strict initial objects, proves `Sets ^op` is a
category, and fixes a typo.

src/Cat/Diagram/Initial.lagda.md

@@ -79,13 +79,41 @@ Additionally, if $C$ is a category, then the space of initial objects is
 a proposition:
 
 ```agda
-⊥-contractible : is-category C → is-prop Initial
-⊥-contractible ccat x1 x2 i .bot =
+⊥-is-prop : is-category C → is-prop Initial
+⊥-is-prop ccat x1 x2 i .bot =
   Univalent.iso→path ccat (⊥-unique x1 x2) i
 
-⊥-contractible ccat x1 x2 i .has⊥ ob =
+⊥-is-prop ccat x1 x2 i .has⊥ ob =
   is-prop→pathp
     (λ i → is-contr-is-prop
       {A = Hom (Univalent.iso→path ccat (⊥-unique x1 x2) i) _})
     (x1 .has⊥ ob) (x2 .has⊥ ob) i
 ```
+
+## Strictness
+
+An initial object is said to be *[strict]* if every morphism into it is an *iso*morphism.
+This is a categorical generalization of the fact that if one can write a function $X \to \bot$ then $X$ must itself be empty.
+
+This is an instance of the more general notion of [van Kampen colimits].
+
+[strict]: https://ncatlab.org/nlab/show/strict+initial+object
+[van Kampen colimits]: https://ncatlab.org/nlab/show/van+Kampen+colimit
+
+
+```agda
+is-strict-initial : Initial → Type _
+is-strict-initial i = ∀ x → (f : Hom x (i .bot)) → is-invertible f
+
+record Strict-initial : Type (o ⊔ h) where
+  field
+    initial : Initial
+    has-is-strict : is-strict-initial initial
+```
+
+Strictness is a property of, not structure on, an initial object.
+
+```agda
+is-strict-initial-is-prop : ∀ i → is-prop (is-strict-initial i)
+is-strict-initial-is-prop i = hlevel!
+```

src/Cat/Instances/Sets.lagda.md

@@ -1,5 +1,7 @@
 <!--
 ```agda
+open import 1Lab.Reflection.Marker
+
 open import Cat.Prelude
 ```
 -->
@@ -89,3 +91,43 @@ We then use [univalence for $n$-types] to directly establish that $(A
     (∣ A ∣ ≃ ∣ B ∣) ≃⟨ equiv≃iso e⁻¹ ⟩
     (A Sets.≅ B)    ≃∎
 ```
+
+## Sets^op is also a category
+
+```agda
+  import Cat.Reasoning (Sets ℓ ^op) as Sets^op
+```
+
+First we show that isomorphism is invariant under `^op`{.Agda}.
+
+```agda
+  iso-op-invariant : ∀ {A B : Set ℓ} → (A Sets^op.≅ B) ≃ (A Sets.≅ B)
+  iso-op-invariant {A} {B} = Iso→Equiv the-iso
+    where
+      open import Cat.Morphism
+      open Inverses
+      the-iso : Iso (A Sets^op.≅ B) (A Sets.≅ B) 
+      the-iso .fst i .to = i .from
+      the-iso .fst i .from = i .to
+      the-iso .fst i .inverses .invl = i .invl
+      the-iso .fst i .inverses .invr = i .invr
+      the-iso .snd .is-iso.inv i .to = i .from
+      the-iso .snd .is-iso.inv i .from = i .to
+      the-iso .snd .is-iso.inv i .inverses .invl = i .invl
+      the-iso .snd .is-iso.inv i .inverses .invr = i .invr
+      the-iso .snd .is-iso.rinv _ = refl
+      the-iso .snd .is-iso.linv _ = refl
+```
+
+This fact lets us re-use the `to-path`{.Agda} component of `Sets-is-category`{.Agda}. Some calculation gives us `to-path-over`{.Agda}.
+
+```agda
+  Sets^op-is-category : is-category (Sets ℓ ^op)
+  Sets^op-is-category .to-path = Sets-is-category .to-path ⊙ transport (ua iso-op-invariant)
+  Sets^op-is-category .to-path-over {a} {b} p = Sets^op.≅-pathp refl _ $ funext-dep λ {x₀} {x₁} q →
+    x₀                                                    ≡˘⟨ ap (_$ x₀) p.invr ⟩ 
+    p.to ⌜ p.from x₀ ⌝                                    ≡˘⟨ ap¡ Regularity.reduce! ⟩ 
+    p.to ⌜ transport refl $ p.from $ transport refl x₀ ⌝  ≡⟨ ap! (λ i → unglue (∂ i) (q i)) ⟩
+    p.to x₁                                               ∎
+    where module p = Sets^op._≅_ p
+```  

src/Cat/Instances/Sets/Cocomplete.lagda.md

@@ -200,3 +200,13 @@ truncation --- to prove $\bot$ using the assumption that $i ≠ j$.
       uniq _ = funext λ where
         (_ , _ , p) → absurd (i≠j (ap (∥-∥₀-elim (λ _ → I .is-tr) fst) p))
 ```
+<!--
+```agda
+Sets-initial : ∀ {ℓ} → Initial (Sets ℓ)
+Sets-initial .Initial.bot = el! (Lift _ ⊥)
+Sets-initial .Initial.has⊥ x .centre () 
+Sets-initial .Initial.has⊥ x .paths _ = ext λ ()
+
+```
+
+-->

src/Cat/Instances/Sets/Counterexamples/SelfDual.lagda.md

@@ -0,0 +1,119 @@
+<!--
+```agda
+open import Cat.Instances.Sets.Cocomplete using (Sets-initial)
+open import Cat.Diagram.Initial
+open import Cat.Instances.Sets using (Sets^op-is-category)
+open import Cat.Morphism
+open import Cat.Prelude
+
+open import Data.Bool
+```
+-->
+
+```agda
+module Cat.Instances.Sets.Counterexamples.SelfDual {ℓ} where
+```
+# Sets is not self-dual
+
+We show that the category of sets is not self-dual, that is, there cannot exist a path between $\Sets$ and $\Sets\op$.
+
+```agda
+import Cat.Reasoning (Sets ℓ) as Sets
+import Cat.Reasoning (Sets ℓ ^op) as Sets^op
+```
+
+
+To show our goal, we need to find a categorical property that holds in $\Sets$ but _not_ in $\Sets\op$.
+First we note that both $\Sets$ and $\Sets\op$ have an initial object.
+
+In $\Sets$:
+
+```agda
+_ : Initial (Sets ℓ)
+_ = Sets-initial
+```
+
+
+In $\Sets\op$:
+
+<!--
+```agda
+open Initial
+open Strict-initial
+open Sets.is-invertible
+open Sets.Inverses
+```
+-->
+
+```agda
+Sets^op-initial : Initial (Sets ℓ ^op)
+Sets^op-initial .bot = el! (Lift _ ⊤)
+Sets^op-initial .has⊥ x = hlevel!
+```
+<!--
+```agda
+_ = ⊥
+``` 
+-->
+
+Now we can observe an interesting property of the initial object of $\Sets$: it is *[strict]*, meaning every morphism into it is in fact an *iso*morphism.
+Intuitively, if you can write a function $X \to \bot$ then $X$ must itself be empty. 
+
+[strict]: Cat.Diagram.Initial.html#strictness
+
+```agda
+Sets-strict-initial : Strict-initial (Sets ℓ)
+Sets-strict-initial .initial = Sets-initial
+Sets-strict-initial .has-is-strict x f .inv ()
+Sets-strict-initial .has-is-strict x f .inverses .invl = ext λ ()
+Sets-strict-initial .has-is-strict x f .inverses .invr = ext λ x → absurd (f x .Lift.lower)
+```
+
+<!-- 
+```agda
+_ = true≠false
+```
+-->
+
+Crucially, this property is not shared by the initial object of $\Sets\op$! Unfolding definitions, it says 
+that any function $\top \to X$ is an isomorphism, or equivalently, every inhabited set is contractible. But is this is certainly false:
+`Bool`{.Agda} is inhabited, but not contractible, since `true≠false`{.Agda}.
+
+```agda
+¬Sets^op-strict-initial : ¬ Strict-initial (Sets ℓ ^op)
+¬Sets^op-strict-initial si = true≠false true≡false
+  where
+```
+
+$\Sets\op$ is univalent, so we invoke the propositionality of its initial object to let us work with `⊤`{.Agda}, for convenience.
+
+```agda
+    si≡⊤ : si .initial ≡ Sets^op-initial
+    si≡⊤ = ⊥-is-prop _ Sets^op-is-category _ _
+
+    to-iso-⊤ : (A : Set ℓ) → (Lift ℓ ⊤ → ⌞ A ⌟) → A Sets^op.≅ el! (Lift ℓ ⊤)
+    to-iso-⊤ A f = invertible→iso _ _ (subst (is-strict-initial (Sets ℓ ^op)) si≡⊤ (si .has-is-strict) A f)
+```
+
+Using our ill-fated hypothesis, we can construct an iso between `Bool`{.Agda} and `⊤`{.Agda} from a function $\top \to$ `Bool`{.Agda}. From this
+we conclude that `Bool`{.Agda} is contractible, from which we obtain (modulo `lift`{.Agda}ing) a proof of `true`{.Agda} `≡`{.Agda} `false`{.Agda}.
+
+```agda
+    Bool≅⊤ : el! (Lift ℓ Bool) Sets^op.≅ el! (Lift ℓ ⊤)
+    Bool≅⊤ = to-iso-⊤ (el! (Lift _ Bool)) λ _ → lift true
+
+    Bool-is-contr : is-contr (Lift ℓ Bool)
+    Bool-is-contr = subst (is-contr ⊙ ∣_∣) (sym (Univalent.iso→path Sets^op-is-category Bool≅⊤)) hlevel!
+
+    true≡false : true ≡ false
+    true≡false = lift-inj $ is-contr→is-prop Bool-is-contr _ _
+```
+
+We've shown that a categorical property holds in $\Sets$ and fails in $\Sets\op$, but paths between categories preserve categorical properties,
+so we have a contradiction!
+
+```agda
+Sets≠Sets^op : ¬ (Sets ℓ ≡ Sets ℓ ^op)
+Sets≠Sets^op p = ¬Sets^op-strict-initial (subst Strict-initial p Sets-strict-initial)
+```
+

src/index.lagda.md

@@ -559,6 +559,7 @@ open import Cat.Instances.Sets.Complete -- is complete
 open import Cat.Instances.Sets.Cocomplete -- is cocomplete, with disjoint coproducts
 open import Cat.Instances.Sets.Congruences -- has effective congruences
 open import Cat.Instances.Sets.CartesianClosed -- and is locally cartesian closed
+open import Cat.Instances.Sets.Counterexamples.SelfDual -- and is not self-dual
 ```
 
 The category of polynomial functors: