def: Fin as a record type (#452)

Reimplement `Fin n` as a pair of a natural `k` + an irrelevant proof
that `k < n`, using a view to preserve the structure of pattern-matching
proofs. A couple proofs need to appeal to the view for the coverage
checker to see that only `fzero` is possible.

Author: plt-amy

src/1Lab/Reflection/Induction/Examples.agda

@@ -12,14 +12,6 @@ open import Homotopy.Space.Circle hiding (S¹-elim)
 
 module 1Lab.Reflection.Induction.Examples where
 
-unquoteDecl Fin-elim = make-elim Fin-elim (quote Fin)
-
-_ : {ℓ : Level} {P : {n : Nat} (f : Fin n) → Type ℓ}
-    (P0 : {n : Nat} → P fzero)
-    (Psuc : {n : Nat} (f : Fin n) (Pf : P f) → P (fsuc f))
-    {n : Nat} (f : Fin n) → P f
-_ = Fin-elim
-
 unquoteDecl J = make-elim-with default-elim-visible J (quote _≡ᵢ_)
 
 _ : {ℓ : Level} {A : Type ℓ} {x : A} {ℓ₁ : Level}

src/1Lab/Reflection/Variables.agda

@@ -66,9 +66,12 @@ private
   ... | nothing      | yes _ = just tm-var
   ... | nothing      | no _  = nothing
 
+  fzero' : ∀ {n} → Fin (suc n)
+  fzero' = fzero
+
   fin-term : Nat → Term
-  fin-term zero = con (quote fzero) (unknown h∷ [])
-  fin-term (suc n) = con (quote fsuc) (unknown h∷ fin-term n v∷ [])
+  fin-term zero    = def (quote fzero') (unknown h∷ [])
+  fin-term (suc n) = def (quote fsuc)   (unknown h∷ fin-term n v∷ [])
 
   env-rec : (Mot : Nat → Type b) →
           (∀ {n} → Mot n → A → Mot (suc n)) →

src/1Lab/Type.lagda.md

@@ -138,5 +138,8 @@ instance
   Number-Lift : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ Number A ⦄ → Number (Lift ℓ' A)
   Number-Lift {ℓ' = ℓ'} ⦃ a ⦄ .Number.Constraint n = Lift ℓ' (a .Number.Constraint n)
   Number-Lift ⦃ a ⦄ .Number.fromNat n ⦃ lift c ⦄ = lift (a .Number.fromNat n ⦃ c ⦄)
+
+absurdω : {A : Typeω} → .⊥ → A
+absurdω ()
 ```
 -->

src/Algebra/Group/Instances/Cyclic.lagda.md

@@ -12,9 +12,11 @@ open import Cat.Prelude
 open import Data.Int.Divisible
 open import Data.Int.Universal
 open import Data.Fin.Closure
+open import Data.Fin.Product
 open import Data.Int.DivMod
 open import Data.Fin
 open import Data.Int hiding (Positive)
+open import Data.Irr
 open import Data.Nat
 
 open represents-subgroup
@@ -182,17 +184,14 @@ $x : \ZZ$ to the representative of its congruence class modulo $n$,
 $x \% n$.
 
 ```agda
-ℤ/n≃ℕ<n : ∀ n → .⦃ Positive n ⦄ → ⌞ ℤ/ n ⌟ ≃ ℕ< n
-ℤ/n≃ℕ<n n .fst = Coeq-rec (λ i → i %ℤ n , x%ℤy<y i n)
-  λ (x , y , p) → Σ-prop-path! (divides-diff→same-rem n x y p)
-ℤ/n≃ℕ<n n .snd = is-iso→is-equiv $ iso
-  (λ (i , p) → inc (pos i))
-  (λ i → Σ-prop-path! (ℕ<-%ℤ i))
-  (elim! λ i → quot (same-rem→divides-diff n (pos (i %ℤ n)) i
-    (ℕ<-%ℤ (_ , x%ℤy<y i n))))
-
 Finite-ℤ/n : ∀ n → .⦃ Positive n ⦄ → ⌞ ℤ/ n ⌟ ≃ Fin n
-Finite-ℤ/n n = ℤ/n≃ℕ<n n ∙e Fin≃ℕ< e⁻¹
+Finite-ℤ/n n .fst = Coeq-rec (λ i → from-ℕ< (i %ℤ n , x%ℤy<y i n))
+  λ (x , y , p) → fin-ap (divides-diff→same-rem n x y p)
+Finite-ℤ/n n .snd = is-iso→is-equiv $ iso
+  (λ (fin i) → inc (pos i))
+  (λ i → fin-ap (Fin-%ℤ i))
+  (elim! λ i → quot (same-rem→divides-diff n (pos (i %ℤ n)) i
+    (Fin-%ℤ (fin _ ⦃ forget (x%ℤy<y i n) ⦄))))
 ```
 
 Using this and the fact that $([2] \simeq [2]) \simeq [2!] = [2]$,
@@ -229,8 +228,6 @@ equivalences:
 ℤ/2≡S₂ = ∫-Path ℤ/2→S₂ $
   equiv-cancell (Fin-permutations 2 .snd)
     (equiv-cancelr ((Finite-ℤ/n 2 e⁻¹) .snd)
-      (subst is-equiv (ext λ where
-        fzero → refl
-        (fsuc fzero) → refl)
+      (subst is-equiv (ext (indexₚ (refl , refl , tt)))
       id-equiv))
 ```

src/Algebra/Group/NAry.lagda.md

@@ -77,10 +77,11 @@ module _ {ℓ} {T : Type ℓ} (G : Group-on T)  where
     → f i ≡ x
     → (∀ j → ¬ i ≡ j → f j ≡ G.unit)
     → ∑ G f ≡ x
-  ∑-diagonal-lemma {suc n} fzero f f0=x fj=0 =
+  ∑-diagonal-lemma i _ _ _ with fin-view i
+  ∑-diagonal-lemma {suc n} _ f f0=x fj=0 | zero =
     G.elimr ( ∑-path {n = n} G (λ i → fj=0 (fsuc i) fzero≠fsuc)
             ∙ ∑-zero {n = n} G) ∙ f0=x
-  ∑-diagonal-lemma {suc n} (fsuc i) {x} f fj=x f≠i=0 =
+  ∑-diagonal-lemma {suc n} _ {x} f fj=x f≠i=0 | suc i =
     f fzero G.⋆ ∑ {n} G (λ e → f (fsuc e)) ≡⟨ G.eliml (f≠i=0 fzero λ e → fzero≠fsuc (sym e)) ⟩
     ∑ {n} G (λ e → f (fsuc e))             ≡⟨ ∑-diagonal-lemma {n} i (λ e → f (fsuc e)) fj=x (λ j i≠j → f≠i=0 (fsuc j) (λ e → i≠j (fsuc-inj e))) ⟩
     x                                      ∎

src/Algebra/Ring/Module/Multilinear.lagda.md

@@ -354,14 +354,12 @@ proofs of linearity.
     → Multilinear-map (suc n) Ms N
   curry-multilinear-map lin = ml where
     ml : Multilinear-map (suc n) _ _
-    ml .map = λ x → lin .map x .map
-    ml .linearₚ = tabulateₚ λ where
-      fzero xs r x y    →
-        ap (λ e → applyᶠ (e .map) (xs .snd)) (Linear-map.linear lin r x y)
+    ml .map x = lin .map x .map
+    ml .linearₚ = tabulateₚ λ i xs r x y → case fin-view i of λ where
+      zero → ap (λ e → applyᶠ (e .map) (xs .snd)) (Linear-map.linear lin r x y)
         ·· apply-zipᶠ _ _ _ _
         ·· ap₂ N._+_ (apply-mapᶠ _ _ _) refl
-      (fsuc i) xs r x y →
-        linear-at (lin .map (xs .fst)) i (xs .snd) r x y
+      (suc i) → linear-at (lin .map (xs .fst)) i (xs .snd) r x y
 
   uncurry-multilinear-map
     : Multilinear-map (suc n) Ms N

src/Algebra/Ring/Solver.agda

@@ -216,8 +216,9 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   normal-coe {suc n} x = poly (∅ *x+ₙ normal-coe x)
 
   normal-var : ∀ {n} → Fin n → Normal n
-  normal-var fzero    = poly ((∅ *x+ 1n) *x+ 0n)
-  normal-var (fsuc f) = poly (∅ *x+ₙ normal-var f)
+  normal-var i with fin-view i
+  ... | zero  = poly ((∅ *x+ 1n) *x+ 0n)
+  ... | suc f = poly (∅ *x+ₙ normal-var f)
 
   normal : ∀ {n} → Polynomial n → Normal n
   normal (op [+] x y) = normal x +ₙ normal y
@@ -381,12 +382,13 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   sound-coe c (x ∷ ρ) = ∅*x+ₙ-hom (normal-coe c) x ρ ∙ sound-coe c ρ
 
   sound-var : ∀ {n} (j : Fin n) ρ → En (normal-var j) ρ ≡ lookup ρ j
-  sound-var fzero (x ∷ ρ) =
+  sound-var i _ with fin-view i
+  sound-var _ (x ∷ ρ) | zero =
     Ep (∅ *x+ 1n) (x ∷ ρ) R.* x R.+ En 0n ρ ≡⟨ R.elimr (0n-hom ρ) ⟩
     ⌜ Ep (∅ *x+ 1n) (x ∷ ρ) ⌝ R.* x         ≡⟨ ap! (R.eliml R.*-zerol ∙ 1n-hom ρ) ⟩
     R.1r R.* x                              ≡⟨ R.*-idl ⟩
     x                                       ∎
-  sound-var (fsuc j) (x ∷ ρ) = ∅*x+ₙ-hom (normal-var j) x ρ ∙ sound-var j ρ
+  sound-var _ (x ∷ ρ) | suc j = ∅*x+ₙ-hom (normal-var j) x ρ ∙ sound-var j ρ
 
   sound : ∀ {n} (p : Polynomial n) ρ → En (normal p) ρ ≡ ⟦ p ⟧ ρ
   sound (op [+] p q) ρ = +ₙ-hom (normal p) (normal q) ρ ∙ ap₂ R._+_ (sound p ρ) (sound q ρ)

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

@@ -60,9 +60,10 @@ Cartesian→standard-finite-products F = prod where
   F-apex {suc (suc n)} F = F fzero ⊗₀ F-apex (λ e → F (fsuc e))
 
   F-pi : ∀ {n} (F : Fin n → Ob) (i : Fin n) → Hom (F-apex F) (F i)
-  F-pi {suc zero} F fzero       = id
-  F-pi {suc (suc n)} F fzero    = Cart.π₁
-  F-pi {suc (suc n)} F (fsuc i) = F-pi (λ e → F (fsuc e)) i ∘ Cart.π₂
+  F-pi F i with fin-view i
+  F-pi {suc zero}    F .fzero    | zero  = id
+  F-pi {suc (suc n)} F .fzero    | zero  = Cart.π₁
+  F-pi {suc (suc n)} F .(fsuc i) | suc i = F-pi (λ e → F (fsuc e)) i ∘ Cart.π₂
 
   F-mult : ∀ {Y} {n} (F : Fin n → Ob)
          → ((i : Fin n) → Hom Y (F i)) → Hom Y (F-apex F)
@@ -72,9 +73,11 @@ Cartesian→standard-finite-products F = prod where
 
   F-commute : ∀ {Y} {n} (F : Fin n → Ob) (f : (i : Fin n) → Hom Y (F i))
             → ∀ i → F-pi F i ∘ F-mult F f ≡ f i
-  F-commute {n = suc zero} F f fzero = idl (f fzero)
-  F-commute {n = suc (suc n)} F f fzero = Cart.π₁∘⟨⟩
-  F-commute {n = suc (suc n)} F f (fsuc i) = pullr Cart.π₂∘⟨⟩ ∙ F-commute (λ e → F (fsuc e)) (λ e → f (fsuc e)) i
+  F-commute F f i with fin-view i
+  F-commute {n = suc zero}    F f .fzero    | zero = idl (f fzero)
+  F-commute {n = suc (suc n)} F f .fzero    | zero = Cart.π₁∘⟨⟩
+  F-commute {n = suc (suc n)} F f .(fsuc i) | suc i =
+    pullr Cart.π₂∘⟨⟩ ∙ F-commute (λ e → F (fsuc e)) (λ e → f (fsuc e)) i
 
   F-unique
     : ∀ {Y} {n} (F : Fin n → Ob) (f : (i : Fin n) → Hom Y (F i))

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

@@ -3,7 +3,9 @@
 open import Cat.Prelude
 open import Cat.Finite
 
+open import Data.Fin.Product
 open import Data.Fin.Finite
+open import Data.Dec.Base
 open import Data.Fin
 ```
 -->
@@ -12,6 +14,7 @@ open import Data.Fin
 module Cat.Instances.Shape.Cospan where
 ```
 
+
 # The "cospan" category
 
 A _cospan_ in a category $\cC$ is a pair of morphisms $a \xto{f} c
@@ -97,12 +100,8 @@ instance
     i .fst cs-a = 0
     i .fst cs-b = 1
     i .fst cs-c = 2
-    i .snd .is-iso.inv fzero = cs-a
-    i .snd .is-iso.inv (fsuc fzero) = cs-b
-    i .snd .is-iso.inv (fsuc (fsuc fzero)) = cs-c
-    i .snd .is-iso.rinv fzero = refl
-    i .snd .is-iso.rinv (fsuc fzero) = refl
-    i .snd .is-iso.rinv (fsuc (fsuc fzero)) = refl
+    i .snd .is-iso.inv = indexₚ (cs-a , cs-b , cs-c , tt)
+    i .snd .is-iso.rinv = indexₚ (refl , refl , refl , tt)
     i .snd .is-iso.linv cs-a = refl
     i .snd .is-iso.linv cs-b = refl
     i .snd .is-iso.linv cs-c = refl

src/Cat/Instances/Simplex.lagda.md

@@ -46,7 +46,7 @@ unquoteDecl H-Level-Δ-map = declare-record-hlevel 2 H-Level-Δ-map (quote Δ-ma
   → f ≡ g
 Δ-map-path p i .map x = p x i
 Δ-map-path {f = f} {g} p i .ascending x y w =
-  is-prop→pathp (λ j → Nat.≤-is-prop {to-nat (p x j)} {to-nat (p y j)})
+  is-prop→pathp (λ j → Nat.≤-is-prop {p x j .lower} {p y j .lower})
     (f .ascending x y w) (g .ascending x y w) i
 ```
 -->