@@ -5,8 +5,11 @@ open import 1Lab.Prelude
55open import Data.Maybe.Properties
66open import Data.Set.Coequaliser
77open import Data.Fin.Properties
8+ open import Data.Nat.Properties
9+ open import Data.Nat.DivMod
10+ open import Data.Nat.Order
811open import Data.Fin.Base
9- open import Data.Nat.Base
12+ open import Data.Nat.Base as Nat
1013open import Data.Dec
1114open import Data.Irr
1215open import Data.Sum
@@ -69,20 +72,74 @@ Finite-successor {n} = Fin-suc ∙e Maybe-is-sum
6972For binary coproducts, we prove the correspondence with addition in
7073steps, to make the proof clearer:
7174
75+ <!--
76+ ```agda
77+ module _ where private
78+ ```
79+ -->
80+
7281``` agda
73- Finite-coproduct : (Fin n ⊎ Fin m) ≃ Fin (n + m)
74- Finite-coproduct {zero} {m} =
75- (Fin 0 ⊎ Fin m) ≃⟨ ⊎-apl Finite-zero-is-initial ⟩
76- (⊥ ⊎ Fin m) ≃⟨ ⊎-zerol ⟩
77- Fin m ≃∎
78- Finite-coproduct {suc n} {m} =
79- (Fin (suc n) ⊎ Fin m) ≃⟨ ⊎-apl Finite-successor ⟩
80- ((⊤ ⊎ Fin n) ⊎ Fin m) ≃⟨ ⊎-assoc ⟩
81- (⊤ ⊎ (Fin n ⊎ Fin m)) ≃⟨ ⊎-apr (Finite-coproduct {n} {m}) ⟩
82- (⊤ ⊎ Fin (n + m)) ≃⟨ Finite-successor e⁻¹ ⟩
83- Fin (suc (n + m)) ≃∎
82+ Finite-coproduct : (Fin n ⊎ Fin m) ≃ Fin (n + m)
83+ Finite-coproduct {zero} {m} =
84+ (Fin 0 ⊎ Fin m) ≃⟨ ⊎-apl Finite-zero-is-initial ⟩
85+ (⊥ ⊎ Fin m) ≃⟨ ⊎-zerol ⟩
86+ Fin m ≃∎
87+ Finite-coproduct {suc n} {m} =
88+ (Fin (suc n) ⊎ Fin m) ≃⟨ ⊎-apl Finite-successor ⟩
89+ ((⊤ ⊎ Fin n) ⊎ Fin m) ≃⟨ ⊎-assoc ⟩
90+ (⊤ ⊎ (Fin n ⊎ Fin m)) ≃⟨ ⊎-apr (Finite-coproduct {n} {m}) ⟩
91+ (⊤ ⊎ Fin (n + m)) ≃⟨ Finite-successor e⁻¹ ⟩
92+ Fin (suc (n + m)) ≃∎
8493```
8594
95+ <!--
96+ ```agda
97+ Finite-coproduct : ∀ {m n} → (Fin m ⊎ Fin n) ≃ Fin (m + n)
98+ Finite-coproduct {m} {n} = Iso→Equiv (to , iso from ir il) where
99+ to : Fin m ⊎ Fin n → Fin (m + n)
100+ to (inl x) = record
101+ { lower = x .lower
102+ ; bounded = forget (≤-trans (to-ℕ< x .snd) (+-≤l m n))
103+ }
104+ to (inr (fin i ⦃ forget α ⦄)) =
105+ let
106+ .p : m + i Nat.< m + n
107+ p = ≤-trans (≤-refl' (sym (+-sucr m i))) (+-preserves-≤ m m (suc _) n ≤-refl α)
108+ in record
109+ { lower = m + i
110+ ; bounded = forget p
111+ }
112+
113+ from : Fin (m + n) → Fin m ⊎ Fin n
114+ from (fin i ⦃ forget b ⦄) with holds? (i Nat.< m)
115+ ... | yes p = inl (fin i ⦃ forget p ⦄)
116+ ... | no ¬p =
117+ let
118+ p' : m Nat.≤ i
119+ p' = ≤-peel (<-from-not-≤ _ _ ¬p)
120+
121+ q : i - m Nat.≤ i
122+ q = monus-≤ i m
123+
124+ .r : i - m Nat.< n
125+ r = +-reflects-≤l (suc (i - m)) n m (≤-trans (≤-refl' (+-sucr m (i - m))) (≤-trans (≤-refl' (ap suc (monus-inversel i m p'))) b))
126+ in inr (fin (i - m) ⦃ forget r ⦄)
127+
128+ ir : is-right-inverse from to
129+ ir (fin i ⦃ forget b ⦄) with holds? (i Nat.< m)
130+ ... | yes p = fin-ap refl
131+ ... | no ¬p = fin-ap (monus-inversel i m (≤-peel (<-from-not-≤ _ _ ¬p)))
132+
133+ il : is-left-inverse from to
134+ il (inl (fin i ⦃ forget b ⦄)) with holds? (i Nat.< m)
135+ ... | yes p = refl
136+ ... | no ¬p = absurd (¬p b)
137+ il (inr (fin i ⦃ forget b ⦄)) with holds? ((m + i) Nat.< m)
138+ ... | yes p = absurd (¬sucx≤x m (+-reflects-≤l (suc m) m i (≤-trans (≤-refl' (+-sucr i m ∙ ap suc (+-commutative i m))) (≤-trans p (+-≤r i m)))))
139+ ... | no ¬p = ap inr (fin-ap (monus-inverser i m))
140+ ```
141+ -->
142+
86143### Sums
87144
88145We also have a correspondence between "coproducts" and "addition" in the
@@ -112,18 +169,67 @@ thing as summing together $n$ copies of the number $m$. Correspondingly,
112169we can use the theorem above for general sums to establish the case of
113170binary products:
114171
172+ <!--
115173```agda
116- Finite-multiply : (Fin n × Fin m) ≃ Fin (n * m)
117- Finite-multiply {n} {m} =
118- (Fin n × Fin m) ≃⟨ Finite-sum (λ _ → m) ⟩
119- Fin (sum n (λ _ → m)) ≃⟨ path→equiv (ap Fin (sum≡* n m)) ⟩
120- Fin (n * m) ≃∎
121- where
122- sum≡* : ∀ n m → sum n (λ _ → m) ≡ n * m
123- sum≡* zero m = refl
124- sum≡* (suc n) m = ap (m +_) (sum≡* n m)
174+ module _ where private
175+ ```
176+ -->
177+
178+ ``` agda
179+ Finite-multiply : (Fin n × Fin m) ≃ Fin (n * m)
180+ Finite-multiply {n} {m} =
181+ (Fin n × Fin m) ≃⟨ Finite-sum (λ _ → m) ⟩
182+ Fin (sum n (λ _ → m)) ≃⟨ path→equiv (ap Fin (sum≡* n m)) ⟩
183+ Fin (n * m) ≃∎
184+ where
185+ sum≡* : ∀ n m → sum n (λ _ → m) ≡ n * m
186+ sum≡* zero m = refl
187+ sum≡* (suc n) m = ap (m +_) (sum≡* n m)
125188```
126189
190+ <!--
191+ ```agda
192+ Finite-multiply : ∀ {m n} → (Fin m × Fin n) ≃ Fin (m * n)
193+ Finite-multiply {zero} {n} = fst , record { is-eqv = λ o → absurd (Fin-absurd o) }
194+ Finite-multiply {suc n} {zero} = ((λ (_ , x) → absurd (Fin-absurd x))) , record { is-eqv = λ o → absurd (Fin-absurd (subst Fin (*-zeror n) o)) }
195+ Finite-multiply {m@(suc m')} {n@(suc n')} = Iso→Equiv (to , iso from ir il) where
196+ to : Fin m × Fin n → Fin (m * n)
197+ to (fin i ⦃ forget b ⦄ , fin j ⦃ forget b' ⦄) = fin (i * n + j) ⦃ forget α ⦄ where
198+ α : i * n + j Nat.< m * n
199+ α =
200+ let
201+ it : i * n + j Nat.≤ m' * n + n'
202+ it = +-preserves-≤ (i * n) (m' * n) j n' (*-preserves-≤r i m' n (≤-peel (recover b))) (≤-peel (recover b'))
203+ in s≤s (≤-trans it (≤-refl' (+-commutative (m' * n) n')))
204+
205+ from : Fin (m * n) → Fin m × Fin n
206+ from (fin i ⦃ forget b ⦄) with divmod q r quot rem ← divide-pos i n =
207+ let
208+ .b' : q Nat.≤ m
209+ b' = *-cancel-≤r n {q} {m} $
210+ ≤-trans (difference→≤ r (sym quot)) (≤-sucr (≤-peel b))
211+
212+ .ne : q ≠ m
213+ ne p =
214+ let
215+ p' : m * n Nat.≤ i
216+ p' = difference→≤ r (sym (subst (λ e → i ≡ e * suc n' + r) p quot))
217+ in ¬sucx≤x _ (≤-trans b p')
218+
219+ in fin q ⦃ forget (<-from-≤ ne b') ⦄ , fin r ⦃ forget rem ⦄
220+
221+ ir : is-right-inverse from to
222+ ir (fin i ⦃ forget b ⦄) = fin-ap (sym (is-divmod i n))
223+
224+ il : is-left-inverse from to
225+ il (fin i ⦃ forget b ⦄ , fin j ⦃ forget b' ⦄) =
226+ let
227+ p : Path (DivMod (i * n + j) n) (divide-pos (i * n + j) n) (divmod i j refl b')
228+ p = prop!
229+ in fin-ap (ap DivMod.quot p) ,ₚ fin-ap (ap DivMod.rem p)
230+ ```
231+ -->
232+
127233### Products
128234
129235Similarly to the case for sums, the cardinality of a dependent * product* of
0 commit comments