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

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)

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)