Skip to content

Commit c47af8c

Browse files
lowasserlowasser
authored
Axioms of countable and dependent choice (UniMath#1463)
Countable choice has come up in UniMath#1458 as a necessary ingredient of the classical completion of a metric space. I have hopes we can avoid ACC, but the only constructive approach I've seen is HoTT's higher inductive-inductive types, which I'm not sure work in Cubical Agda, let alone unimath. I haven't managed to put that together -- but it seemed a reasonable time to at least define these axioms and their relationships.
1 parent 39c4224 commit c47af8c

10 files changed

Lines changed: 455 additions & 2 deletions

‎codespell-dictionary.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ homomorhpism->homomorphism
2727
homomorhpisms->homomorphisms
2828
homomorphsim->homomorphism
2929
homomorphsims->homomorphisms
30+
identitification->identification
3031
isomorhpism->isomorphism
3132
isomorhpisms->isomorphisms
3233
isomorphsim->isomorphism

‎src/foundation-core/embeddings.lagda.md‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,12 @@ open import foundation-core.identity-types
2020

2121
## Idea
2222

23-
An **embedding** from one type into another is a map that induces
23+
An {{#concept "embedding" Agda=_↪_ WD="embedding" WDID=Q980509}} from one type
24+
into another is a map that induces
2425
[equivalences](foundation-core.equivalences.md) on
2526
[identity types](foundation-core.identity-types.md). In other words, the
2627
identitifications `(f x) ＝ (f y)` for an embedding `f : A → B` are in
27-
one-to-one correspondence with the identitifications `x ＝ y`. Embeddings are
28+
one-to-one correspondence with the identifications `x ＝ y`. Embeddings are
2829
better behaved homotopically than
2930
[injective maps](foundation-core.injective-maps.md), because the condition of
3031
being an equivalence is a [property](foundation-core.propositions.md) under

‎src/foundation.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ open import foundation.arithmetic-law-coproduct-and-sigma-decompositions public
2929
open import foundation.arithmetic-law-product-and-pi-decompositions public
3030
open import foundation.automorphisms public
3131
open import foundation.axiom-of-choice public
32+
open import foundation.axiom-of-countable-choice public
33+
open import foundation.axiom-of-dependent-choice public
3234
open import foundation.bands public
3335
open import foundation.base-changes-span-diagrams public
3436
open import foundation.bicomposition-functions public

‎src/foundation/axiom-of-choice.lagda.md‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,10 @@ module foundation.axiom-of-choice where
77
<details><summary>Imports</summary>
88

99
```agda
10+
open import elementary-number-theory.natural-numbers
11+
12+
open import foundation.action-on-identifications-functions
13+
open import foundation.coproduct-types
1014
open import foundation.dependent-pair-types
1115
open import foundation.function-extensionality
1216
open import foundation.functoriality-propositional-truncation
@@ -17,6 +21,8 @@ open import foundation.propositional-truncations
1721
open import foundation.sections
1822
open import foundation.split-surjective-maps
1923
open import foundation.surjective-maps
24+
open import foundation.unit-type
25+
open import foundation.univalence
2026
open import foundation.universe-levels
2127
2228
open import foundation-core.equivalences
@@ -26,6 +32,10 @@ open import foundation-core.functoriality-dependent-pair-types
2632
open import foundation-core.identity-types
2733
open import foundation-core.precomposition-functions
2834
open import foundation-core.sets
35+
36+
open import univalent-combinatorics.counting
37+
open import univalent-combinatorics.finite-types
38+
open import univalent-combinatorics.standard-finite-types
2939
```
3040

3141
</details>
@@ -112,10 +122,58 @@ AC0-is-set-projective H A B K =
112122
( id))
113123
```
114124

125+
### Choice holds constructively for finite types
126+
127+
```agda
128+
instance-choice-Fin :
129+
(n : ℕ) → {l : Level} → (F : Fin n → UU l) →
130+
instance-choice (Fin n) F
131+
instance-choice-Fin zero-ℕ F _ = unit-trunc-Prop (λ ())
132+
instance-choice-Fin (succ-ℕ n) F inhabited-F =
133+
let
134+
open do-syntax-trunc-Prop (is-inhabited-Prop ((x : Fin (succ-ℕ n)) → F x))
135+
in do
136+
f<n ← instance-choice-Fin n (F ∘ inl-Fin n) (inhabited-F ∘ inl-Fin n)
137+
fn ← inhabited-F (neg-one-Fin n)
138+
unit-trunc-Prop
139+
( λ where
140+
(inr star) → fn
141+
(inl k) → f<n k)
142+
143+
module _
144+
{l : Level} (A : Finite-Type l)
145+
where
146+
147+
instance-choice-Finite-Type :
148+
{l' : Level} → (B : type-Finite-Type A → UU l') →
149+
instance-choice (type-Finite-Type A) B
150+
instance-choice-Finite-Type B inhabited-B =
151+
let
152+
open
153+
do-syntax-trunc-Prop
154+
( is-inhabited-Prop ((a : type-Finite-Type A) → B a))
155+
in do
156+
(n , Fin-n≃A) ← is-finite-type-Finite-Type A
157+
f-Fin-n ←
158+
instance-choice-Fin
159+
( n)
160+
( B ∘ map-equiv Fin-n≃A)
161+
( inhabited-B ∘ map-equiv Fin-n≃A)
162+
unit-trunc-Prop
163+
( λ a →
164+
map-eq
165+
( ap B (is-section-map-section-map-equiv Fin-n≃A a))
166+
( f-Fin-n (map-inv-equiv Fin-n≃A a)))
167+
```
168+
115169
## See also
116170

117171
- [Diaconescu's theorem](foundation.diaconescus-theorem.md), which states that
118172
the axiom of choice implies the law of excluded middle.
173+
- [The axiom of countable choice](foundation.axiom-of-countable-choice.md), the
174+
axiom of choice restricted to [countable sets](set-theory.countable-sets.md).
175+
- [The axiom of dependent choice](foundation.axiom-of-dependent-choice.md),
176+
another weaker form of the axiom of choice.
119177

120178
## References
121179

‎src/foundation/axiom-of-countable-choice.lagda.md‎

Lines changed: 173 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,173 @@
1+
# The axiom of countable choice
2+
3+
```agda
4+
module foundation.axiom-of-countable-choice where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.equality-natural-numbers
11+
open import elementary-number-theory.inequality-natural-numbers
12+
open import elementary-number-theory.natural-numbers
13+
open import elementary-number-theory.strict-inequality-natural-numbers
14+
15+
open import foundation.action-on-identifications-functions
16+
open import foundation.axiom-of-choice
17+
open import foundation.axiom-of-dependent-choice
18+
open import foundation.binary-relations
19+
open import foundation.coproduct-types
20+
open import foundation.decidable-equality
21+
open import foundation.dependent-pair-types
22+
open import foundation.embeddings
23+
open import foundation.equivalences
24+
open import foundation.function-types
25+
open import foundation.identity-types
26+
open import foundation.inhabited-types
27+
open import foundation.maybe
28+
open import foundation.propositional-truncations
29+
open import foundation.raising-universe-levels
30+
open import foundation.sets
31+
open import foundation.transport-along-identifications
32+
open import foundation.unit-type
33+
open import foundation.univalence
34+
open import foundation.universe-levels
35+
36+
open import set-theory.countable-sets
37+
38+
open import univalent-combinatorics.classical-finite-types
39+
```
40+
41+
</details>
42+
43+
## Idea
44+
45+
The
46+
{{#concept "axiom of countable choice" WD="axiom of countable choice" WDID=Q1000116 Agda=ACω}}
47+
asserts that for every family of [inhabited](foundation.inhabited-types.md)
48+
[sets](foundation.sets.md) `B` indexed by the
49+
[natural numbers](elementary-number-theory.natural-numbers.md) `ℕ`, the type of
50+
sections of that family `(n : ℕ) → B n` is inhabited.
51+
52+
## Definition
53+
54+
```agda
55+
level-ACω : (l : Level) → UU (lsuc l)
56+
level-ACω l =
57+
(f : ℕ → Set l) (inhabited-f : (n : ℕ) → is-inhabited (type-Set (f n))) →
58+
is-inhabited ((n : ℕ) → type-Set (f n))
59+
60+
ACω : UUω
61+
ACω = {l : Level} → level-ACω l
62+
```
63+
64+
## Properties
65+
66+
### The axiom of countable choice implies choice for countable sets with decidable equality
67+
68+
```agda
69+
module _
70+
{l : Level} (X : Set l)
71+
(countable-X : is-countable X)
72+
(decidable-equality-X : has-decidable-equality (type-Set X))
73+
where
74+
75+
choice-countable-discrete-set-ACω :
76+
{l2 : Level} → ACω → (F : type-Set X → Set l2) → instance-choice-Set X F
77+
choice-countable-discrete-set-ACω {l2} acω F inhabited-F =
78+
let
79+
open
80+
do-syntax-trunc-Prop
81+
( is-inhabited-Prop ((x : type-Set X) → type-Set (F x)))
82+
F' : Maybe (type-Set X) → Set l2
83+
F' = rec-coproduct F (λ _ → raise-Set l2 unit-Set)
84+
inhabited-F' : (x : Maybe (type-Set X)) → is-inhabited (type-Set (F' x))
85+
inhabited-F' =
86+
λ where
87+
(inl x) → inhabited-F x
88+
(inr star) → unit-trunc-Prop (map-raise star)
89+
in do
90+
e ← countable-X
91+
g ← acω (F' ∘ map-enumeration X e) (inhabited-F' ∘ map-enumeration X e)
92+
unit-trunc-Prop
93+
( λ x →
94+
let
95+
( n , en=unit-x , _) =
96+
minimal-preimage-enumeration-discrete-Set
97+
( X)
98+
( e)
99+
( decidable-equality-X)
100+
( x)
101+
in map-eq (ap (type-Set ∘ F') en=unit-x) (g n))
102+
```
103+
104+
### The axiom of choice implies the axiom of countable choice
105+
106+
```agda
107+
level-ACω-level-AC0 : {l : Level} → level-AC0 lzero l → level-ACω l
108+
level-ACω-level-AC0 ac0 f inhabited-f = ac0 ℕ-Set (type-Set ∘ f) inhabited-f
109+
110+
ACω-AC0 : AC0 → ACω
111+
ACω-AC0 ac0 = level-ACω-level-AC0 ac0
112+
```
113+
114+
### The axiom of dependent choice implies the axiom of countable choice
115+
116+
```agda
117+
level-ACω-level-ADC : {l : Level} → level-ADC l lzero → level-ACω l
118+
level-ACω-level-ADC {l} adc f inhabited-f =
119+
do
120+
(g , r-gn-g⟨n+1⟩) ←
121+
adc (A , is-set-A) (unit-trunc-Prop (0 , λ ())) R entire-R
122+
let
123+
dom-g : (m : ℕ) → m ≤-ℕ pr1 (g m)
124+
dom-g =
125+
ind-ℕ
126+
( leq-zero-ℕ (pr1 (g 0)))
127+
( λ m m≤gn → tr (leq-ℕ (succ-ℕ m)) (r-gn-g⟨n+1⟩ m) m≤gn)
128+
h : (m : ℕ) (k : classical-Fin m) → type-Set (f (pr1 k))
129+
h =
130+
λ m (k , k<m) →
131+
pr2 (g m) (k , concatenate-le-leq-ℕ {k} {m} {pr1 (g m)} k<m (dom-g m))
132+
unit-trunc-Prop (λ n → h (succ-ℕ n) (n , succ-le-ℕ n))
133+
where
134+
open
135+
do-syntax-trunc-Prop
136+
( is-inhabited-Prop ((n : ℕ) → type-Set (f n)))
137+
A : UU l
138+
A =
139+
Σ ℕ
140+
( λ n →
141+
(k : classical-Fin n) →
142+
type-Set (f (nat-classical-Fin n k)))
143+
is-set-A : is-set A
144+
is-set-A = is-set-Σ is-set-ℕ (λ _ → is-set-Π (pr2 ∘ f ∘ pr1))
145+
R : Relation lzero A
146+
R (m , _) (n , _) = succ-ℕ m ＝ n
147+
entire-R : is-entire-Relation R
148+
entire-R (n , f<n) =
149+
rec-trunc-Prop
150+
( is-inhabited-Prop (Σ A (R (n , f<n))))
151+
( λ fn →
152+
unit-trunc-Prop
153+
( ( succ-ℕ n ,
154+
λ (k , k<sn) →
155+
rec-coproduct
156+
( λ k<n → f<n (k , k<n))
157+
( λ n≤k →
158+
map-eq
159+
( ap
160+
( type-Set ∘ f)
161+
( antisymmetric-leq-ℕ n k
162+
( n≤k)
163+
( leq-le-succ-ℕ k n k<sn)))
164+
( fn))
165+
( decide-le-leq-ℕ k n)) ,
166+
refl))
167+
( inhabited-f n)
168+
```
169+
170+
## See also
171+
172+
- [The axiom of choice](foundation.axiom-of-choice.md)
173+
- [The axiom of dependent choice](foundation.axiom-of-dependent-choice.md)

‎src/foundation/axiom-of-dependent-choice.lagda.md‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
# The axiom of dependent choice
2+
3+
```agda
4+
module foundation.axiom-of-dependent-choice where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.natural-numbers
11+
12+
open import foundation.axiom-of-choice
13+
open import foundation.binary-relations
14+
open import foundation.dependent-pair-types
15+
open import foundation.existential-quantification
16+
open import foundation.function-types
17+
open import foundation.inhabited-types
18+
open import foundation.propositional-truncations
19+
open import foundation.sets
20+
open import foundation.universe-levels
21+
```
22+
23+
</details>
24+
25+
## Idea
26+
27+
The
28+
{{#concept "axiom of dependent choice" WD="axiom of dependent choice" WDID=Q3303153 Agda=ADC}}
29+
asserts that for every [entire binary relation](foundation.binary-relations.md)
30+
`R` on an [inhabited type](foundation.inhabited-types.md) `A`, there
31+
[exists](foundation.existential-quantification.md) `f : ℕ → A` such that for all
32+
`n : ℕ` , `R (f n) (f (succ-ℕ n))`.
33+
34+
## Definition
35+
36+
```agda
37+
module _
38+
{l1 : Level} (A : Set l1) (inhabited-A : is-inhabited (type-Set A))
39+
{l2 : Level} (R : Relation l2 (type-Set A))
40+
(H : is-entire-Relation R)
41+
where
42+
43+
instance-ADC : UU (l1 ⊔ l2)
44+
instance-ADC =
45+
is-inhabited (Σ (ℕ → type-Set A) (λ f → (n : ℕ) → R (f n) (f (succ-ℕ n))))
46+
47+
level-ADC : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
48+
level-ADC l1 l2 =
49+
(A : Set l1) (inhabited-A : is-inhabited (type-Set A)) →
50+
(R : Relation l2 (type-Set A)) (H : is-entire-Relation R) →
51+
instance-ADC A inhabited-A R H
52+
53+
ADC : UUω
54+
ADC = {l1 l2 : Level} → level-ADC l1 l2
55+
```
56+
57+
## Properties
58+
59+
### The axiom of choice implies the axiom of dependent choice
60+
61+
```agda
62+
level-ADC-level-AC0 : {l1 l2 : Level} → level-AC0 l1 (l1 ⊔ l2) → level-ADC l1 l2
63+
level-ADC-level-AC0 ac0 A inhabited-A R entire-R =
64+
let
65+
open
66+
do-syntax-trunc-Prop
67+
( is-inhabited-Prop
68+
( Σ (ℕ → type-Set A) (λ f → (n : ℕ) → R (f n) (f (succ-ℕ n)))))
69+
in do
70+
f ← ac0 A (λ a → Σ (type-Set A) (R a)) entire-R
71+
a₀ ← inhabited-A
72+
let g = ind-ℕ a₀ (λ _ → pr1 ∘ f)
73+
unit-trunc-Prop (g , pr2 ∘ f ∘ g)
74+
75+
ADC-AC0 : AC0 → ADC
76+
ADC-AC0 ac0 = level-ADC-level-AC0 ac0
77+
```
78+
79+
## See also
80+
81+
- [The axiom of choice](foundation.axiom-of-choice.md)
82+
- [The axiom of countable choice](foundation.axiom-of-countable-choice.md)

0 commit comments

Comments
 (0)