Finiteness in terms of lists (#477)

Redefines `Finite` in terms of `List` (there's also the non-truncated
version `Listing` which isn't a prop), defines K-finite subsets as a
higher inductive type, and provides more efficient versions of the
equivalences `Fin n + Fin k ≃ Fin (n + k)` and `Fin n × Fin k = Fin (n *
k)`.

---------

Co-authored-by: Naïm Camille Favier <[email protected]>

Author: plt-amy

src/1Lab/Function/Embedding.lagda.md

@@ -10,6 +10,8 @@ description: |
 open import 1Lab.Equiv.Fibrewise
 open import 1Lab.HLevel.Universe
 open import 1Lab.HLevel.Closure
+open import 1Lab.Path.Reasoning
+open import 1Lab.Path.Groupoid
 open import 1Lab.Type.Sigma
 open import 1Lab.Univalence
 open import 1Lab.HLevel
@@ -68,7 +70,8 @@ inclusion".
 has-prop-fibres→injective
   : (f : A → B) → (∀ x → is-prop (fibre f x))
   → injective f
-has-prop-fibres→injective _ prop p = ap fst (prop _ (_ , p) (_ , refl))
+has-prop-fibres→injective f prop {x} {y} p =
+  ap fst (prop (f y) (x , p) (y , refl))
 
 between-sets-injective≃has-prop-fibres
   : is-set A → is-set B → (f : A → B)
@@ -202,17 +205,24 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} where
       contr (x , refl) λ (y , p) i → p (~ i) , λ j → p (~ i ∨ j)
 
   embedding→cancellable : is-embedding f → ∀ {x y} → is-equiv {B = f x ≡ f y} (ap f)
-  embedding→cancellable emb = total→equiv {f = λ y p → ap f {y = y} p}
-    (is-contr→is-equiv
-      (contr (_ , refl) λ (y , p) i → p i , λ j → p (i ∧ j))
-      (contr (_ , refl) (Equiv→is-hlevel 1 (Σ-ap-snd λ _ → sym-equiv) (emb _) _)))
+  embedding→cancellable emb {x} {y} = is-iso→is-equiv λ where
+    .is-iso.inv p → ap fst (emb (f y) (x , p) (y , refl))
+    .is-iso.rinv p → flatten-∨-square (ap snd (emb (f y) (x , p) (y , refl)))
+    .is-iso.linv → J (λ y p → ap fst (emb (f y) (x , ap f p) (y , refl)) ≡ p)
+      (ap-square fst (is-prop→is-set (emb (f x)) _ _ (emb (f x) (x , refl) (x , refl)) refl))
 
   equiv→cancellable : is-equiv f → ∀ {x y} → is-equiv {B = f x ≡ f y} (ap f)
   equiv→cancellable eqv = embedding→cancellable (is-equiv→is-embedding eqv)
 ```
 
 <!--
 ```agda
+  cancellable→embedding'
+    : (inj : injective f) → (∀ {x y} (p : f x ≡ f y) → ap f (inj p) ≡ p)
+    → is-embedding f
+  cancellable→embedding' i p = embedding-lemma λ x → contr (x , refl) λ where
+    (x , q) → Σ-pathp (i (sym q)) (commutes→square (ap (_∙ q) (p _) ∙∙ ∙-invl _ ∙∙ sym (∙-idr _)))
+
   abstract
     embedding→is-hlevel
       : ∀ n → is-embedding f

src/1Lab/HLevel/Closure.lagda.md

@@ -134,6 +134,15 @@ left, and `path` on the right.
       path                                      ∎
 ```
 
+<!--
+```agda
+split-surjection→is-hlevel
+  : ∀ n (f : A → B) (s : (b : B) → fibre f b)
+  → is-hlevel A n → is-hlevel B n
+split-surjection→is-hlevel n f s = retract→is-hlevel n f (λ x → s x .fst) (λ x → s x .snd)
+```
+-->
+
 ### Isomorphisms and equivalences
 
 Even though we know that [[univalence]] implies that $n$-types are

src/1Lab/Path/Reasoning.lagda.md

@@ -147,6 +147,39 @@ module _ (pq≡rs : p ∙ q ≡ r ∙ s) where
     k (i = i0) → q j
     k (j = i0) → p (~ i)
     k (i = i1) (j = i1) → s k
+
+module _ {p q : x ≡ y} where
+  ∨-square : p ≡ q → Square p q refl refl
+  ∨-square sq i j = hcomp (∂ i ∨ ∂ j) λ where
+    k (k = i0) → p j
+    k (i = i0) → sq k j
+    k (i = i1) → p (j ∨ k)
+    k (j = i0) → p (i ∧ k)
+    k (j = i1) → y
+
+  flatten-∨-square : Square p q refl refl → p ≡ q
+  flatten-∨-square sq i j = hcomp (∂ i ∨ ∂ j) λ where
+    k (k = i0) → sq j i
+    k (i = i0) → p j
+    k (i = i1) → q (j ∨ ~ k)
+    k (j = i1) → y
+    k (j = i0) → q (i ∧ ~ k)
+
+  ∧-square : p ≡ q → Square refl refl p q
+  ∧-square sq i j = hcomp (∂ i ∨ ∂ j) λ where
+    k (k = i0) → p (i ∧ j)
+    k (i = i0) → x
+    k (i = i1) → p j
+    k (j = i0) → x
+    k (j = i1) → sq k i
+
+  flatten-∧-square : Square refl refl p q → p ≡ q
+  flatten-∧-square sq i j = hcomp (∂ i ∨ ∂ j) λ where
+    k (k = i0) → sq j i
+    k (i = i0) → p (j ∧ k)
+    k (i = i1) → q j
+    k (j = i0) → x
+    k (j = i1) → p (i ∨ k)
 ```
 
 ## Cancellation

src/Cat/Diagram/Product/Finite.lagda.md

@@ -111,10 +111,11 @@ Cartesian→finite-products
   : is-category C
   → ∀ {ℓ} {X : Type ℓ} → Finite X
   → has-products-indexed-by C X
-Cartesian→finite-products cat {X = X} (fin {n} e) F =
+Cartesian→finite-products cat {X = X} e F =
   ∥-∥-rec (Indexed-product-unique C _ cat) go e
   where
-    go : X ≃ Fin n → Indexed-product C F
-    go e = Indexed-product-≃ C e
-      (Cartesian→standard-finite-products (F ⊙ Equiv.from e))
+    go : Listing X → Indexed-product C F
+    go l with e ← listing→equiv-fin l =
+      Indexed-product-≃ C e
+        (Cartesian→standard-finite-products (F ⊙ Equiv.from e))
 ```

src/Cat/Instances/FinSets/Omega.lagda.md

@@ -33,7 +33,7 @@ cardinality of $m^*(x)$.
 
 ```agda
 fin-name : ∀ {X} → Subobject X → Fin X → Fin 2
-fin-name {X = X} so m with cardinality {T = fibre (so .map) m}
+fin-name {X = X} so m with cardinality {A = fibre (so .map) m}
 ... | zero  = 0
 ... | suc x = 1
 ```
@@ -58,12 +58,12 @@ are embeddings).
 
 ```agda
 from-name : ∀ {X} (m : Subobject X) x → fin-name m x ≡ 1 → fibre (m .map) x
-from-name m x p with cardinality {T = fibre (m .map) x} | enumeration {T = fibre (m .map) x}
+from-name m x p with cardinality {A = fibre (m .map) x} | enumeration {A = fibre (m .map) x}
 ... | zero  | e = absurd (fzero≠fsuc p)
 ... | suc x | e = ∥-∥-out (injective→is-embedding! (inj m) _) (case e of λ eqv → pure (Equiv.from eqv 0))
 
 to-name : ∀ {X} (m : Subobject X) x → fibre (m .map) x → fin-name m x ≡ 1
-to-name m x p with cardinality {T = fibre (m .map) x} | enumeration {T = fibre (m .map) x}
+to-name m x p with cardinality {A = fibre (m .map) x} | enumeration {A = fibre (m .map) x}
 ... | zero  | e = absurd (case e of λ eqv → Fin-absurd (Equiv.to eqv p))
 ... | suc x | e = refl
 ```
@@ -92,7 +92,7 @@ we then have $n(x) = n(mx') = 1$ as needed.
 ```agda
 FinSets-omega .Subobject-classifier.generic .unique {m = m} {nm} pb = ext uniq where
   uniq : ∀ x → nm x ≡ fin-name m x
-  uniq x with cardinality {T = fibre (m .map) x} | enumeration {T = fibre (m .map) x} | from-name m x
+  uniq x with cardinality {A = fibre (m .map) x} | enumeration {A = fibre (m .map) x} | from-name m x
   ... | suc n | e | f with (x' , α) ← f refl = ap nm (sym α) ∙ happly (pb .square) _
 ```
 

src/Cat/Instances/Shape/Cospan.lagda.md

@@ -95,7 +95,7 @@ Cospan-hom cs-c cs-c = Lift _ ⊤ -- identity on c
 
 instance
   Finite-Cospan-ob : ∀ {ℓ} → Finite (Cospan-ob ℓ)
-  Finite-Cospan-ob = fin {cardinality = 3} (inc (Iso→Equiv i)) where
+  Finite-Cospan-ob = inc (Equiv→listing (Equiv.inverse (Iso→Equiv i)) (Listing-Fin {n = 3})) where
     i : Iso _ _
     i .fst cs-a = 0
     i .fst cs-b = 1

src/Data/Fin/Base.lagda.md

@@ -151,8 +151,8 @@ Fin-elim P pfzero pfsuc i with fin-view i
 
 <!--
 ```agda
-fin-ap : ∀ {n} {x y : Fin n} → x .lower ≡ y .lower → x ≡ y
-fin-ap p = ap₂ (λ x y → fin x ⦃ y ⦄) p (to-pathp refl)
+fin-ap : ∀ {n : I → Nat} {x : Fin (n i0)} {y : Fin (n i1)} → x .lower ≡ y .lower → PathP (λ i → Fin (n i)) x y
+fin-ap {n = n} {fin i ⦃ q ⦄} {fin j ⦃ r ⦄} s k = fin (s k) ⦃ is-prop→pathp (λ k → hlevel {T = Irr (s k Nat.< n k)} 1) q r k ⦄
 ```
 -->
 

src/Data/Fin/Closure.lagda.md

@@ -5,8 +5,11 @@ open import 1Lab.Prelude
 open import Data.Maybe.Properties
 open import Data.Set.Coequaliser
 open import Data.Fin.Properties
+open import Data.Nat.Properties
+open import Data.Nat.DivMod
+open import Data.Nat.Order
 open import Data.Fin.Base
-open import Data.Nat.Base
+open import Data.Nat.Base as Nat
 open import Data.Dec
 open import Data.Irr
 open import Data.Sum
@@ -69,20 +72,74 @@ Finite-successor {n} = Fin-suc ∙e Maybe-is-sum
 For binary coproducts, we prove the correspondence with addition in
 steps, to make the proof clearer:
 
+<!--
+```agda
+module _ where private
+```
+-->
+
 ```agda
-Finite-coproduct : (Fin n ⊎ Fin m) ≃ Fin (n + m)
-Finite-coproduct {zero} {m}  =
-  (Fin 0 ⊎ Fin m) ≃⟨ ⊎-apl Finite-zero-is-initial ⟩
-  (⊥ ⊎ Fin m)     ≃⟨ ⊎-zerol ⟩
-  Fin m           ≃∎
-Finite-coproduct {suc n} {m} =
-  (Fin (suc n) ⊎ Fin m) ≃⟨ ⊎-apl Finite-successor ⟩
-  ((⊤ ⊎ Fin n) ⊎ Fin m) ≃⟨ ⊎-assoc ⟩
-  (⊤ ⊎ (Fin n ⊎ Fin m)) ≃⟨ ⊎-apr (Finite-coproduct {n} {m}) ⟩
-  (⊤ ⊎ Fin (n + m))     ≃⟨ Finite-successor e⁻¹ ⟩
-  Fin (suc (n + m))     ≃∎
+  Finite-coproduct : (Fin n ⊎ Fin m) ≃ Fin (n + m)
+  Finite-coproduct {zero} {m}  =
+    (Fin 0 ⊎ Fin m) ≃⟨ ⊎-apl Finite-zero-is-initial ⟩
+    (⊥ ⊎ Fin m)     ≃⟨ ⊎-zerol ⟩
+    Fin m           ≃∎
+  Finite-coproduct {suc n} {m} =
+    (Fin (suc n) ⊎ Fin m) ≃⟨ ⊎-apl Finite-successor ⟩
+    ((⊤ ⊎ Fin n) ⊎ Fin m) ≃⟨ ⊎-assoc ⟩
+    (⊤ ⊎ (Fin n ⊎ Fin m)) ≃⟨ ⊎-apr (Finite-coproduct {n} {m}) ⟩
+    (⊤ ⊎ Fin (n + m))     ≃⟨ Finite-successor e⁻¹ ⟩
+    Fin (suc (n + m))     ≃∎
 ```
 
+<!--
+```agda
+Finite-coproduct : ∀ {m n} → (Fin m ⊎ Fin n) ≃ Fin (m + n)
+Finite-coproduct {m} {n} = Iso→Equiv (to , iso from ir il) where
+  to : Fin m ⊎ Fin n → Fin (m + n)
+  to (inl x) = record
+    { lower   = x .lower
+    ; bounded = forget (≤-trans (to-ℕ< x .snd) (+-≤l m n))
+    }
+  to (inr (fin i ⦃ forget α ⦄)) =
+    let
+      .p : m + i Nat.< m + n
+      p = ≤-trans (≤-refl' (sym (+-sucr m i))) (+-preserves-≤ m m (suc _) n ≤-refl α)
+    in record
+      { lower   = m + i
+      ; bounded = forget p
+      }
+
+  from : Fin (m + n) → Fin m ⊎ Fin n
+  from (fin i ⦃ forget b ⦄) with holds? (i Nat.< m)
+  ... | yes p = inl (fin i ⦃ forget p ⦄)
+  ... | no ¬p =
+    let
+      p' : m Nat.≤ i
+      p' = ≤-peel (<-from-not-≤ _ _ ¬p)
+
+      q : i - m Nat.≤ i
+      q = monus-≤ i m
+
+      .r : i - m Nat.< n
+      r = +-reflects-≤l (suc (i - m)) n m (≤-trans (≤-refl' (+-sucr m (i - m))) (≤-trans (≤-refl' (ap suc (monus-inversel i m p'))) b))
+    in inr (fin (i - m) ⦃ forget r ⦄)
+
+  ir : is-right-inverse from to
+  ir (fin i ⦃ forget b ⦄) with holds? (i Nat.< m)
+  ... | yes p = fin-ap refl
+  ... | no ¬p = fin-ap (monus-inversel i m (≤-peel (<-from-not-≤ _ _ ¬p)))
+
+  il : is-left-inverse from to
+  il (inl (fin i ⦃ forget b ⦄)) with holds? (i Nat.< m)
+  ... | yes p = refl
+  ... | no ¬p = absurd (¬p b)
+  il (inr (fin i ⦃ forget b ⦄)) with holds? ((m + i) Nat.< m)
+  ... | 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)))))
+  ... | no ¬p = ap inr (fin-ap (monus-inverser i m))
+```
+-->
+
 ### Sums
 
 We 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,
 we can use the theorem above for general sums to establish the case of
 binary products:
 
+<!--
 ```agda
-Finite-multiply : (Fin n × Fin m) ≃ Fin (n * m)
-Finite-multiply {n} {m} =
-  (Fin n × Fin m)       ≃⟨ Finite-sum (λ _ → m) ⟩
-  Fin (sum n (λ _ → m)) ≃⟨ path→equiv (ap Fin (sum≡* n m)) ⟩
-  Fin (n * m)           ≃∎
-  where
-    sum≡* : ∀ n m → sum n (λ _ → m) ≡ n * m
-    sum≡* zero m = refl
-    sum≡* (suc n) m = ap (m +_) (sum≡* n m)
+module _ where private
+```
+-->
+
+```agda
+  Finite-multiply : (Fin n × Fin m) ≃ Fin (n * m)
+  Finite-multiply {n} {m} =
+    (Fin n × Fin m)       ≃⟨ Finite-sum (λ _ → m) ⟩
+    Fin (sum n (λ _ → m)) ≃⟨ path→equiv (ap Fin (sum≡* n m)) ⟩
+    Fin (n * m)           ≃∎
+    where
+      sum≡* : ∀ n m → sum n (λ _ → m) ≡ n * m
+      sum≡* zero m = refl
+      sum≡* (suc n) m = ap (m +_) (sum≡* n m)
 ```
 
+<!--
+```agda
+Finite-multiply : ∀ {m n} → (Fin m × Fin n) ≃ Fin (m * n)
+Finite-multiply {zero} {n} = fst , record { is-eqv = λ o → absurd (Fin-absurd o) }
+Finite-multiply {suc n} {zero} = ((λ (_ , x) → absurd (Fin-absurd x))) , record { is-eqv = λ o → absurd (Fin-absurd (subst Fin (*-zeror n) o)) }
+Finite-multiply {m@(suc m')} {n@(suc n')} = Iso→Equiv (to , iso from ir il) where
+  to : Fin m × Fin n → Fin (m * n)
+  to (fin i ⦃ forget b ⦄ , fin j ⦃ forget b' ⦄) = fin (i * n + j) ⦃ forget α ⦄ where
+    α : i * n + j Nat.< m * n
+    α =
+      let
+        it : i * n + j Nat.≤ m' * n + n'
+        it = +-preserves-≤ (i * n) (m' * n) j n' (*-preserves-≤r i m' n (≤-peel (recover b))) (≤-peel (recover b'))
+      in s≤s (≤-trans it  (≤-refl' (+-commutative (m' * n) n')))
+
+  from : Fin (m * n) → Fin m × Fin n
+  from (fin i ⦃ forget b ⦄) with divmod q r quot rem ← divide-pos i n =
+    let
+      .b' : q Nat.≤ m
+      b' = *-cancel-≤r n {q} {m} $
+        ≤-trans (difference→≤ r (sym quot)) (≤-sucr (≤-peel b))
+
+      .ne : q ≠ m
+      ne p =
+        let
+          p' : m * n Nat.≤ i
+          p' = difference→≤ r (sym (subst (λ e → i ≡ e * suc n' + r) p quot))
+        in ¬sucx≤x _ (≤-trans b p')
+
+    in fin q ⦃ forget (<-from-≤ ne b') ⦄ , fin r ⦃ forget rem ⦄
+
+  ir : is-right-inverse from to
+  ir (fin i ⦃ forget b ⦄) = fin-ap (sym (is-divmod i n))
+
+  il : is-left-inverse from to
+  il (fin i ⦃ forget b ⦄ , fin j ⦃ forget b' ⦄) =
+    let
+      p : Path (DivMod (i * n + j) n) (divide-pos (i * n + j) n) (divmod i j refl b')
+      p = prop!
+    in fin-ap (ap DivMod.quot p) ,ₚ fin-ap (ap DivMod.rem p)
+```
+-->
+
 ### Products
 
 Similarly to the case for sums, the cardinality of a dependent *product* of