Propositions, Sets and Logic
Contents
- Singletons and Propositions
- Sets
- Examples
- Props are Sets
- A taste of Excluded Middle
- Hedberg’s theorem and characterization of sets
- Appendix: the axiom K
{-# OPTIONS --without-K --safe --exact-split #-} module sets-logic where open import mltt open import twocatconstructions open import negation hiding (Id-to-Fun; Id-to-Fun') --redefined in univalence-base open import basichomotopy open import univalence-base open ≡-Reasoning open ◾-lemmas open ap-lemmas open transport-lemmas
Singletons and Propositions
In Basic Homotopy we have looked at contractible and path-connected types. Here we explore these notions more in depth.
First, we create new names for some of the types we introduced there:
isEmpty isSingleton isProp : ∀ {ℓ} → Set ℓ → Set ℓ isEmpty = is-empty isSingleton = iscontr isProp = ispathconn center : ∀ {ℓ} (A : Set ℓ) → isSingleton A → A center = iscontr-center
Recall that if for a type A isProp A is inhabited, it means the type is connected, or alternatively that any two of its terms are (propositionally) equal. Interpreting such a type as a “proposition” is sensible because all its terms, namely the “proofs” of the “proposition” that the type represents, are equal: in other words, we do not care of which proof we have, as long as we have one.
Remark This is different from the “propositions as types” slogan. This latter statement refers to the fact that in Type Theory the propositions of the theory are not metatheoretic 1.
The choice of isSingleton should be self-explanatory. Singletons (or contractible types) and Propositions (or path-connected types) are referred to, respectively, as (-2)-groupoids and (-1)-groupoids. In the HoTT book, and elsewhere, Propositions are also referred to as “Mere Propositions.”
We have already seen that Singletons are Props, or, in other words, (-2)-groupoids are (-1)-groupoids. We just update the names and make one of the variables implicit:
singleton-is-prop : ∀ {ℓ} {A : Set ℓ} → isSingleton A → isProp A singleton-is-prop {ℓ} {A} = contr-is-pathconn A
Inhabited Props are Singletons:
inhabited-prop-is-singleton : ∀ {ℓ} {A : Set ℓ} → A → isProp A → isSingleton A inhabited-prop-is-singleton a ispropA = a , (ispropA a)
As it is apparent from the proof, our judgement a : A provides a center of contraction.
prop-logical-eq-is-eq : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → isProp A → isProp B → (A → B) → (B → A) → A ≃ B prop-logical-eq-is-eq ispropA ispropB f g = f , (g , ε) , (g , η) where φ = ispropA ψ = ispropB ε : f ∘′ g ~ id ε = λ x → ψ (f (g x)) x η : g ∘′ f ~ id η = λ x → φ (g (f x)) x
Actually, this is a consequence of the fact that if a proposition A is logically equivalent to a type B, then it is a retract of it:
prop-and-logical-equivalence→retract : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (is : isProp A) → (A → B) → (B → A) → A ◅ B Σ.fst (prop-and-logical-equivalence→retract is s r) = r Σ.fst (Σ.snd (prop-and-logical-equivalence→retract is s r)) = s Σ.snd (Σ.snd (prop-and-logical-equivalence→retract is s r)) = λ x → is (r (s x)) x
Finally, being a proposition is preserved by weak equivalences:
weak-equivalences-preserve-props : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → isProp A → A ≃ B → isProp B weak-equivalences-preserve-props i (e , iseq) x y = x ≡⟨ π₁ (π₂ (iseq→qinv e iseq)) (x) ⁻¹ ⟩ e (e⁻¹ x ) ≡⟨ ap e (i (e⁻¹ x) (e⁻¹ y)) ⟩ e (e⁻¹ y ) ≡⟨ π₁ (π₂ (iseq→qinv e iseq)) (y) ⟩ y ∎ where A = domain e B = codomain e e⁻¹ : B → A e⁻¹ = π₁ (iseq→qinv e iseq)
Sets
The next level is that of “Set”:
isSet : ∀ {ℓ} → Set ℓ → Set ℓ -- isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q isSet A = Π[ (x , y) ∈ A × A ] Π[ (p , q) ∈ (x ≡ y) × (x ≡ y) ] (p ≡ q )
Sets are the 0-groupoids. The statement of the type encodes the assertion that any two parallel paths or identifications between x and y are equal. This, or the definition itself, says that for any two terms of a set, their identity type is path-connected, i.e. it is a Proposition. So we could alternatively have set:
isSet' : ∀ {ℓ} → Set ℓ → Set ℓ isSet' A = (x y : A) → isProp (x ≡ y)
isSet→isSet' : ∀ {ℓ} (A : Set ℓ) → isSet A → isSet' A isSet→isSet' A f x y = λ p q → f (x , y) (p , q)
It would not be difficult to show that this function is an equivalence, with inverse:
isSet'→isSet : ∀ {ℓ} (A : Set ℓ) → isSet' A → isSet A isSet'→isSet A f (x , y) = λ { (p , q) → f x y p q}For future use, let us prove that, just like propositions, weak equivalences preserve sets (note the usage of naturality and 2-categorical constructions in the proof):
weak-equivalences-preserve-sets : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → isSet A → A ≃ B → isSet B weak-equivalences-preserve-sets {ℓ} {ℓ'} {A} {B} i (e , iseq) (x , y) (p , q) = (ε x) ◾⁻ˡ w where open naturality e⁻¹ : B → A e⁻¹ = π₁ (iseq→qinv e iseq) ε : e ∘′ e⁻¹ ~ id ε = π₁ (π₂ (iseq→qinv e iseq)) p̂ q̂ : e⁻¹ x ≡ e⁻¹ y p̂ = ap e⁻¹ p q̂ = ap e⁻¹ q γ : p̂ ≡ q̂ γ = i (e⁻¹ x , e⁻¹ y) (p̂ , q̂) δ : ap e p̂ ≡ ap e q̂ δ = ap2 e γ σ : (r : x ≡ y) → (ap e (ap e⁻¹ r)) ◾ (ε y) ≡ (ε x) ◾ r σ r = (ap e (ap e⁻¹ r)) ◾ (ε y) ≡⟨ (ap∘ e⁻¹ e r) ⁻¹ ◾ʳ (ε y) ⟩ ap (e ∘′ e⁻¹) r ◾ (ε y) ≡⟨ homot-natural' ε r ⟩ (ε x) ◾ ap id r ≡⟨ (ε x) ◾ˡ (apid r) ⟩ (ε x) ◾ r ∎ w : (ε x) ◾ p ≡ (ε x) ◾ q w = (ε x) ◾ p ≡⟨ (σ p) ⁻¹ ⟩ (ap e (ap e⁻¹ p)) ◾ (ε y) ≡⟨ δ ◾ʳ (ε y) ⟩ (ap e (ap e⁻¹ q)) ◾ (ε y) ≡⟨ σ q ⟩ (ε x) ◾ q ∎
Examples
The unit type 𝟙
We have seen that 𝟙 is contractible:
𝟙-is-singleton : isSingleton 𝟙 𝟙-is-singleton = 𝟙-iscontr
and (therefore) it is a Prop:
𝟙-is-prop : isProp 𝟙 𝟙-is-prop = 𝟙-ispathconn
because:
singleton→prop : ∀ {ℓ} (A : Set ℓ) → isSingleton A → isProp A singleton→prop A = contr-is-pathconn A
More interesting, although expected, is that 𝟙 is a set because, as we have seen, for all x y : 𝟙 the type x ≡ y is equivalent to 𝟙, so any two of its terms are equal. Here is a verbose proof of this fact:
𝟙-is-set : isSet 𝟙 𝟙-is-set (x , y) (p , q) = φ ◾ ψ ⁻¹ where u = π₁ (x=y:𝟙-is-𝟙) --underlying function v = π₁ (π₁ (π₂ (x=y:𝟙-is-𝟙))) --right inverse ε = π₂ (π₁ (π₂ (x=y:𝟙-is-𝟙))) --right homotopy w = π₁ (π₂ (π₂ (x=y:𝟙-is-𝟙))) --left inverse η = π₂ (π₂ (π₂ (x=y:𝟙-is-𝟙))) --left homotopy φ : p ≡ refl φ = p ≡⟨ (η p) ⁻¹ ⟩ --this is already the goal w (u p) ≡⟨ refl ⟩ w * ≡⟨ refl ⟩ refl ∎ ψ : q ≡ refl ψ = (η q) ⁻¹ --see above
The zero type 𝟘
𝟘 is a set, because given any x y : 𝟘 we can deduce anything we like:
𝟘-is-set : isSet 𝟘 𝟘-is-set (x , y) = λ { (p , q) → !𝟘 {B = p ≡ q} x }
This is a direct proof. In fact, as we have seen, 𝟘 is a proposition:
𝟘-is-prop : isProp 𝟘 𝟘-is-prop = 𝟘-ispathconn
That 𝟘 is set will be also deducible from that it is a proposition, when we prove that propositions are sets.
Sum types
If A and B are sets, then so is their sum A + B (recall the type sum operation expresses the idea of “disjoint union”):
sum-isset : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → isSet A → isSet B → isSet (A + B) sum-isset issetA issetB (inl a , inl a') (p , q) = p ≡⟨ ap-inl-linv p ⁻¹ ⟩ ap inl p' ≡⟨ naturality.ap2 inl α ⟩ ap inl q' ≡⟨ ap-inl-linv q ⟩ q ∎ where -- any path between the injected elements in A + B comes from a path in A between the elements themselves inl-lc : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {a a' : A} (p : _≡_ {A = A + B} (inl a) (inl a')) → a ≡ a' inl-lc refl = refl ap-inl-linv : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {a a' : A} (p : _≡_ {A = A + B} (inl a) (inl a')) → ap inl (inl-lc p) ≡ p ap-inl-linv refl = refl p' q' : a ≡ a' p' = inl-lc p q' = inl-lc q f = issetA α : p' ≡ q' α = f (a , a') (p' , q') sum-isset issetA issetB (inr b , inr b') (p , q) = p ≡⟨ ap-inr-linv p ⁻¹ ⟩ ap inr p' ≡⟨ naturality.ap2 inr α ⟩ ap inr q' ≡⟨ ap-inr-linv q ⟩ q ∎ where -- do the same for the right injection inr : B → A + B inr-lc : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {b b' : B} (q : _≡_ {A = A + B} (inr b) (inr b')) → b ≡ b' inr-lc refl = refl ap-inr-linv : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {b b' : B} (q : _≡_ {A = A + B} (inr b) (inr b')) → ap inr (inr-lc q) ≡ q ap-inr-linv refl = refl p' q' : b ≡ b' p' = inr-lc p q' = inr-lc q g = issetB α : p' ≡ q' α = g (b , b') (p' , q')
Remark By contrast, the sum type of two propositions is not necessarily a proposition. This is because the type inl a ≡ inr b is empty. So, even though 𝟙 is a proposition (because it is a singleton), 𝟚 = 𝟙 + 𝟙 is not.
Cartesian Products
If A and B are sets, then so is the Cartesian Product A × B:
cart-prod-isset : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → isSet A → isSet B → isSet (A × B) cart-prod-isset issetA issetB ((a , b) , (x , y)) (p , q) = p ≡⟨ ( π₂ (π₂ (π₂ ap'-iseq )) p ) ⁻¹ ⟩ pair⁼ (ap' p ) ≡⟨ refl ⟩ pair⁼ (p₁ , p₂) ≡⟨ ap pair⁼ γ ⟩ pair⁼ (q₁ , q₂) ≡⟨ refl ⟩ pair⁼ (ap' q ) ≡⟨ π₂ (π₂ (π₂ ap'-iseq )) q ⟩ q ∎ where -- paths in A p₁ q₁ : a ≡ x p₁ = ap π₁ p q₁ = ap π₁ q -- paths in B p₂ q₂ : b ≡ y p₂ = ap π₂ p q₂ = ap π₂ q -- prove p₁ ≡ p₂ α : p₁ ≡ q₁ α = issetA (a , x) (p₁ , q₁) -- prove p₂ ≡ q₂ β : p₂ ≡ q₂ β = issetB (b , y) (p₂ , q₂) γ : (p₁ , p₂) ≡ (q₁ , q₂) γ = pair⁼ (α , β)
Σ-types
The same goes for more general Σ-types, although the proof is considerably more difficult:
Σ-type-isset : ∀ {ℓ ℓ'} {A : Set ℓ} {P : A → Set ℓ'} → isSet A → ((x : A) → isSet (P x)) → isSet (Σ A P) Σ-type-isset {P = P} issetA issetP ((x , s) , (y , t)) (p , q) = p ≡⟨ γ ⟩ q' ≡⟨ δ ⟩ q ∎ where pathinfiber : ∀ {ℓ ℓ'} {A : Set ℓ} {P : A → Set ℓ'} {u v : Σ A P} (q : u ≡ v) → transport P (ap π₁ q) (π₂ u) ≡ π₂ v pathinfiber {u = u} refl = idp (π₂ u) pp qq : (x , s) ╝ (y , t) pp = PathΣ→PathPair p qq = PathΣ→PathPair q p₁ q₁ : x ≡ y p₁ = π₁ pp q₁ = π₁ qq -- the paths in the base are equal α : p₁ ≡ q₁ α = issetA (x , y) (p₁ , q₁) -- in the fiber over y p₂ : transport P p₁ s ≡ t p₂ = π₂ pp q₂ : transport P q₁ s ≡ t q₂ = π₂ qq
Now the problem is that after breaking the paths with PathPair we get different transports in the fiber over the endpoint of the path in the base.
r : transport P p₁ s ≡ transport P q₁ s
r = transport≡ α
β : p₂ ≡ r ◾ q₂
β = issetP y ((transport P p₁ s) , t) (p₂ , (r ◾ q₂))
qq' : (x , s) ╝ (y , t)
qq' = p₁ , (r ◾ q₂)
γγ : pp ≡ qq'
γγ = pp ≡⟨ refl ⟩
(p₁ , p₂) ≡⟨ ap (λ v → p₁ , v) β ⟩
(p₁ , (r ◾ q₂)) ≡⟨ refl ⟩
qq' ∎
q' : (x , s) ≡ (y , t)
q' = PathPair→PathΣ qq'
γ : p ≡ q'
γ = p ≡⟨ (PathΣ-equiv {q = p}) ⁻¹ ⟩
PathPair→PathΣ pp ≡⟨ ap PathPair→PathΣ γγ ⟩
PathPair→PathΣ qq' ≡⟨ refl ⟩
q' ∎
We need to prove a lemma that moves the path in the base and, accordingly, shifts the corresponding path in the fiber:
lemma : ∀ {ℓ ℓ'} {A : Set ℓ} {P : A → Set ℓ'} {u v : Σ A P} ((p , q) : u ╝ v) {p' : π₁ u ≡ π₁ v} (α : p ≡ p') → (p , q) ≡ (p' , ((transport≡ α) ⁻¹ ◾ q)) lemma (p , q) {.p} refl = refl δδ : qq' ≡ qq δδ = qq' ≡⟨ lemma qq' α ⟩ q₁ , (r ⁻¹ ◾ (r ◾ q₂)) ≡⟨ ap (λ v → (q₁ , v)) (assoc (r ⁻¹) r q₂) ⁻¹ ⟩ q₁ , ((r ⁻¹ ◾ r) ◾ q₂) ≡⟨ ap (λ v → (q₁ , v)) ((linv r) ◾ʳ q₂) ⟩ q₁ , (refl ◾ q₂) ≡⟨ refl ⟩ qq ∎ δ : q' ≡ q δ = q' ≡⟨ refl ⟩ PathPair→PathΣ qq' ≡⟨ ap PathPair→PathΣ δδ ⟩ PathPair→PathΣ qq ≡⟨ PathΣ-equiv {q = q} ⟩ q ∎
An easier proof gives that, under corresponding conditions, the Σ-type of propositions is a proposition:
Σ-type-isprop : ∀ {ℓ ℓ'} {A : Set ℓ} {P : A → Set ℓ'} → isProp A → ((x : A) → isProp (P x)) → isProp (Σ A P) Σ-type-isprop {P = P} ispa i u v = PathPair→PathΣ pp where pp : u ╝ v Σ.fst pp = (ispa (π₁ u) (π₁ v)) Σ.snd pp = i (π₁ v) (transport P p (π₂ u)) (π₂ v) where p : π₁ u ≡ π₁ v p = ispa (π₁ u) (π₁ v)
Other types
There are many more examples to try as an exercise. It is the case, though, that for some of the interesting types some help from the axioms is needed in order. You can try them as exercises:
The type ℕ is a set. See the HoTT book, Example 3.1.4. No further help needed. See also below, where we use a different technique.
If
A : 𝓤is any type, andP : (x : A) → 𝓤such that eachP xis a set, then so is the typeΠ (x : A) P x. Proving this uses function extensionality.The universe
𝓤is not a set. For there are types for which there are two inequivalent self-functions such as the type𝟚, with the identity and the swap. However, one needs to turn them into identifications, which requires univalence.
Props are Sets
As expected, mere propositions as sets, just as singletons happen to be mere propostions. Thus, somewhat reassuringly, we have that 𝟙 and 𝟘 are sets.
prop-is-set : ∀ {ℓ} {A : Set ℓ} → isProp A → isSet A prop-is-set {ℓ} {A} ispropA (x , y) (p , q) = p ≡⟨ linv (g {x} x) ⁻¹ ◾ʳ p ⟩ (g x ⁻¹ ◾ g x) ◾ p ≡⟨ assoc (g x ⁻¹) (g x) p ⟩ g x ⁻¹ ◾ (g x ◾ p) ≡⟨ (g x) ⁻¹ ◾ˡ (k {x} p) ⟩ (g {x} x) ⁻¹ ◾ (g {x} y) ≡⟨ (g x) ⁻¹ ◾ˡ (k {x} q) ⁻¹ ⟩ g x ⁻¹ ◾ (g x ◾ q) ≡⟨ ( assoc (g x ⁻¹) (g x) q ) ⁻¹ ⟩ (g x ⁻¹ ◾ g x) ◾ q ≡⟨ linv (g {x} x) ◾ʳ q ⟩ q ∎ where f = ispropA g : {x : A} (y : A) → (x ≡ y) g {x} y = f x y h : {x : A} {y z : A} (p : y ≡ z) → transport (λ v → x ≡ v) p (g y) ≡ g z h {x} {y} {z} p = apd g p k : {x : A} {y z : A} (p : y ≡ z) → (g {x} y) ◾ p ≡ g z k {x} {y} {z} p = (g {x} y) ◾ p ≡⟨ ( transport-path-f p (g y) ) ⁻¹ ⟩ transport (λ v → x ≡ v) p (g y) ≡⟨ h p ⟩ g z ∎ where open transport-in-paths
A taste of Excluded Middle
There is a statement that can be proved in the context of Martin-Löf Type Theory without assuming axioms: that the Excluded Middle is, as they say, “irrefutable,” that is, its double negation always holds. In other words, for all types A
It is not the case that it is not the case that either A or ¬ A
In the following, recall that for any type, ¬ A = A → 𝟘. In the proof we start with evidence ξ : ¬ (A + ¬ A) that is, ξ : (A + ¬ A) → 𝟘.
EM-is-irrefutable : ∀ {ℓ} (A : Set ℓ) → ¬¬ (A + ¬ A) EM-is-irrefutable A ξ = ξ --takes a term of A + ¬ A (inr --we choose ¬ A, since there's no A. But ¬ A = A → 𝟘 λ x → ξ ( inl x)) --x : A so to produce 𝟘 we apply ξ to its left injection
The “wild” Law of the Excluded Middle simply asserts that we can peel those two negation operators off. This cannot be proved, but we can write its type:
wLEM : ∀ ℓ → Set (lsuc ℓ) wLEM ℓ = (A : Set ℓ) → A + ¬ A
Another way to interpret it is to say that every type, interpreted as a Proposition, is decidable.
We have seen in Negation that for any type A we have ¬ A ⟺ ¬¬¬ A. The double negation introduction rule, A → ¬¬ A which we proved, is at the basis of it. Again, the converse, that is, peeling off one negation operator from triple negation, is not provable and we can state it as an axiom, that is, we can write its type:
wLDN : ∀ ℓ → Set (lsuc ℓ) wLDN ℓ = (A : Set ℓ) → (¬¬ A → A)
The two axioms are logically equivalent:
ldn-implies-lem : ∀ {ℓ} → wLDN ℓ → wLEM ℓ ldn-implies-lem {ℓ} ldn A = ldn (A + ¬ A) dn-em where dn-em = EM-is-irrefutable A
For the converse implication we use a new construction, the With Abstraction. Its purpose is to allow us to pattern-match on an intermediate computation. In the case at hand, the value of lem A = A + ¬ A.
lem-implies-ldn : ∀ {ℓ} → wLEM ℓ → wLDN ℓ lem-implies-ldn lem A ¬¬a with (lem A) lem-implies-ldn lem A ¬¬a | inl x = x lem-implies-ldn lem A ¬¬a | inr x = !𝟘 (¬¬a x) lem-implies-ldn' : ∀ {ℓ} → wLEM ℓ → wLDN ℓ lem-implies-ldn' lem A = help (lem A) where help : (A + ¬ A) → (¬¬ A → A) help (inl a) = λ _ → a help (inr ¬a) = λ ¬¬a → !𝟘 {B = A} (¬¬a ¬a)
Remark It is important to note the form of the two lemmas for the logical equivalence of LEM and LDN. For example, LEM → LDN is not formulated as
(A : Set ℓ) → ( (A + ¬ A) → (¬¬ A → A))as one might expect, but as:
((A : Set ℓ) → (A + ¬ A)) → (B : Set ℓ) → (¬¬ B → B)The difference is crucial: in order to prove LDN for a given type \(B\), we need to know that LEM holds for all types.
However, assuming either of those axioms is incompatible with univalence: if both hold we can derive a contradiction HoTT, Thm. 3.2.2. A more reasonable version of the axiom is the following:
LEM : ∀ ℓ → Set (lsuc ℓ) LEM ℓ = (A : Set ℓ ) → isProp A → (A + ¬ A)
and
LDN : ∀ ℓ → Set (lsuc ℓ) LDN ℓ = (A : Set ℓ) → isProp A → (¬¬ A → A)
which are only stated for propositions. These are compatible with univalence, as we will probably see. Furthermore, still for mere propositions, there is a compelling alternative characterization worked out in MHE.
LEM' : ∀ ℓ → Set (lsuc ℓ) LEM' ℓ = (A : Set ℓ) → isProp A → (isSingleton A + isEmpty A)
This says that if a type is a (mere) proposition, then it either is contractible or it is empty. The two versions are logically equivalent:
LEM-implies-LEM' : ∀ {ℓ} → LEM ℓ → LEM' ℓ LEM-implies-LEM' lem A is with (lem A is) LEM-implies-LEM' lem A is | inl a = inl (inhabited-prop-is-singleton a is) LEM-implies-LEM' lem A is | inr ¬a = inr ¬a
Of course the above lemma, as well as the following converse, can be rewritten with a helper function instead of the with abstraction.
LEM'-implies-LEM : ∀ {ℓ} → LEM' ℓ → LEM ℓ LEM'-implies-LEM lem' A is with (lem' A is ) ... | inl issingl = inl (center A issingl) ... | inr ¬a = inr ¬a
The equivalent formulation of LEM is interesting because it says that a mere Proposition is either a singleton or it is empty. What if we do not assume it? We can stil prove that it is not the case that there are mere proposition that are not singletons (i.e. contractible) and also not empty: they’re aptly called “unicorns” in MHE, so let us retain the name:
there-are-no-unicorns : ∀ {ℓ} → ¬ ( Σ[ A ∈ Set ℓ ] ((isProp A) × ( (¬ (isSingleton A)) × (¬ (isEmpty A))) ) ) there-are-no-unicorns (A , isp , f , g) = nothing where ¬a : isEmpty A ¬a = λ x → f (inhabited-prop-is-singleton x isp) nothing : 𝟘 nothing = g ¬a
We have actually proved the above statement, so we can exclude these “unicorns” exist. Therefore, if LEM is not assumed, it is the case that the possible propositions are the contractible types and the empty one, however there is no way in our type theory to determine which of the two alternatives occurs for a given (mere) proposition A.
Hedberg’s theorem and characterization of sets
Hedberg’s theorem states that if a type has decidable equality then it is a set. There are other equivalent formulations (see the HoTT book), but this one contains a useful criterion to determine when a type is a set. For this particular proof and related definitions we follow the paper Generalization of Hedberg’s Theorem (published version).
We have seen that a type is decidable if A + ¬ A. Following our reference, we re-christen a type discrete it has a decidable equality:
discrete : ∀ {ℓ} → Set ℓ → Set ℓ discrete A = decidable-equality AA function is (weakly or homotopically) constant if its values are propositionally equal:
const : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B) → Set (ℓ ⊔ ℓ') const f = (x y : domain f) → f x ≡ f yand we say that a type is collapsible if there exists a constant endomorphism:
--collapsible coll : ∀ {ℓ} → Set ℓ → Set ℓ coll A = Σ[ f ∈ (A → A) ] const fFirst, a decidable type is collapsible:
decidable→collapsible : ∀ {ℓ} {A : Set ℓ} → decidable A → coll A decidable→collapsible {ℓ} {A} (inl a) = (λ x → a) , λ x y → refl decidable→collapsible {ℓ} {A} (inr ¬a) = (λ x → !𝟘 (¬a x)) , (λ x y → ap !𝟘 (γ x y)) where γ : (x y : A) → ¬a x ≡ ¬a y γ x y = 𝟘-is-prop (¬a x) (¬a y)
The technique of the proof is to observe that if A is true, namely we get a : A, then we can define a constant function f : A → A by simply assigning λ x → a, and therefore refl is a proof of constancy; if, on the other hand, we have ¬ A, i.e. we have a term ¬a : A → 𝟘, then for any x : A we get ¬a x : 𝟘, and hence we get back to A using the (unique) map !𝟘 : 𝟘 → A. Then the proof of constancy uses that 𝟘 is a proposition to prove ¬a x ≡ ¬a y, for all x y : A.
--path-collapsible path-coll : ∀ {ℓ} → Set ℓ → Set ℓ path-coll A = (x y : A) → coll (x ≡ y)Then, we have our first lemma, that discrete types are path-collapsible:
discrete→path-collapsible : ∀ {ℓ} {A : Set ℓ} → discrete A → path-coll A discrete→path-collapsible d = λ x y → decidable→collapsible (d x y) Lemma-1[Hedberg] = discrete→path-collapsibleSets are path collapsible: the constant endo-function we need on each identity type is actually the identity, and the proof that the type is a set provides the proof of constancy for the endo-function:
--sets are path-collapsible isSet→path-collapsible : ∀ {ℓ} {A : Set ℓ} → isSet A → path-coll A isSet→path-collapsible {ℓ} {A} is x y = id , (λ p q → is (x , y) (p , q))
Now, we come to the second lemma that will be needed in Hedberg’s theorem proof. This statement is very useful in its own right: it gives a more practical criterion to determine that a type is a set, by providing a constant endo-function on its identity types. The proof relies on the following non-obvious fact: assuming we are given for each x y : A an f : x ≡ y → x ≡ y, then we have that for each r : x ≡ y
r ≡ (f x x refl) ⁻¹ ◾ (f x y r)which is proved by path induction on r. Indeed, assuming r = refl, which means y = x the above reduces to
refl ≡ (f x x refl) ⁻¹ ◾ (f x x refl)--path-collapsible are sets path-collapsible→isSet : ∀ {ℓ} {A : Set ℓ} → path-coll A → isSet A path-collapsible→isSet {ℓ} {A} pc (x , y) (p , q) = lemma-3 where f : (x y : A) → x ≡ y → x ≡ y f x y = π₁ (pc x y) f-is-const : (x y : A) (p q : x ≡ y) → f x y p ≡ f x y q f-is-const x y = π₂ (pc x y) lemma-1 : (x y : A) (r : x ≡ y) → r ≡ (f x x refl) ⁻¹ ◾ (f x y r) lemma-1 x .x refl = ( (linv (f x x refl)) ) ⁻¹ lemma-2 : (f x x refl) ⁻¹ ◾ (f x y p) ≡ (f x x refl) ⁻¹ ◾ (f x y q) lemma-2 = ap (λ h → (f x x refl) ⁻¹ ◾ h) (f-is-const x y p q) lemma-3 : p ≡ q lemma-3 = p ≡⟨ lemma-1 x y p ⟩ (f x x refl) ⁻¹ ◾ (f x y p) ≡⟨ lemma-2 ⟩ (f x x refl) ⁻¹ ◾ (f x y q) ≡⟨ (lemma-1 x y q) ⁻¹ ⟩ q ∎ Lemma-2[Hedberg] = path-collapsible→isSetFinally, we have Hedberg’s theorem proper:
--Hedberg's theorem discrete→isSet : ∀ {ℓ} {A : Set ℓ} → discrete A → isSet A discrete→isSet d = path-collapsible→isSet (discrete→path-collapsible d) Thm[Hedberg] = discrete→isSetAs a simple application, let us prove that the type of Natural Numbers is a set. We have already proved that ℕ has decidable equality, so that it is a set by a straightforward application of Hedberg’s theorem:
module ℕ-is-set where open import naturals ℕ-is-discrete : discrete ℕ ℕ-is-discrete = ℕ-decidable-equality ℕ-is-set : isSet ℕ ℕ-is-set = discrete→isSet (ℕ-is-discrete)
Appendix: the axiom K
There is another characterization of Sets. It involves the famous T. Streicher’s “axiom K”.
As usual, we write the type holding it:module K-axiom where K : ∀ {ℓ} → {A : Set ℓ} → Set ℓ K {ℓ} {A} = (x : A) (p : x ≡ x) → p ≡ reflThe meaning is transparent: for all types, any self-identification of any term is a equal to the reflexivity one. It follows that if a type satisfies the axiom K it is a set
K-holds→isSet : ∀ {ℓ} {A : Set ℓ} → K → isSet A K-holds→isSet k (x , .x) (p , refl) = k x pand, conversely, if it is a set it satisfies K:
isSet→K-holds : ∀ {ℓ} {A : Set ℓ} → isSet A → K {ℓ} {A} isSet→K-holds is = λ x p → is (x , x) (p , refl)
This axiom is actually assumed by default in Agda, see the docs, unless turned off via
{-# OPTIONS --without-K #-}By the above discussion, if it is on, we get a more powerful notion of equality, but we turn every type into a set, from a connectivity point of view.
In our mathematical writings we should refrain from labeling some of our statements “Propositions”↩︎