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

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 $\mathbf{Sets}$ and ${\mathbf{Sets}}^{\mathrm{op}}\text{.}$

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 $\mathbf{Sets}$ but not in ${\mathbf{Sets}}^{\mathrm{op}}\text{.}$ First we note that both $\mathbf{Sets}$ and ${\mathbf{Sets}}^{\mathrm{op}}$ have an initial object.

In $\mathbf{Sets}\text{:}$

_ : Initial (Sets ℓ)
_ = Sets-initial

In ${\mathbf{Sets}}^{\mathrm{op}}\text{:}$

open Initial
open Strict-initial
open Sets.is-invertible
open Sets.Inverses

Sets^op-initial : Initial (Sets ℓ ^op)
Sets^op-initial .bot = el! (Lift _ ⊤)
Sets^op-initial .has⊥ x = hlevel 

_ = ⊥

Now we can observe an interesting property of the initial object of $\mathbf{Sets}\text{:}$ it is strict, meaning every morphism into it is in fact an isomorphism. Intuitively, if you can write a function $X\to \perp$ then $X$ must itself be empty.

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)

_ = true≠false

Crucially, this property is not shared by the initial object of ${\mathbf{Sets}}^{\mathrm{op}}\text{!}$ 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 is inhabited, but not contractible, since true≠false.

¬Sets^op-strict-initial : ¬ Strict-initial (Sets ℓ ^op)
¬Sets^op-strict-initial si = true≠false true≡false
  where

${\mathbf{Sets}}^{\mathrm{op}}$ is univalent, so we invoke the propositionality of its initial object to let us work with ⊤, for convenience.

    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 and ⊤ from a function $\top \to$ Bool. From this we conclude that Bool is contractible, from which we obtain (modulo lifting) a proof of true ≡ false.

    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 $\mathbf{Sets}$ and fails in ${\mathbf{Sets}}^{\mathrm{op}}\text{,}$ but paths between categories preserve categorical properties, so we have a contradiction!

Sets≠Sets^op : ¬ (Sets ℓ ≡ Sets ℓ ^op)
Sets≠Sets^op p = ¬Sets^op-strict-initial (subst Strict-initial p Sets-strict-initial)