diff --git a/src/Cat/Diagram/Initial.lagda.md b/src/Cat/Diagram/Initial.lagda.md index 4a721d4c4..7e4f0e254 100644 --- a/src/Cat/Diagram/Initial.lagda.md +++ b/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! +``` diff --git a/src/Cat/Instances/Sets.lagda.md b/src/Cat/Instances/Sets.lagda.md index 377c8df0c..144660d51 100644 --- a/src/Cat/Instances/Sets.lagda.md +++ b/src/Cat/Instances/Sets.lagda.md @@ -1,5 +1,7 @@ @@ -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 +``` diff --git a/src/Cat/Instances/Sets/Cocomplete.lagda.md b/src/Cat/Instances/Sets/Cocomplete.lagda.md index cc0b96b10..fbc8d0259 100644 --- a/src/Cat/Instances/Sets/Cocomplete.lagda.md +++ b/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)) ``` + diff --git a/src/Cat/Instances/Sets/Counterexamples/SelfDual.lagda.md b/src/Cat/Instances/Sets/Counterexamples/SelfDual.lagda.md new file mode 100644 index 000000000..7c3b314fb --- /dev/null +++ b/src/Cat/Instances/Sets/Counterexamples/SelfDual.lagda.md @@ -0,0 +1,119 @@ + + +```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 +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 $\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) +``` + + + +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) +``` + diff --git a/src/index.lagda.md b/src/index.lagda.md index 14596e62f..eacab034d 100644 --- a/src/index.lagda.md +++ b/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: