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 and

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 but not in First we note that both and have an initial object.

In

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


In

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 it is strict, meaning every morphism into it is in fact an isomorphism. Intuitively, if you can write a function then 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 Unfolding definitions, it says that any function 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


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 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 and fails in 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)