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}.$

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:$

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

In $Sets_{op}:$

Sets^op-initial : Initial (Sets β ^op) Sets^op-initial .bot = el! (Lift _ β€) Sets^op-initial .hasβ₯ x = hlevel 0

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ββ₯$
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 .lower)

Crucially, this property is not shared by the initial object of
$Sets_{op}!$
Unfolding definitions, it says that any function
$β€β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

$Sets_{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
$β€β$
`Bool`

. From this we conclude
that `Bool`

is contractible, from
which we obtain (modulo `lift`

ing) 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 0) 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!

Setsβ Sets^op : Β¬ (Sets β β‘ Sets β ^op) Setsβ Sets^op p = Β¬Sets^op-strict-initial (subst Strict-initial p Sets-strict-initial)