diff --git a/src/1Lab/Reflection/Induction/Examples.agda b/src/1Lab/Reflection/Induction/Examples.agda index 6f2320f32..a56eb585e 100644 --- a/src/1Lab/Reflection/Induction/Examples.agda +++ b/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} diff --git a/src/1Lab/Reflection/Variables.agda b/src/1Lab/Reflection/Variables.agda index 16003f015..5cc9cb501 100644 --- a/src/1Lab/Reflection/Variables.agda +++ b/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)) → diff --git a/src/1Lab/Type.lagda.md b/src/1Lab/Type.lagda.md index 7e564842e..2564a2aa7 100644 --- a/src/1Lab/Type.lagda.md +++ b/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ω () ``` --> diff --git a/src/Algebra/Group/Instances/Cyclic.lagda.md b/src/Algebra/Group/Instances/Cyclic.lagda.md index ec0aed61c..f761f8ed5 100644 --- a/src/Algebra/Group/Instances/Cyclic.lagda.md +++ b/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≃ℕ @@ -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 diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index 7456e99bf..47badd23c 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/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 ``` --> diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md index 32c0426b9..27225e65a 100644 --- a/src/Data/Fin/Base.lagda.md +++ b/src/Data/Fin/Base.lagda.md @@ -10,6 +10,9 @@ open import 1Lab.Type open import Data.Dec.Base open import Data.Sum.Base open import Data.Id.Base +open import Data.Irr + +open import Meta.Idiom import Data.Nat.Base as Nat ``` @@ -21,59 +24,135 @@ module Data.Fin.Base where # Finite sets {defines=standard-finite-set} -The type `Fin`{.Agda} is the type of size `n`. These are defined as an -inductive family over `Nat`{.Agda}, such that `Fin 0` has 0 elements, -`Fin 1` has 1 element, and so on. +The type $\operatorname{Fin}(n)$ is the type with exactly $n$ elements. +We define it as a record type, packaging a natural number $k$ with a +proof that $k \lt n$. + +```agda +record Fin (n : Nat) : Type where + constructor fin + field + lower : Nat + ⦃ bounded ⦄ : Irr (lower Nat.< n) +``` + +While the type $k \lt n$ is a [[homotopy proposition|proposition]], we +would like to enforce that constructions on $\operatorname{Fin}(n)$ +*definitionally* do not depend on the given proof. Therefore, we have +wrapped it in `Irr`{.Agda}. + +In dependent type theory, it's common to instead define the finite sets +as an inductive family indexed over `Nat`{.Agda}. However, in cubical +type theory, there is a good reason to avoid inductive families: they +have `subst`{.Agda} as an additional constructor, *including* along +constant paths. This makes the normal form of any expression involving +substitution in an indexed family, even if the thing being transported +is a constructor form, very bad. + +Instead, we would like the `subst`{.Agda} operation on `Fin`{.Agda} to +definitionally commute with the constructors, and (if possible) to +definitionally preserve the underlying numeric value. Defining +`Fin`{.Agda} as an indexed type with an irrelevant proof field achieves +exactly this: -Another way to view `Fin`{.Agda} is as the type of numbers less than -some upper bound. For instance, `fsuc fzero` is of type `Fin 3`, but -will _not_ typecheck as a `Fin 1`! +```agda +private + cast : ∀ {m n} → m ≡ n → Fin m → Fin n + cast p (fin n ⦃ i ⦄) = record + { lower = n + ; bounded = subst (n Nat.<_) p <$> i + } + + _ : ∀ {m n} {p : m ≡ n} {x : Fin m} → subst Fin p x ≡ cast p x + _ = refl +``` + -Keeping with the perspective of `Fin`{.Agda} as a type of bounded -natural numbers, we provide conversion functions going back and forth. +We can still *prove* that the definition above is equivalent to an +inductive family. In particular, it's generated by the "constructors" +`fzero`{.Agda} and `fsuc`{.Agda}. +```agda +_ : ∀ {n} → Fin (suc n) +_ = fzero + +fsuc : ∀ {n} → Fin n → Fin (suc n) +fsuc (fin n ⦃ x ⦄) = fin (suc n) ⦃ Nat.s≤s <$> x ⦄ +``` + + + +## Viewing elements of a finite set + +Agda has good support, through the `with`{.Agda} abstraction, to pretend +that a type is inductively generated. We therefore expose a type +`Fin-view`{.Agda} which allows us to discriminate on whether an element +of $\operatorname{Fin}(n)$ is `fzero`{.Agda} or `fsuc`{.Agda}. + +```agda +data Fin-view : {n : Nat} → Fin n → Type where + zero : ∀ {n} → Fin-view {suc n} fzero + suc : ∀ {n} (i : Fin n) → Fin-view {suc n} (fsuc i) +``` + +Of course, this family has a section, expressing that any finite number +is generated by one of the two "constructors". + +```agda +fin-view : ∀ {n} (i : Fin n) → Fin-view i +fin-view {suc n} fzero = zero +fin-view {suc n} (fin (suc i) ⦃ b ⦄) = suc (fin i ⦃ Nat.≤-peel <$> b ⦄) + +fin-view {zero} (fin _ ⦃ forget i ⦄) = absurd (Nat.¬suc≤0 i) ``` -A note of caution: because of some ✨technical reasons✨ cubical -agda cannot handle transports over indexed inductive types very well. -Instead, we define a function `cast`{.Agda} that computes on -the indices of `Fin`{.Agda}, rather than on the path. +As a first application, we can prove that `Fin 0` is empty: ```agda -cast : ∀ {m n} → m ≡ n → Fin m → Fin n -cast {suc m} {zero} p fzero = absurd (Nat.suc≠zero p) -cast {suc m} {suc n} p fzero = fzero -cast {suc m} {zero} p (fsuc i) = absurd (Nat.suc≠zero p) -cast {suc m} {suc n} p (fsuc i) = fsuc (cast (Nat.suc-inj p) i) +Fin-absurd : Fin 0 → ⊥ +Fin-absurd i with fin-view i +... | () +``` + +We can also define an elimination principle for the family +$\operatorname{Fin}(-)$, which applies the view at "every level". + +```agda +Fin-elim + : ∀ {ℓ} (P : ∀ {n} → Fin n → Type ℓ) + → (∀ {n} → P {suc n} fzero) + → (∀ {i} (j : Fin i) → P j → P (fsuc j)) + → ∀ {n} (i : Fin n) → P i +Fin-elim P pfzero pfsuc i with fin-view i +... | zero = pfzero +... | suc i = pfsuc i (Fin-elim P pfzero pfsuc i) ``` @@ -83,9 +162,11 @@ on some `Fin n`. ```agda strengthen : ∀ {n} → Fin (suc n) → Fin (suc n) ⊎ Fin n -strengthen {n = zero} fzero = inl fzero -strengthen {n = suc n} fzero = inr fzero -strengthen {n = suc n} (fsuc i) = ⊎-map fsuc fsuc (strengthen i) +strengthen {n = zero} k with fin-view k +... | vzero = inl fzero +strengthen {n = suc n} k with fin-view k +... | zero = inr fzero +... | suc i = ⊎-map fsuc fsuc (strengthen i) ``` On the other hand, `weaken`{.Agda} does the opposite: it relaxes @@ -94,68 +175,34 @@ the upper bound on some `Fin n`, allowing us to regard it as a ```agda weaken : ∀ {n} → Fin n → Fin (suc n) -weaken fzero = fzero -weaken (fsuc i) = fsuc (weaken i) +weaken n with fin-view n +... | zero = fzero +... | suc i = fsuc (weaken i) ``` We can also relax the upper bounds if `m ≤ n`. ```agda inject : ∀ {m n} → m Nat.≤ n → Fin m → Fin n -inject {_} {suc n} le fzero = fzero -inject {_} {suc n} (Nat.s≤s le) (fsuc i) = fsuc (inject le i) +inject p (fin n ⦃ b ⦄) = fin n ⦃ (λ e → Nat.≤-trans e p) <$> b ⦄ ``` ## Discreteness -The proof here mirrors the one found in [`Data.Nat.Base`], -just with some slight tweaks required to handle the indexing. - -[`Data.Nat.Base`]: Data.Nat.Base.html - -We begin by showing that one can `distinguish`{.Agda} zero -from successor: - -```agda -fzero≠fsuc : ∀ {n} {i : Fin n} → ¬ fzero ≡ fsuc i -fzero≠fsuc {n = n} path = subst distinguish path tt where - distinguish : Fin (suc n) → Type - distinguish fzero = ⊤ - distinguish (fsuc _) = ⊥ -``` - -Next, we show that `fsuc` is injective. This again follows -the proof in [`Data.Nat.Base`], but some extra care must be -taken to ensure that `pred`{.Agda} is well typed! - -[`Data.Nat.Base`]: Data.Nat.Base.html - -```agda -fsuc-inj : ∀ {n} {i j : Fin n} → fsuc i ≡ fsuc j → i ≡ j -fsuc-inj {n = suc n} p = ap pred p - where - pred : Fin (suc (suc n)) → Fin (suc n) - pred fzero = fzero - pred (fsuc i) = i -``` - -Finally, we pull everything together to show that `Fin`{.Agda} is -`Discrete`{.Agda}. This is not exactly a shock (after all, `Nat`{.Agda} -is discrete), but it's useful nonetheless! +Since the finite set of size $n$ is a subset of the natural numbers, +which have decidable equality, it follows that $\operatorname{Fin}(n)$ +also has decidable equality. ```agda instance Discrete-Fin : ∀ {n} → Discrete (Fin n) - Discrete-Fin {x = fzero} {fzero} = yes refl - Discrete-Fin {x = fzero} {fsuc j} = no fzero≠fsuc - Discrete-Fin {x = fsuc i} {fzero} = no (fzero≠fsuc ∘ sym) - Discrete-Fin {x = fsuc i} {fsuc j} with Discrete-Fin {x = i} {j} - ... | yes p = yes (ap fsuc p) - ... | no ¬i≡j = no λ si=sj → ¬i≡j (fsuc-inj si=sj) + Discrete-Fin {x = x} {y} with x .lower ≡? y .lower + ... | yes p = yes (fin-ap p) + ... | no ¬p = no λ p → ¬p (ap lower p) ``` -[[Hedberg's theorem]] implies that `Fin`{.Agda} is a [[set]], i.e., it only -has trivial paths. +In particular, [[Hedberg's theorem]] shows that $\operatorname{Fin}(n)$ +is a set. ```agda opaque @@ -167,32 +214,51 @@ instance H-Level-Fin = basic-instance 2 Fin-is-set ``` +However, we can also mimic parts of the proof that `Nat`{.Agda} itself +is discrete, and obtain useful combinators for reasoning with finite +sets. For example, the zero element in $\operatorname{Fin}(1 + n)$ is +never equal to a successor: + +```agda +fzero≠fsuc : ∀ {n k p} → ¬ Path (Fin (suc n)) fzero (fin (suc k) ⦃ p ⦄) +fzero≠fsuc p = Nat.zero≠suc (ap lower p) + +``` + + +Moreover, since we can implement a "predecessor" operation, we get that +`fsuc`{.Agda} is an injection. + +```agda +fsuc-inj : ∀ {n} {i j : Fin n} → fsuc i ≡ fsuc j → i ≡ j +fsuc-inj {n = suc n} p = ap pred p where + pred : Fin (suc (suc n)) → Fin (suc n) + pred n with fin-view n + ... | zero = fzero + ... | suc i = i +``` + @@ -206,11 +272,11 @@ sets. ```agda _≤_ : ∀ {n} → Fin n → Fin n → Type -i ≤ j = to-nat i Nat.≤ to-nat j +i ≤ j = i .lower Nat.≤ j .lower infix 7 _≤_ _<_ : ∀ {n} → Fin n → Fin n → Type -i < j = to-nat i Nat.< to-nat j +i < j = i .lower Nat.< j .lower infix 7 _<_ ``` @@ -222,72 +288,44 @@ mapping both `i` and `i+1` to `i`. Its counterpart `skip i` takes some ```agda squish : ∀ {n} → Fin n → Fin (suc n) → Fin n -squish fzero fzero = fzero -squish fzero (fsuc j) = j -squish (fsuc i) fzero = fzero -squish (fsuc i) (fsuc j) = fsuc (squish i j) +squish n k with fin-view n | fin-view k +... | zero | zero = fzero +... | zero | suc j = j +... | suc i | zero = fzero +... | suc i | suc j = fsuc (squish i j) skip : ∀ {n} → Fin (suc n) → Fin n → Fin (suc n) -skip fzero j = fsuc j -skip (fsuc i) fzero = fzero -skip (fsuc i) (fsuc j) = fsuc (skip i j) -``` - -## As a subset - -While `Fin`{.Agda} is very conveniently defined as an indexed family of -types, it can also be defined as a subset of the natural numbers: -Namely, the finite ordinal $[n]$ is the same type as as $\{ x : x < n -\}$. This makes sense! Any set with $n$ elements is equivalent to any -other set with $n$ elements, and a very canonical choice is the first -$n$ values of $\bb{N}$. - -```agda -ℕ< : Nat → Type -ℕ< x = Σ[ n ∈ Nat ] n Nat.< x - -from-ℕ< : ∀ {n} → ℕ< n → Fin n -from-ℕ< {n = suc n} (zero , q) = fzero -from-ℕ< {n = suc n} (suc p , Nat.s≤s q) = fsuc (from-ℕ< (p , q)) - -to-ℕ< : ∀ {n} → Fin n → ℕ< n -to-ℕ< x = to-nat x , p x where - p : ∀ {n} (x : Fin n) → suc (to-nat x) Nat.≤ n - p {n = suc n} fzero = Nat.s≤s Nat.0≤x - p {n = suc n} (fsuc x) = Nat.s≤s (p x) +skip n k with fin-view n +... | zero = fsuc k +... | suc i with fin-view k +... | zero = fzero +... | suc j = fsuc (skip i j) ``` ## Arithmetic ```agda -weaken-≤ : ∀ {m n} → m Nat.≤ n → Fin m → Fin n -weaken-≤ {suc m} {suc n} m≤n fzero = fzero -weaken-≤ {suc m} {suc n} (Nat.s≤s m≤n) (fsuc i) = fsuc (weaken-≤ m≤n i) - -shift-≤ : ∀ {m n} → m Nat.≤ n → Fin m → Fin n -shift-≤ {n = suc zero} (Nat.s≤s 0≤x) i = i -shift-≤ {n = suc (suc n)} (Nat.s≤s 0≤x) i = fsuc (shift-≤ (Nat.s≤s 0≤x) i) -shift-≤ {n = n} (Nat.s≤s (Nat.s≤s m≤n)) fzero = weaken (shift-≤ (Nat.s≤s m≤n) fzero) -shift-≤ {n = n} (Nat.s≤s (Nat.s≤s m≤n)) (fsuc i) = fsuc (shift-≤ (Nat.s≤s m≤n) i) - split-+ : ∀ {m n} → Fin (m + n) → Fin m ⊎ Fin n split-+ {m = zero} i = inr i -split-+ {m = suc m} fzero = inl fzero -split-+ {m = suc m} (fsuc i) = ⊎-map fsuc id (split-+ i) +split-+ {m = suc m} k with fin-view k +... | zero = inl fzero +... | suc i = ⊎-map fsuc id (split-+ i) avoid : ∀ {n} (i j : Fin (suc n)) → i ≠ j → Fin n -avoid fzero fzero i≠j = absurd (i≠j refl) -avoid {n = suc n} fzero (fsuc j) i≠j = j -avoid {n = suc n} (fsuc i) fzero i≠j = fzero -avoid {n = suc n} (fsuc i) (fsuc j) i≠j = fsuc (avoid i j (i≠j ∘ ap fsuc)) +avoid {n = n} i j i≠j with fin-view i | fin-view j +... | zero | zero = absurd (i≠j refl) +... | zero | suc j = j +avoid {n = suc n} _ _ i≠j | suc i | zero = fzero +avoid {n = suc n} _ _ i≠j | suc i | suc j = fsuc (avoid i j (i≠j ∘ ap fsuc)) fshift : ∀ {n} (m : Nat) → Fin n → Fin (m + n) -fshift zero i = i +fshift zero i = i fshift (suc m) i = fsuc (fshift m i) opposite : ∀ {n} → Fin n → Fin n -opposite {n = suc n} fzero = from-nat n -opposite {n = suc n} (fsuc i) = weaken (opposite i) +opposite {n = n} i with fin-view i +opposite {n = suc n} _ | zero = from-nat n +opposite {n = suc n} _ | suc i = weaken (opposite i) ``` ## Vector operations @@ -297,10 +335,11 @@ _[_≔_] : ∀ {ℓ} {A : Type ℓ} {n} → (Fin n → A) → Fin (suc n) → A → Fin (suc n) → A -_[_≔_] {n = n} ρ fzero a fzero = a -_[_≔_] {n = n} ρ fzero a (fsuc j) = ρ j -_[_≔_] {n = suc n} ρ (fsuc i) a fzero = ρ fzero -_[_≔_] {n = suc n} ρ (fsuc i) a (fsuc j) = ((ρ ∘ fsuc) [ i ≔ a ]) j +_[_≔_] {n = n} p i a j with fin-view i | fin-view j +_[_≔_] {n = n} ρ fzero a fzero | zero | zero = a +_[_≔_] {n = n} ρ fzero a .(fsuc j) | zero | suc j = ρ j +_[_≔_] {n = suc n} ρ .(fsuc i) a .fzero | suc i | zero = ρ fzero +_[_≔_] {n = suc n} ρ .(fsuc i) a .(fsuc j) | suc i | suc j = ((ρ ∘ fsuc) [ i ≔ a ]) j delete : ∀ {ℓ} {A : Type ℓ} {n} diff --git a/src/Data/Fin/Closure.lagda.md b/src/Data/Fin/Closure.lagda.md index 12b460aaf..7eca9cf9b 100644 --- a/src/Data/Fin/Closure.lagda.md +++ b/src/Data/Fin/Closure.lagda.md @@ -2,11 +2,13 @@ ```agda open import 1Lab.Prelude +open import Data.Maybe.Properties open import Data.Set.Coequaliser open import Data.Fin.Properties open import Data.Fin.Base open import Data.Nat.Base open import Data.Dec +open import Data.Irr open import Data.Sum open import Meta.Invariant @@ -50,7 +52,8 @@ Finite-zero-is-initial .snd .is-eqv () Finite-one-is-contr : is-contr (Fin 1) Finite-one-is-contr .centre = fzero -Finite-one-is-contr .paths fzero = refl +Finite-one-is-contr .paths i with fin-view i +... | zero = refl ``` The successor operation on indices corresponds to taking coproducts with @@ -58,22 +61,7 @@ the unit set. ```agda Finite-successor : Fin (suc n) ≃ (⊤ ⊎ Fin n) -Finite-successor {n} = Iso→Equiv (f , iso g f-g g-f) where - f : Fin (suc n) → ⊤ ⊎ Fin n - f fzero = inl tt - f (fsuc x) = inr x - - g : ⊤ ⊎ Fin n → Fin (suc n) - g (inr x) = fsuc x - g (inl _) = fzero - - f-g : is-right-inverse g f - f-g (inr _) = refl - f-g (inl _) = refl - - g-f : is-left-inverse g f - g-f fzero = refl - g-f (fsuc x) = refl +Finite-successor {n} = Fin-suc ∙e Maybe-is-sum ``` ## Addition @@ -128,7 +116,7 @@ binary products: Finite-multiply : (Fin n × Fin m) ≃ Fin (n * m) Finite-multiply {n} {m} = (Fin n × Fin m) ≃⟨ Finite-sum (λ _ → m) ⟩ - Fin (sum n (λ _ → m)) ≃⟨ cast (sum≡* n m) , cast-is-equiv _ ⟩ + Fin (sum n (λ _ → m)) ≃⟨ path→equiv (ap Fin (sum≡* n m)) ⟩ Fin (n * m) ≃∎ where sum≡* : ∀ n m → sum n (λ _ → m) ≡ n * m @@ -149,9 +137,11 @@ product (suc n) f = f fzero * product n (f ∘ fsuc) Finite-product : (B : Fin n → Nat) → (∀ x → Fin (B x)) ≃ Fin (product n B) Finite-product {zero} B .fst _ = fzero Finite-product {zero} B .snd = is-iso→is-equiv λ where - .is-iso.inv _ () - .is-iso.rinv fzero → refl + .is-iso.inv _ () .is-iso.linv _ → funext λ () + + .is-iso.rinv fzero → refl + .is-iso.rinv (fin (suc i) ⦃ forget p ⦄) → absurd (¬suc≤0 (≤-peel p)) Finite-product {suc n} B = (∀ x → Fin (B x)) ≃⟨ Fin-suc-Π ⟩ Fin (B fzero) × (∀ x → Fin (B (fsuc x))) ≃⟨ Σ-ap-snd (λ _ → Finite-product (B ∘ fsuc)) ⟩ @@ -175,22 +165,29 @@ Fin-permutations-suc n = to , is-iso→is-equiv is where to : (Fin (suc n) ≃ Fin (suc n)) → Fin (suc n) × (Fin n ≃ Fin n) to e .fst = e # 0 to e .snd .fst i = avoid (e # 0) (e # (fsuc i)) λ p → - fzero≠fsuc (Equiv.injective e p) + zero≠suc (ap lower (Equiv.injective e p)) to e .snd .snd = Fin-injection→equiv _ λ p → fsuc-inj (Equiv.injective e (avoid-injective (e # 0) p)) is : is-iso to - is .is-iso.inv (n , e) .fst fzero = n - is .is-iso.inv (n , e) .fst (fsuc x) = skip n (e # x) - is .is-iso.inv (n , e) .snd = Fin-injection→equiv _ λ where - {fzero} {fzero} p → refl - {fzero} {fsuc y} p → absurd (skip-skips n _ (sym p)) - {fsuc x} {fzero} p → absurd (skip-skips n _ p) - {fsuc x} {fsuc y} p → ap fsuc (Equiv.injective e (skip-injective n _ _ p)) + is .is-iso.inv (n , e) = record { fst = fun ; snd = Fin-injection→equiv _ inj } module inv where + fun : Fin (suc _) → Fin (suc _) + fun i with fin-view i + ... | zero = n + ... | suc x = skip n (e # x) + + inj : injective fun + inj {i} {j} p with fin-view i | fin-view j + ... | zero | zero = refl + ... | zero | suc y = absurd (skip-skips n _ (sym p)) + ... | suc i | zero = absurd (skip-skips n _ p) + ... | suc i | suc j = ap fsuc (Equiv.injective e (skip-injective n _ _ p)) is .is-iso.rinv (n , e) = Σ-pathp refl (ext λ i → avoid-skip n (e # i)) - is .is-iso.linv e = ext λ where - fzero → refl - (fsuc i) → skip-avoid (e # 0) (e # (fsuc i)) + is .is-iso.linv e = ext p where + p : ∀ x → inv.fun (e # 0) (to e .snd) x ≡ e .fst x + p x with fin-view x + ... | zero = refl + ... | suc i = skip-avoid (e # 0) (e # fsuc i) ``` We can now show that $([n] \simeq [n]) \simeq [n!]$ by induction. @@ -292,16 +289,19 @@ the quotient remains unchanged. go ⦃ yes (i , r) ⦄ .snd = n/R₁ .snd ∙e Iso→Equiv is where is : Iso (Fin n / R₁._∼_) (Fin (suc n) / R._∼_) is .fst = Coeq-rec (λ x → inc (fsuc x)) λ (x , y , s) → quot s - is .snd .inv = Coeq-rec - (λ where fzero → inc i - (fsuc x) → inc x) - (λ where (fzero , fzero , s) → refl - (fzero , fsuc y , s) → quot (R.symᶜ r R.∙ᶜ s) - (fsuc x , fzero , s) → quot (s R.∙ᶜ r) - (fsuc x , fsuc y , s) → quot s) - is .snd .rinv = elim! λ where - fzero → quot (R.symᶜ r) - (fsuc x) → refl + is .snd .inv = Coeq-rec fn λ (i , j , s) → resp i j s where + fn : Fin (suc n) → Fin n / R₁._∼_ + fn j with fin-view j + ... | zero = inc i + ... | suc x = inc x + + resp : ∀ i j → i R.∼ j → fn i ≡ fn j + resp i j s with fin-view i | fin-view j + ... | zero | zero = refl + ... | zero | suc y = quot (R.symᶜ r R.∙ᶜ s) + ... | suc x | zero = quot (s R.∙ᶜ r) + ... | suc x | suc y = quot s + is .snd .rinv = elim! (Fin-cases (quot (R.symᶜ r)) (λ _ → refl)) is .snd .linv = elim! λ _ → refl ``` @@ -311,21 +311,22 @@ Otherwise, $0$ creates a new equivalence class for itself. go ⦃ no ¬r ⦄ .fst = suc (n/R₁ .fst) go ⦃ no ¬r ⦄ .snd = Finite-successor ∙e ⊎-apr (n/R₁ .snd) ∙e Iso→Equiv is where to : Fin (suc n) → ⊤ ⊎ (Fin n / R₁._∼_) - to fzero = inl _ - to (fsuc x) = inr (inc x) + to i with fin-view i + ... | zero = inl _ + ... | suc x = inr (inc x) + + resp : ∀ i j → i R.∼ j → to i ≡ to j + resp i j s with fin-view i | fin-view j + ... | zero | zero = refl + ... | zero | suc y = absurd (¬r (y , s)) + ... | suc x | zero = absurd (¬r (x , R.symᶜ s)) + ... | suc x | suc y = ap inr (quot s) is : Iso (⊤ ⊎ (Fin n / R₁._∼_)) (Fin (suc n) / R._∼_) is .fst (inl tt) = inc 0 is .fst (inr x) = Coeq-rec (λ x → inc (fsuc x)) (λ (x , y , s) → quot s) x - is .snd .inv = Coeq-rec to λ where - (fzero , fzero , s) → refl - (fzero , fsuc y , s) → absurd (¬r (y , s)) - (fsuc x , fzero , s) → absurd (¬r (x , R.symᶜ s)) - (fsuc x , fsuc y , s) → ap inr (quot s) - is .snd .rinv = elim! go' where - go' : ∀ x → is .fst (to x) ≡ inc x - go' fzero = refl - go' (fsuc _) = refl + is .snd .inv = Coeq-rec to λ (x , y , r) → resp x y r + is .snd .rinv = elim! (Fin-cases refl (λ _ → refl)) is .snd .linv (inl tt) = refl is .snd .linv (inr x) = elim x where elim : ∀ x → is .snd .inv (is .fst (inr x)) ≡ inr x @@ -366,7 +367,7 @@ $[n] \to [n+1]$, written $R_1$, as well as the *symmetric closure* of $R$, written $R^s$. ```agda - Closure-Fin-Dec {suc n} {R = R} {x} {y} = R*-dec where + Closure-Fin-Dec {suc n} {ℓ} {R} {x} {y} = R*-dec where open Congruence module R = Congruence (Closure-congruence R) @@ -388,8 +389,8 @@ written $R^s$. We build $D$ by cases. $D(0, 0)$ is trivial, since the closure is reflexive. ```agda - D : Fin (suc n) → Fin (suc n) → Type _ - D fzero fzero = Lift _ ⊤ + D' : {i j : Fin (suc n)} → Fin-view i → Fin-view j → Type ℓ + D' zero zero = Lift _ ⊤ ``` For $D(0, y+1)$, we use the omniscience of $[n]$ to search for an $x$ @@ -398,8 +399,8 @@ of $R_1$ being decidable by the induction hypothesis. The case $D(x+1, 0)$ is symmetric. ```agda - D fzero (fsuc y) = Σ[ x ∈ Fin n ] Rˢ 0 (fsuc x) × Closure R₁ x y - D (fsuc x) fzero = Σ[ y ∈ Fin n ] Closure R₁ x y × Rˢ (fsuc y) 0 + D' zero (suc y) = Σ[ x ∈ Fin n ] Rˢ 0 (fsuc x) × Closure R₁ x y + D' (suc x) zero = Σ[ y ∈ Fin n ] Closure R₁ x y × Rˢ (fsuc y) 0 ``` Finally, in order to decide whether $x+1$ and $y+1$ are related by $R^*$, @@ -409,9 +410,16 @@ are paths from $x+1$ to $0$ and from $0$ to $y+1$ in $[n+1]$, which we can find using the previous two cases. ```agda - D (fsuc x) (fsuc y) = Closure R₁ x y ⊎ D (fsuc x) 0 × D 0 (fsuc y) + D' (suc x) (suc y) = Closure R₁ x y ⊎ D' (suc x) zero × D' zero (suc y) ``` + +
Proving that (the [[propositional truncation]] of) $D$ is a decidable @@ -425,45 +433,48 @@ congruence is tedious but not difficult. ```agda D-refl : ∀ x → D x x - D-refl fzero = _ - D-refl (fsuc x) = inl R₁.reflᶜ + D-refl i with fin-view i + ... | zero = _ + ... | suc x = inl R₁.reflᶜ D-trans : ∀ x y z → D x y → D y z → D x z - D-trans fzero fzero z _ d = d - D-trans fzero (fsuc y) fzero _ _ = _ - D-trans fzero (fsuc y) (fsuc z) (y' , ry , cy) (inl c) = y' , ry , cy R₁.∙ᶜ c - D-trans fzero (fsuc y) (fsuc z) _ (inr (_ , dz)) = dz - D-trans (fsuc x) fzero fzero d _ = d - D-trans (fsuc x) fzero (fsuc z) dx dy = inr (dx , dy) - D-trans (fsuc x) (fsuc y) fzero (inl c) (y' , cy , ry) = y' , c R₁.∙ᶜ cy , ry - D-trans (fsuc x) (fsuc y) fzero (inr (dx , _)) _ = dx - D-trans (fsuc x) (fsuc y) (fsuc z) (inl c) (inl d) = inl (c R₁.∙ᶜ d) - D-trans (fsuc x) (fsuc y) (fsuc z) (inl c) (inr ((y' , cy , ry) , dz)) = - inr ((y' , c R₁.∙ᶜ cy , ry) , dz) - D-trans (fsuc x) (fsuc y) (fsuc z) (inr (dx , (y' , ry , cy))) (inl c) = - inr (dx , y' , ry , cy R₁.∙ᶜ c) - D-trans (fsuc x) (fsuc y) (fsuc z) (inr (dx , dy)) (inr (dy' , dz)) = - inr (dx , dz) - - D-sym : ∀ x y → D x y → D y x - D-sym fzero fzero _ = _ - D-sym fzero (fsuc y) (y' , r , c) = y' , R₁.symᶜ c , ⊎-comm .fst r - D-sym (fsuc x) fzero (x' , c , r) = x' , ⊎-comm .fst r , R₁.symᶜ c - D-sym (fsuc x) (fsuc y) (inl r) = inl (R₁.symᶜ r) - D-sym (fsuc x) (fsuc y) (inr (dx , dy)) = - inr (D-sym fzero (fsuc y) dy , D-sym (fsuc x) fzero dx) + D-trans i j k p q with fin-view i | fin-view j | fin-view k | p | q + ... | zero | zero | z | _ | d = d + ... | zero | suc y | zero | _ | _ = _ + ... | zero | suc y | suc z | y' , ry , cy | inl c = y' , ry , cy R₁.∙ᶜ c + ... | zero | suc y | suc z | _ | inr (_ , dz) = dz + ... | suc x | zero | zero | d | _ = d + ... | suc x | zero | suc z | dx | dy = inr (dx , dy) + ... | suc x | suc y | zero | inl c | y' , cy , ry = y' , c R₁.∙ᶜ cy , ry + ... | suc x | suc y | zero | inr (dx , _) | _ = dx + ... | suc x | suc y | suc z | inl c | inl d = inl (c R₁.∙ᶜ d) + ... | suc x | suc y | suc z | inl c | inr ((y' , cy , ry) , dz) = + inr ((y' , c R₁.∙ᶜ cy , ry) , dz) + ... | suc x | suc y | suc z | inr (dx , (y' , ry , cy)) | inl c = + inr (dx , y' , ry , cy R₁.∙ᶜ c) + ... | suc x | suc y | suc z | inr (dx , dy) | inr (dy' , dz) = + inr (dx , dz) + + D-sym : ∀ {i j} (x : Fin-view i) (y : Fin-view j) → D' x y → D' y x + D-sym zero zero _ = _ + D-sym zero (suc y) (y' , r , c) = y' , R₁.symᶜ c , ⊎-comm .fst r + D-sym (suc x) zero (x' , c , r) = x' , ⊎-comm .fst r , R₁.symᶜ c + D-sym (suc x) (suc y) (inl r) = inl (R₁.symᶜ r) + D-sym (suc x) (suc y) (inr (dx , dy)) = + inr (D-sym zero (suc y) dy , D-sym (suc x) zero dx) D-cong ._∼_ x y = ∥ D x y ∥ D-cong .has-is-prop _ _ = hlevel 1 D-cong .reflᶜ {x} = inc (D-refl x) D-cong ._∙ᶜ_ {x} {y} {z} = ∥-∥-map₂ (D-trans x y z) - D-cong .symᶜ {x} {y} = map (D-sym x y) + D-cong .symᶜ {x} {y} = map (D-sym (fin-view x) (fin-view y)) {-# INCOHERENT D-Dec #-} - D-Dec {fzero} {fzero} = auto - D-Dec {fzero} {fsuc y} = auto - D-Dec {fsuc x} {fzero} = auto - D-Dec {fsuc x} {fsuc y} = auto + D-Dec {i} {j} with fin-view i | fin-view j + ... | zero | zero = auto + ... | zero | suc y = auto + ... | suc x | zero = auto + ... | suc x | suc y = auto ```
@@ -472,17 +483,19 @@ it suffices to show that $D$ lies between $R$ and $R^*$. ```agda R→D : ∀ {x y} → R x y → D x y - R→D {fzero} {fzero} _ = _ - R→D {fzero} {fsuc y} r = y , inl r , R₁.reflᶜ - R→D {fsuc x} {fzero} r = x , R₁.reflᶜ , inl r - R→D {fsuc x} {fsuc y} r = inl (inc r) - - D→R* : ∀ {x y} → D x y → Closure R x y - D→R* {fzero} {fzero} _ = R.reflᶜ - D→R* {fzero} {fsuc y} (y' , r , c) = Rˢ→R r R.∙ᶜ R₁→R c - D→R* {fsuc x} {fzero} (x' , c , r) = R₁→R c R.∙ᶜ Rˢ→R r - D→R* {fsuc x} {fsuc y} (inl r) = R₁→R r - D→R* {fsuc x} {fsuc y} (inr (dx , dy)) = D→R* dx R.∙ᶜ D→R* {fzero} dy + R→D {i} {j} r with fin-view i | fin-view j + ... | zero | zero = _ + ... | zero | suc y = y , inl r , R₁.reflᶜ + ... | suc x | zero = x , R₁.reflᶜ , inl r + ... | suc x | suc y = inl (inc r) + + D→R* : ∀ {x y i j} → D' {x} {y} i j → Closure R x y + D→R* {i = zero} {j = zero} _ = R.reflᶜ + D→R* {i = zero} {j = suc y} (y' , r , c) = Rˢ→R r R.∙ᶜ R₁→R c + D→R* {i = suc x} {j = zero} (x' , c , r) = R₁→R c R.∙ᶜ Rˢ→R r + D→R* {i = suc x} {j = suc y} (inl r) = R₁→R r + D→R* {i = suc x} {j = suc y} (inr (dx , dy)) = + D→R* {i = suc x} {j = zero} dx R.∙ᶜ D→R* {i = zero} {suc y} dy R*→D : ∀ {x y} → Closure R x y → ∥ D x y ∥ R*→D = Closure-rec-congruence R D-cong (inc ∘ R→D) diff --git a/src/Data/Fin/Finite.lagda.md b/src/Data/Fin/Finite.lagda.md index 1c158cb73..c85e1b9fa 100644 --- a/src/Data/Fin/Finite.lagda.md +++ b/src/Data/Fin/Finite.lagda.md @@ -4,12 +4,15 @@ open import 1Lab.Prelude open import Algebra.Group.Homotopy.BAut +open import Data.Maybe.Properties open import Data.Set.Coequaliser open import Data.Fin.Properties open import Data.Fin.Closure open import Data.Fin.Base open import Data.Nat.Base +open import Data.Maybe open import Data.Dec +open import Data.Irr open import Data.Sum ``` --> @@ -157,7 +160,7 @@ same-cardinality→equiv same-cardinality→equiv ⦃ fa ⦄ ⦃ fb ⦄ p = do ea ← fa .Finite.enumeration eb ← fb .Finite.enumeration - pure (ea ∙e (_ , cast-is-equiv p) ∙e eb e⁻¹) + pure (ea ∙e path→equiv (ap Fin p) ∙e eb e⁻¹) module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ fb : Finite B ⦄ (e : ∥ A ≃ B ∥) (f : A → B) where @@ -195,6 +198,7 @@ private variable instance Finite-Fin : ∀ {n} → Finite (Fin n) Finite-⊎ : ⦃ Finite A ⦄ → ⦃ Finite B ⦄ → Finite (A ⊎ B) + Finite-Maybe : ⦃ fa : Finite A ⦄ → Finite (Maybe A) Finite-Σ : {P : A → Type ℓ} → ⦃ Finite A ⦄ → ⦃ ∀ {x} → Finite (P x) ⦄ → Finite (Σ A P) @@ -221,6 +225,10 @@ Finite-⊎ {A = A} {B = B} = fin $ do beq ← enumeration {T = B} pure (⊎-ap aeq beq ∙e Finite-coproduct) +Finite-Maybe {A = A} = fin do + an ← enumeration {T = ⊤ ⊎ A} + pure (Maybe-is-sum ∙e an) + Finite-Π {A = A} {P = P} ⦃ afin ⦄ ⦃ pfin ⦄ = ∥-∥-out! do aeq ← afin .Finite.enumeration let @@ -249,10 +257,13 @@ Bool≃Fin2 = Iso→Equiv enum where enum : Iso Bool (Fin 2) enum .fst false = 0 enum .fst true = 1 - enum .snd .is-iso.inv fzero = false - enum .snd .is-iso.inv (fsuc fzero) = true - enum .snd .is-iso.rinv fzero = refl - enum .snd .is-iso.rinv (fsuc fzero) = refl + enum .snd .is-iso.inv i with fin-view i + enum .snd .is-iso.inv _ | zero = false + enum .snd .is-iso.inv _ | suc _ = true + enum .snd .is-iso.rinv i with fin-view i + enum .snd .is-iso.rinv _ | suc fzero = refl + enum .snd .is-iso.rinv _ | suc (fin (suc n) ⦃ forget p ⦄) = absurd (¬suc≤0 (≤-peel p)) + enum .snd .is-iso.rinv _ | zero = refl enum .snd .is-iso.linv true = refl enum .snd .is-iso.linv false = refl @@ -288,6 +299,6 @@ abstract instance diff --git a/src/Data/Fin/Product.lagda.md b/src/Data/Fin/Product.lagda.md index ee06b37e8..dc7bda5c1 100644 --- a/src/Data/Fin/Product.lagda.md +++ b/src/Data/Fin/Product.lagda.md @@ -47,8 +47,9 @@ these functions are isomorphisms in full generality. indexₚ : ∀ {n ℓ} {P : (i : Fin n) → Type (ℓ i)} → Πᶠ {ℓ = ℓ} P → ∀ i → P i indexₚ {n = zero} {P = P} prod () -indexₚ {n = suc n} {P = P} prod fzero = prod .fst -indexₚ {n = suc n} {P = P} prod (fsuc x) = indexₚ (prod .snd) x +indexₚ {n = suc n} {P = P} prod i with fin-view i +... | zero = prod .fst +... | suc x = indexₚ (prod .snd) x tabulateₚ : ∀ {n} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} @@ -107,8 +108,9 @@ simply compute away. updateₚ : ∀ {n} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} → Πᶠ P → ∀ i → P i → Πᶠ P -updateₚ xs fzero x = x , xs .snd -updateₚ xs (fsuc k) x = xs .fst , updateₚ (xs .snd) k x +updateₚ xs i x' with fin-view i | xs +... | zero | _ , xs = x' , xs +... | suc k | x , xs = x , updateₚ xs k x' mapₚ : ∀ {n} {ℓ ℓ' : Fin n → Level} @@ -127,14 +129,16 @@ indexₚ-mapₚ {Q : (i : Fin n) → Type (ℓ' i)} → ∀ (f : ∀ i → P i → Q i) (xs : Πᶠ P) i → indexₚ (mapₚ f xs) i ≡ f i (indexₚ xs i) -indexₚ-mapₚ {suc n} f xs fzero = refl -indexₚ-mapₚ {suc n} f xs (fsuc i) = indexₚ-mapₚ (λ i → f (fsuc i)) (xs .snd) i +indexₚ-mapₚ {suc n} f xs i with fin-view i +... | zero = refl +... | suc i = indexₚ-mapₚ (λ i → f (fsuc i)) (xs .snd) i indexₚ-tabulateₚ : ∀ {n} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} (f : ∀ i → P i) i → indexₚ (tabulateₚ f) i ≡ f i -indexₚ-tabulateₚ f fzero = refl -indexₚ-tabulateₚ f (fsuc i) = indexₚ-tabulateₚ (λ i → f (fsuc i)) i +indexₚ-tabulateₚ f i with fin-view i +... | zero = refl +... | suc i = indexₚ-tabulateₚ (λ i → f (fsuc i)) i ``` --> @@ -146,20 +150,22 @@ updatedₚ : ∀ {n} {ℓ : Fin (suc n) → Level} {P : (i : Fin (suc n)) → Type (ℓ i)} → (p : Πᶠ P) (i : Fin (suc n)) (x : P i) → (indexₚ {P = P} (updateₚ {P = P} p i x) i) ≡ x -updatedₚ {zero} p fzero x = refl -updatedₚ {suc n} p fzero x = refl -updatedₚ {suc n} p (fsuc i) x = updatedₚ (p .snd) i x +updatedₚ p i x with fin-view i +updatedₚ {zero} p _ x | zero = refl +updatedₚ {suc n} p _ x | zero = refl +updatedₚ {suc n} p _ x | suc i = updatedₚ (p .snd) i x updated-neₚ : ∀ {n} {ℓ : Fin (suc n) → Level} {P : (i : Fin (suc n)) → Type (ℓ i)} → (p : Πᶠ P) (i j : Fin (suc n)) (x : P i) → (i ≡ j → ⊥) → indexₚ {P = P} (updateₚ {P = P} p i x) j ≡ indexₚ {P = P} p j -updated-neₚ {zero} p fzero fzero x i≠j = absurd (i≠j refl) -updated-neₚ {suc n} p fzero fzero x i≠j = absurd (i≠j refl) -updated-neₚ {suc n} p fzero (fsuc j) x i≠j = refl -updated-neₚ {suc n} p (fsuc i) fzero x i≠j = refl -updated-neₚ {suc n} p (fsuc i) (fsuc j) x i≠j = updated-neₚ (p .snd) i j x λ p → i≠j (ap fsuc p) +updated-neₚ p i j x i≠j with fin-view i | fin-view j +updated-neₚ {zero} p _ _ x i≠j | zero | zero = absurd (i≠j refl) +updated-neₚ {suc n} p _ _ x i≠j | zero | zero = absurd (i≠j refl) +updated-neₚ {suc n} p _ _ x i≠j | zero | suc j = refl +updated-neₚ {suc n} p _ _ x i≠j | suc i | zero = refl +updated-neₚ {suc n} p _ _ x i≠j | suc i | suc j = updated-neₚ (p .snd) i j x λ p → i≠j (ap fsuc p) ``` # Finitary curried functions diff --git a/src/Data/Fin/Properties.lagda.md b/src/Data/Fin/Properties.lagda.md index fbdc8a807..f74ffaffd 100644 --- a/src/Data/Fin/Properties.lagda.md +++ b/src/Data/Fin/Properties.lagda.md @@ -2,9 +2,12 @@ ```agda open import 1Lab.Prelude +open import Data.Maybe.Properties +open import Data.Maybe.Base open import Data.Fin.Base open import Data.Nat.Base using (s≤s) open import Data.Dec +open import Data.Irr open import Data.Sum open import Meta.Invariant @@ -44,107 +47,78 @@ of a mess! ```agda skip-comm : ∀ {n} (i j : Fin (suc n)) → i ≤ j → ∀ x → skip (weaken i) (skip j x) ≡ skip (fsuc j) (skip i x) -skip-comm fzero j le x = refl -skip-comm (fsuc i) (fsuc j) le fzero = refl -skip-comm (fsuc i) (fsuc j) (Nat.s≤s le) (fsuc x) = ap fsuc (skip-comm i j le x) +skip-comm i j le x with fin-view i | fin-view j | le | fin-view x +... | zero | zero | _ | _ = refl +... | zero | suc _ | _ | _ = refl +... | suc i | suc j | le | zero = refl +... | suc i | suc j | s≤s le | (suc x) = ap fsuc (skip-comm i j le x) drop-comm : ∀ {n} (i j : Fin n) → i ≤ j → ∀ x → squish j (squish (weaken i) x) ≡ squish i (squish (fsuc j) x) -drop-comm fzero fzero le fzero = refl -drop-comm fzero fzero le (fsuc x) = refl -drop-comm fzero (fsuc j) le fzero = refl -drop-comm fzero (fsuc j) le (fsuc x) = refl -drop-comm (fsuc i) (fsuc j) le fzero = refl -drop-comm (fsuc i) (fsuc j) (Nat.s≤s le) (fsuc x) = ap fsuc (drop-comm i j le x) +drop-comm i j le x with fin-view i | fin-view j | le | fin-view x +... | zero | zero | le | zero = refl +... | zero | zero | le | suc x = refl +... | zero | suc j | le | zero = refl +... | zero | suc j | le | suc x = refl +... | suc i | suc j | le | zero = refl +... | suc i | suc j | s≤s le | suc x = ap fsuc (drop-comm i j le x) squish-skip-comm : ∀ {n} (i : Fin (suc n)) (j : Fin n) → i < fsuc j → ∀ x → squish (fsuc j) (skip (weaken i) x) ≡ skip i (squish j x) -squish-skip-comm fzero j (Nat.s≤s p) x = refl -squish-skip-comm (fsuc i) (fsuc j) (Nat.s≤s p) fzero = refl -squish-skip-comm (fsuc i) (fsuc j) (Nat.s≤s p) (fsuc x) = +squish-skip-comm i j le x with fin-view i | fin-view j | le | fin-view x +... | zero | zero | s≤s p | zero = refl +... | zero | zero | s≤s p | suc _ = refl +... | zero | suc _ | s≤s p | zero = refl +... | zero | suc _ | s≤s p | suc _ = refl +... | suc i | (suc j) | (Nat.s≤s p) | zero = refl +... | suc i | (suc j) | (Nat.s≤s p) | (suc x) = ap fsuc (squish-skip-comm i j p x) squish-skip : ∀ {n} (i j : Fin n) → i ≡ j → ∀ x → squish j (skip (weaken j) x) ≡ x -squish-skip fzero fzero p x = refl -squish-skip fzero (fsuc j) p x = absurd (fzero≠fsuc p) -squish-skip (fsuc i) fzero p x = refl -squish-skip (fsuc i) (fsuc j) p fzero = refl -squish-skip (fsuc i) (fsuc j) p (fsuc x) = ap fsuc (squish-skip i j (fsuc-inj p) x) +squish-skip i j p x with fin-view i | fin-view j | fin-view x +... | zero | zero | x = refl +... | zero | (suc j) | x = absurd (fzero≠fsuc p) +... | (suc i) | zero | x = refl +... | (suc i) | (suc j) | zero = refl +... | (suc i) | (suc j) | (suc x) = + ap fsuc (squish-skip i j (fsuc-inj p) x) squish-skip-fsuc : ∀ {n} (i : Fin (suc n)) (j : Fin n) → i ≡ fsuc j → ∀ x → squish j (skip i x) ≡ x -squish-skip-fsuc fzero fzero p x = refl -squish-skip-fsuc fzero (fsuc j) p x = absurd (fzero≠fsuc p) -squish-skip-fsuc (fsuc i) fzero p fzero = refl -squish-skip-fsuc (fsuc fzero) fzero p (fsuc x) = refl -squish-skip-fsuc (fsuc (fsuc i)) fzero p (fsuc x) = - absurd (fzero≠fsuc (fsuc-inj (sym p))) -squish-skip-fsuc (fsuc i) (fsuc j) p fzero = refl -squish-skip-fsuc (fsuc i) (fsuc j) p (fsuc x) = - ap fsuc (squish-skip-fsuc i j (fsuc-inj p) x) +squish-skip-fsuc i j p x with fin-view i | fin-view j | fin-view x +... | zero | zero | x = refl +... | zero | suc j | x = absurd (fzero≠fsuc p) +... | suc i | suc j | zero = refl +... | suc i | suc j | suc x = ap fsuc (squish-skip-fsuc i j (fsuc-inj p) x) +... | suc i | zero | x with fin-view i | x +... | zero | zero = refl +... | zero | suc x = refl +... | suc i | zero = refl +... | suc i | suc x = absurd (Nat.zero≠suc λ i → Nat.pred (p (~ i) .lower)) + +Fin-suc : ∀ {n} → Fin (suc n) ≃ Maybe (Fin n) +Fin-suc = Iso→Equiv (to , iso from ir il) where + to : ∀ {n} → Fin (suc n) → Maybe (Fin n) + to i with fin-view i + ... | suc i = just i + ... | zero = nothing + + from : ∀ {n} → Maybe (Fin n) → Fin (suc n) + from (just x) = fsuc x + from nothing = fzero + + ir : is-right-inverse from to + ir nothing = refl + ir (just x) = refl + + il : is-left-inverse from to + il i with fin-view i + ... | suc i = refl + ... | zero = refl Fin-peel : ∀ {l k} → Fin (suc l) ≃ Fin (suc k) → Fin l ≃ Fin k -Fin-peel {l} {k} sl≃sk = (Iso→Equiv (l→k , (iso k→l b→a→b a→b→a))) where - sk≃sl : Fin (suc k) ≃ Fin (suc l) - sk≃sl = sl≃sk e⁻¹ - module sl≃sk = Equiv sl≃sk - module sk≃sl = Equiv sk≃sl - - l→k : Fin l → Fin k - l→k x with inspect (sl≃sk.to (fsuc x)) - ... | fsuc y , _ = y - ... | fzero , p with inspect (sl≃sk.to fzero) - ... | fsuc y , _ = y - ... | fzero , q = absurd (fzero≠fsuc (sl≃sk.injective₂ q p)) - - k→l : Fin k → Fin l - k→l x with inspect (sk≃sl.to (fsuc x)) - ... | fsuc x , _ = x - ... | fzero , p with inspect (sk≃sl.to fzero) - ... | fsuc y , _ = y - ... | fzero , q = absurd (fzero≠fsuc (sk≃sl.injective₂ q p)) - - absurd-path : ∀ {ℓ} {A : Type ℓ} {y : A} .{x : ⊥} → absurd x ≡ y - absurd-path {x = ()} - - a→b→a : ∀ a → k→l (l→k a) ≡ a - a→b→a a with inspect (sl≃sk.to (fsuc a)) - a→b→a a | fsuc x , p' with inspect (sk≃sl.to (fsuc x)) - a→b→a a | fsuc x , p' | fsuc y , q' = fsuc-inj ( - sym q' ∙ ap (sk≃sl.to) (sym p') ∙ sl≃sk.η _) - a→b→a a | fsuc x , p' | fzero , q' = absurd contra where - r = sl≃sk.injective₂ p' (sl≃sk.ε (fsuc x)) - contra = fzero≠fsuc (sym (r ∙ q')) - a→b→a a | fzero , p' with inspect (sl≃sk.to fzero) - a→b→a a | fzero , p' | fsuc x , q' with inspect (sk≃sl.to (fsuc x)) - a→b→a a | fzero , p' | fsuc x , q' | fsuc y , r' = absurd do - fzero≠fsuc (sym (sym r' ∙ ap sk≃sl.to (sym q') ∙ sl≃sk.η fzero)) - a→b→a a | fzero , p' | fsuc x , q' | fzero , r' with inspect (sk≃sl.to fzero) - a→b→a a | fzero , p' | fsuc x , q' | fzero , r' | fsuc z , s = fsuc-inj $ - sym s ∙ ap sk≃sl.to (sym p') ∙ sl≃sk.η (fsuc a) - a→b→a a | fzero , p' | fsuc x , q' | fzero , r' | fzero , s = absurd-path - a→b→a a | fzero , p' | fzero , q' = absurd (fzero≠fsuc $ - sl≃sk.injective₂ q' p') - - b→a→b : ∀ b → l→k (k→l b) ≡ b - b→a→b b with inspect (sk≃sl.to (fsuc b)) - b→a→b b | fsuc x , p' with inspect (sl≃sk.to (fsuc x)) - b→a→b b | fsuc x , p' | fsuc y , q' = fsuc-inj $ - sym q' ∙ ap (sl≃sk.to) (sym p') ∙ sk≃sl.η _ - b→a→b b | fsuc x , p' | fzero , q' = absurd contra where - r = sk≃sl.injective₂ p' (sk≃sl.ε (fsuc x)) - contra = fzero≠fsuc (sym (r ∙ q')) - b→a→b b | fzero , p' with inspect (sk≃sl.to fzero) - b→a→b b | fzero , p' | fsuc x , q' with inspect (sl≃sk.to (fsuc x)) - b→a→b b | fzero , p' | fsuc x , q' | fsuc y , r' = absurd (fzero≠fsuc $ - sym (sym r' ∙ ap (sl≃sk.to) (sym q') ∙ sk≃sl.η _)) - b→a→b b | fzero , p' | fsuc x , q' | fzero , r' with inspect (sl≃sk.to fzero) - b→a→b a | fzero , p' | fsuc x , q' | fzero , r' | fsuc z , s = fsuc-inj $ - sym s ∙ ap (sl≃sk.to) (sym p') ∙ sk≃sl.η (fsuc a) - b→a→b a | fzero , p' | fsuc x , q' | fzero , r' | fzero , s = absurd-path - b→a→b b | fzero , p' | fzero , q' = absurd (fzero≠fsuc $ - sk≃sl.injective₂ q' p') +Fin-peel {l} {k} sl≃sk = Maybe-injective (Equiv.inverse Fin-suc ∙e sl≃sk ∙e Fin-suc) Fin-injective : ∀ {l k} → Fin l ≃ Fin k → l ≡ k Fin-injective {zero} {zero} l≃k = refl @@ -154,62 +128,53 @@ Fin-injective {suc l} {zero} l≃k with l≃k .fst fzero ... | () Fin-injective {suc l} {suc k} sl≃sk = ap suc $ Fin-injective (Fin-peel sl≃sk) -to-from-ℕ< : ∀ {n} (x : ℕ< n) → to-ℕ< {n = n} (from-ℕ< x) ≡ x -to-from-ℕ< {n = suc n} x = Σ-prop-path! (to-from-ℕ {n = suc n} x) where - to-from-ℕ : ∀ {n} x → to-nat {n = n} (from-ℕ< x) ≡ x .fst - to-from-ℕ {n = suc n} (zero , p) = refl - to-from-ℕ {n = suc n} (suc x , Nat.s≤s p) = ap suc (to-from-ℕ {n = n} (x , p)) - -from-to-ℕ< : ∀ {n} (x : Fin n) → from-ℕ< (to-ℕ< x) ≡ x -from-to-ℕ< fzero = refl -from-to-ℕ< (fsuc x) = ap fsuc (from-to-ℕ< x) - -Fin≃ℕ< : ∀ {n} → Fin n ≃ ℕ< n -Fin≃ℕ< {n} = to-ℕ< , is-iso→is-equiv (iso from-ℕ< (to-from-ℕ< {n}) from-to-ℕ<) - avoid-injective : ∀ {n} (i : Fin (suc n)) {j k : Fin (suc n)} {i≠j : i ≠ j} {i≠k : i ≠ k} → avoid i j i≠j ≡ avoid i k i≠k → j ≡ k -avoid-injective fzero {fzero} {k} {i≠j} p = absurd (i≠j refl) -avoid-injective fzero {fsuc j} {fzero} {i≠k = i≠k} p = absurd (i≠k refl) -avoid-injective {suc n} fzero {fsuc j} {fsuc k} p = ap fsuc p -avoid-injective {suc n} (fsuc i) {fzero} {fzero} p = refl -avoid-injective {suc n} (fsuc i) {fzero} {fsuc k} p = absurd (fzero≠fsuc p) -avoid-injective {suc n} (fsuc i) {fsuc j} {fzero} p = absurd (fzero≠fsuc (sym p)) -avoid-injective {suc n} (fsuc i) {fsuc j} {fsuc k} p = - ap fsuc (avoid-injective {n} i {j} {k} (fsuc-inj p)) +avoid-injective i {j} {k} {i≠j} {i≠k} p with fin-view i | fin-view j | fin-view k +... | zero | zero | _ = absurd (i≠j refl) +... | zero | suc j | zero = absurd (i≠k refl) +... | zero | suc j | suc k = ap fsuc p +... | suc i | zero | zero = refl +avoid-injective {suc n} _ p | suc i | zero | suc k = absurd (fzero≠fsuc p) +avoid-injective {suc n} _ p | suc i | suc j | zero = absurd (fsuc≠fzero p) +avoid-injective {suc n} _ p | suc i | suc j | suc k = ap fsuc (avoid-injective {n} i {j} {k} (fsuc-inj p)) skip-injective : ∀ {n} (i : Fin (suc n)) (j k : Fin n) → skip i j ≡ skip i k → j ≡ k -skip-injective fzero j k p = fsuc-inj p -skip-injective (fsuc i) fzero fzero p = refl -skip-injective (fsuc i) fzero (fsuc k) p = absurd (fzero≠fsuc p) -skip-injective (fsuc i) (fsuc j) fzero p = absurd (fzero≠fsuc (sym p)) -skip-injective (fsuc i) (fsuc j) (fsuc k) p = ap fsuc (skip-injective i j k (fsuc-inj p)) +skip-injective i j k p with fin-view i | fin-view j | fin-view k +... | zero | j | k = fsuc-inj p +... | suc i | zero | zero = refl +... | suc i | zero | suc k = absurd (fzero≠fsuc p) +... | suc i | suc j | zero = absurd (fsuc≠fzero p) +... | suc i | suc j | suc k = ap fsuc (skip-injective i j k (fsuc-inj p)) skip-skips : ∀ {n} (i : Fin (suc n)) (j : Fin n) → skip i j ≠ i -skip-skips fzero j p = fzero≠fsuc (sym p) -skip-skips (fsuc i) fzero p = fzero≠fsuc p -skip-skips (fsuc i) (fsuc j) p = skip-skips i j (fsuc-inj p) +skip-skips i j p with fin-view i | fin-view j +... | zero | j = fsuc≠fzero p +... | suc i | zero = fzero≠fsuc p +... | suc i | suc j = skip-skips i j (fsuc-inj p) avoid-skip : ∀ {n} (i : Fin (suc n)) (j : Fin n) {neq : i ≠ skip i j} → avoid i (skip i j) neq ≡ j -avoid-skip fzero fzero = refl -avoid-skip fzero (fsuc j) = refl -avoid-skip (fsuc i) fzero = refl -avoid-skip (fsuc i) (fsuc j) = ap fsuc (avoid-skip i j) +avoid-skip i j with fin-view i | fin-view j +... | zero | zero = refl +... | zero | suc j = refl +... | suc i | zero = refl +... | suc i | suc j = ap fsuc (avoid-skip i j) skip-avoid : ∀ {n} (i : Fin (suc n)) (j : Fin (suc n)) {i≠j : i ≠ j} → skip i (avoid i j i≠j) ≡ j -skip-avoid fzero fzero {i≠j} = absurd (i≠j refl) -skip-avoid {suc n} fzero (fsuc j) = refl -skip-avoid {suc n} (fsuc i) fzero = refl -skip-avoid {suc n} (fsuc i) (fsuc j) = ap fsuc (skip-avoid i j) +skip-avoid i j {i≠j} with fin-view i | fin-view j +... | zero | zero = absurd (i≠j refl) +skip-avoid {suc n} _ _ | zero | suc j = refl +skip-avoid {suc n} _ _ | suc i | zero = refl +skip-avoid {suc n} _ _ | suc i | suc j = ap fsuc (skip-avoid i j) ``` ## Iterated products and sums {defines="iterated-products"} @@ -228,24 +193,30 @@ Fin-suc-Π = Iso→Equiv λ where .snd .is-iso.rinv x → refl - .snd .is-iso.linv k i fzero → k fzero - .snd .is-iso.linv k i (fsuc n) → k (fsuc n) + .snd .is-iso.linv k i fzero → k (fin zero ⦃ forget auto ⦄) + .snd .is-iso.linv k i (fin (suc n) ⦃ b ⦄) → k (fin (suc n) ⦃ b ⦄) Fin-suc-Σ : ∀ {ℓ} {n} {A : Fin (suc n) → Type ℓ} → Σ (Fin (suc n)) A ≃ (A fzero ⊎ Σ (Fin n) (A ∘ fsuc)) -Fin-suc-Σ = Iso→Equiv λ where - .fst (fzero , a) → inl a - .fst (fsuc x , a) → inr (x , a) - - .snd .is-iso.inv (inl a) → fzero , a - .snd .is-iso.inv (inr (x , a)) → fsuc x , a - - .snd .is-iso.rinv (inl _) → refl - .snd .is-iso.rinv (inr _) → refl - - .snd .is-iso.linv (fzero , a) → refl - .snd .is-iso.linv (fsuc x , a) → refl +Fin-suc-Σ {A = A} = Iso→Equiv (to , iso from ir il) where + to : ∫ₚ A → A fzero ⊎ ∫ₚ (A ∘ fsuc) + to (i , a) with fin-view i + ... | zero = inl a + ... | suc x = inr (x , a) + + from : A fzero ⊎ ∫ₚ (A ∘ fsuc) → ∫ₚ A + from (inl x) = fzero , x + from (inr (x , a)) = fsuc x , a + + ir : is-right-inverse from to + ir (inl x) = refl + ir (inr x) = refl + + il : is-left-inverse from to + il (i , a) with fin-view i + ... | zero = refl + ... | suc _ = refl ``` ## Finite choice {defines="finite-choice"} @@ -374,17 +345,20 @@ Fin-injection→equiv Fin-injection→equiv {zero} f inj .is-eqv () Fin-injection→equiv {suc n} f inj .is-eqv i with f 0 ≡? i ... | yes p = contr (0 , p) λ (j , p') → Σ-prop-path! (inj (p ∙ sym p')) -... | no ¬p = contr - (fsuc (rec .centre .fst) , avoid-injective (f 0) (rec .centre .snd)) - λ where - (fzero , p) → absurd (¬p p) - (fsuc j , p) → Σ-prop-path! (ap (fsuc ∘ fst) +... | no ¬p = contr fib cen where + rec = Fin-injection→equiv {n} + (λ x → avoid (f 0) (f (fsuc x)) (Nat.zero≠suc ∘ ap lower ∘ inj)) + (λ p → fsuc-inj (inj (avoid-injective (f 0) p))) + .is-eqv (avoid (f 0) i ¬p) + + fib : fibre f i + fib = fsuc (rec .centre .fst) , avoid-injective (f 0) (rec .centre .snd) + + cen : ∀ x → fib ≡ x + cen (i , p) with fin-view i + ... | zero = absurd (¬p p) + ... | suc j = Σ-prop-path! (ap (fsuc ∘ fst) (rec .paths (j , ap₂ (avoid (f 0)) p prop!))) - where - rec = Fin-injection→equiv {n} - (λ x → avoid (f 0) (f (fsuc x)) (fzero≠fsuc ∘ inj)) - (λ p → fsuc-inj (inj (avoid-injective (f 0) p))) - .is-eqv (avoid (f 0) i ¬p) ``` Since [[every surjection between finite sets splits|finite choice]], any @@ -412,10 +386,11 @@ avoid-insert → (j : Fin (suc n)) → (i≠j : i ≠ j) → (ρ [ i ≔ a ]) j ≡ ρ (avoid i j i≠j) -avoid-insert {n = n} ρ fzero a fzero i≠j = absurd (i≠j refl) -avoid-insert {n = suc n} ρ fzero a (fsuc j) i≠j = refl -avoid-insert {n = suc n} ρ (fsuc i) a fzero i≠j = refl -avoid-insert {n = suc n} ρ (fsuc i) a (fsuc j) i≠j = +avoid-insert ρ i a j i≠j with fin-view i | fin-view j +... | zero | zero = absurd (i≠j refl) +... | zero | suc j = refl +avoid-insert {suc n} ρ _ a _ _ | suc i | zero = refl +avoid-insert {suc n} ρ _ a _ i≠j | suc i | suc j = avoid-insert (ρ ∘ fsuc) i a j (i≠j ∘ ap fsuc) insert-lookup @@ -423,17 +398,19 @@ insert-lookup → (ρ : Fin n → A) → (i : Fin (suc n)) (a : A) → (ρ [ i ≔ a ]) i ≡ a -insert-lookup {n = n} ρ fzero a = refl -insert-lookup {n = suc n} ρ (fsuc i) a = insert-lookup (ρ ∘ fsuc) i a +insert-lookup {n = n} ρ i a with fin-view i +... | zero = refl +insert-lookup {n = suc n} ρ _ a | suc i = insert-lookup (ρ ∘ fsuc) i a delete-insert : ∀ {n} {ℓ} {A : Type ℓ} → (ρ : Fin n → A) → (i : Fin (suc n)) (a : A) → ∀ j → delete (ρ [ i ≔ a ]) i j ≡ ρ j -delete-insert ρ fzero a j = refl -delete-insert ρ (fsuc i) a fzero = refl -delete-insert ρ (fsuc i) a (fsuc j) = delete-insert (ρ ∘ fsuc) i a j +delete-insert ρ i a j with fin-view i | fin-view j +... | zero | j = refl +... | suc i | zero = refl +... | suc i | (suc j) = delete-insert (ρ ∘ fsuc) i a j insert-delete : ∀ {n} {ℓ} {A : Type ℓ} @@ -441,8 +418,18 @@ insert-delete → (i : Fin (suc n)) (a : A) → ρ i ≡ a → ∀ j → ((delete ρ i) [ i ≔ a ]) j ≡ ρ j -insert-delete {n = n} ρ fzero a p fzero = sym p -insert-delete {n = n} ρ fzero a p (fsuc j) = refl -insert-delete {n = suc n} ρ (fsuc i) a p fzero = refl -insert-delete {n = suc n} ρ (fsuc i) a p (fsuc j) = insert-delete (ρ ∘ fsuc) i a p j +insert-delete ρ i a p j with fin-view i | fin-view j +... | zero | zero = sym p +... | zero | suc j = refl +insert-delete {suc n} ρ _ a p _ | suc i | zero = refl +insert-delete {suc n} ρ _ a p _ | suc i | suc j = insert-delete (ρ ∘ fsuc) i a p j + +ℕ< : Nat → Type +ℕ< n = Σ[ k ∈ Nat ] k Nat.< n + +from-ℕ< : ∀ {n} → ℕ< n → Fin n +from-ℕ< (i , p) = fin i ⦃ forget p ⦄ + +to-ℕ< : ∀ {n} → Fin n → ℕ< n +to-ℕ< (fin i ⦃ forget p ⦄) = i , recover p ``` diff --git a/src/Data/Int/DivMod.lagda.md b/src/Data/Int/DivMod.lagda.md index 06c81abcf..2e83e99bc 100644 --- a/src/Data/Int/DivMod.lagda.md +++ b/src/Data/Int/DivMod.lagda.md @@ -11,6 +11,7 @@ open import Data.Nat.DivMod open import Data.Dec.Base open import Data.Fin hiding (_<_) open import Data.Int hiding (Positive ; _<_ ; <-weaken) +open import Data.Irr open import Data.Nat as Nat ``` --> @@ -210,8 +211,8 @@ same-rem→divides-diff n x y p = dividesℤ (x /ℤ n -ℤ y /ℤ n) $ ...and that natural numbers below $n$ are their own remainder modulo $n$. ```agda -ℕ<-%ℤ : ∀ {n} (i : ℕ< n) → .⦃ _ : Positive n ⦄ → pos (i .fst) %ℤ n ≡ i .fst -ℕ<-%ℤ {n} (i , p) = ap remℤ (DivModℤ-unique (pos i) n +Fin-%ℤ : ∀ {n} (i : Fin n) → .⦃ _ : Positive n ⦄ → pos (i .lower) %ℤ n ≡ i .lower +Fin-%ℤ {n} (fin i ⦃ forget p ⦄) = ap remℤ (DivModℤ-unique (pos i) n (divide-posℤ (pos i) n) (divmodℤ 0 i refl p)) ``` diff --git a/src/Data/Irr.lagda.md b/src/Data/Irr.lagda.md new file mode 100644 index 000000000..f4eca552d --- /dev/null +++ b/src/Data/Irr.lagda.md @@ -0,0 +1,56 @@ + + +```agda +module Data.Irr where +``` + +# Strict propositional truncations + + + +In Agda, it's possible to turn any type into one that *definitionally* +has at most one inhabitant. We do this using a record containing an +irrelevant field. + +```agda +record Irr {ℓ} (A : Type ℓ) : Type ℓ where + constructor forget + field + .lower : A +``` + +The most important property of this type is that, given any $x, y$ in +$\operatorname{Irr}(A)$, the constant path `refl`{.Agda} checks at type +$x \is y$. + +```agda +instance + H-Level-Irr : ∀ {n} → H-Level (Irr A) (suc n) + H-Level-Irr {n} = prop-instance λ _ _ → refl +``` + + diff --git a/src/Data/List/Base.lagda.md b/src/Data/List/Base.lagda.md index 4dfbaedee..7a219e5a1 100644 --- a/src/Data/List/Base.lagda.md +++ b/src/Data/List/Base.lagda.md @@ -304,8 +304,9 @@ lookup x ((k , v) ∷ xs) with x ≡? k ... | no _ = lookup x xs _!_ : (l : List A) → Fin (length l) → A -(x ∷ xs) ! fzero = x -(x ∷ xs) ! fsuc n = xs ! n +(x ∷ xs) ! n with fin-view n +... | zero = x +... | suc i = xs ! i tabulate : ∀ {n} (f : Fin n → A) → List A tabulate {n = zero} f = [] diff --git a/src/Data/List/Membership.lagda.md b/src/Data/List/Membership.lagda.md index a395e7914..ab910e5e8 100644 --- a/src/Data/List/Membership.lagda.md +++ b/src/Data/List/Membership.lagda.md @@ -72,8 +72,9 @@ element→!-fibre (there prf) with element→!-fibre prf !-fibre→element : ∀ {x : A} {xs} → fibre (xs !_) x → x ∈ xs !-fibre→element {A = A} {x = x} = λ (ix , p) → go ix p module !-fibre→element where go : ∀ {xs} (ix : Fin (length xs)) → xs ! ix ≡ x → x ∈ xs - go {xs = x ∷ xs} fzero p = here (sym p) - go {xs = x ∷ xs} (fsuc ix) p = there (go ix p) + go ix _ with fin-view ix + go {xs = x ∷ xs} _ p | zero = here (sym p) + go {xs = x ∷ xs} _ p | (suc ix) = there (go ix p) ``` The equivalence between these definitions explains why $a \in_l as$ can @@ -86,8 +87,9 @@ depending on the type $A$. !-fibre→element→fibre : ∀ {x : A} {xs} (f : fibre (xs !_) x) → element→!-fibre (!-fibre→element f) ≡ f !-fibre→element→fibre {A = A} {x = x} (ix , p) = go ix p where go : ∀ {xs} (ix : Fin (length xs)) (p : xs ! ix ≡ x) → element→!-fibre (!-fibre→element.go {xs = xs} ix p) ≡ (ix , p) - go {xs = x ∷ xs} fzero p = refl - go {xs = x ∷ xs} (fsuc ix) p = Σ-pathp (ap fsuc (ap fst p')) (ap snd p') + go ix p with fin-view ix + go {xs = x ∷ xs} _ p | zero = refl + go {xs = x ∷ xs} _ p | suc ix = Σ-pathp (ap fsuc (ap fst p')) (ap snd p') where p' = go {xs = xs} ix p element→!-fibre→element @@ -182,12 +184,13 @@ member→member-nub {xs = x ∷ xs} (there α) with elem? x (nub xs) @@ -150,28 +149,6 @@ Maybe-reflect-discrete Maybe-reflect-discrete eq? = Discrete-inj just just-inj eq? ``` -## Finiteness - -If `A` is finite, then `Maybe A` is also finite. - -```agda -Finite-Maybe - : ⦃ fa : Finite A ⦄ - → Finite (Maybe A) -Finite-Maybe ⦃ fa ⦄ .cardinality = suc (fa .cardinality) -Finite-Maybe {A = A} ⦃ fa ⦄ .enumeration = - ∥-∥-map (Iso→Equiv ∘ maybe-iso) (fa .enumeration) where - maybe-iso : A ≃ Fin (fa .cardinality) → Iso (Maybe A) (Fin (suc (fa .cardinality))) - maybe-iso f .fst (just x) = fsuc (Equiv.to f x) - maybe-iso f .fst nothing = fzero - maybe-iso f .snd .is-iso.inv fzero = nothing - maybe-iso f .snd .is-iso.inv (fsuc i) = just (Equiv.from f i) - maybe-iso f .snd .is-iso.rinv fzero = refl - maybe-iso f .snd .is-iso.rinv (fsuc i) = ap fsuc (Equiv.ε f i) - maybe-iso f .snd .is-iso.linv (just x) = ap just (Equiv.η f x) - maybe-iso f .snd .is-iso.linv nothing = refl -``` - # Misc. properties If `A` is empty, then a `Maybe A` must be `nothing`{.Agda}. @@ -230,3 +207,69 @@ map-<|> map-<|> (just x) y = refl map-<|> nothing y = refl ``` + +## Injectivity + +We can prove that the `Maybe`{.Agda} type constructor, considered as a +function from a universe to itself, is injective. + +```agda +Maybe-injective : Maybe A ≃ Maybe B → A ≃ B +Maybe-injective e = Iso→Equiv (a→b , iso b→a (lemma e) il) where + a→b = maybe-injective e + b→a = maybe-injective (Equiv.inverse e) + + module _ (e : Maybe A ≃ Maybe B) where abstract + private + module e = Equiv e + module e⁻¹ = Equiv e.inverse + + lemma : is-right-inverse (maybe-injective (Equiv.inverse e)) (maybe-injective e) + lemma x with inspect (e.from (just x)) + lemma x | just y , p with inspect (e.to (just y)) + lemma x | just y , p | just z , q = just-inj (sym q ∙ ap e.to (sym p) ∙ e.ε _) + lemma x | just y , p | nothing , q with inspect (e.to nothing) + lemma x | just y , p | nothing , q | nothing , r = absurd (just≠nothing (e.injective₂ q r)) + lemma x | just y , p | nothing , q | just z , r = absurd (nothing≠just (sym q ∙ ap e.to (sym p) ∙ e.ε _)) + lemma x | nothing , p with inspect (e.from nothing) + lemma x | nothing , p | nothing , q = absurd (just≠nothing (e⁻¹.injective₂ p q)) + lemma x | nothing , p | just y , q with inspect (e.to (just y)) + lemma x | nothing , p | just y , q | just z , r = absurd (just≠nothing (sym r ∙ ap e.to (sym q) ∙ e.ε _)) + lemma x | nothing , p | just y , q | nothing , r with inspect (e.to nothing) + lemma x | nothing , p | just y , q | nothing , r | nothing , s = absurd (just≠nothing (e.injective₂ r s)) + lemma x | nothing , p | just y , q | nothing , r | just z , s = just-inj (sym s ∙ ap e.to (sym p) ∙ e.ε _) + + abstract + il : is-left-inverse b→a a→b + il = p' where + p : is-right-inverse (maybe-injective (Equiv.inverse (Equiv.inverse e))) (maybe-injective (Equiv.inverse e)) + p = lemma (Equiv.inverse e) + + p' : is-right-inverse (maybe-injective e) (maybe-injective (Equiv.inverse e)) + p' = subst + (λ e' → is-right-inverse (maybe-injective e') (maybe-injective (Equiv.inverse e))) + {Equiv.inverse (Equiv.inverse e)} {e} + trivial! p +``` + + diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md index 7c6c26de4..750fe3ba0 100644 --- a/src/Data/Nat/Base.lagda.md +++ b/src/Data/Nat/Base.lagda.md @@ -219,6 +219,17 @@ instance {-# INCOHERENT x≤x x≤sucy #-} +≤-peel : ∀ {x y : Nat} → suc x ≤ suc y → x ≤ y +≤-peel (s≤s p) = p + +¬suc≤0 : ∀ {x} → suc x ≤ 0 → ⊥ +¬suc≤0 () + +≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z +≤-trans 0≤x 0≤x = 0≤x +≤-trans 0≤x (s≤s q) = 0≤x +≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q) + factorial : Nat → Nat factorial zero = 1 factorial (suc n) = suc n * factorial n @@ -237,6 +248,17 @@ m < n = suc m ≤ n infix 7 _<_ _≤_ ``` + + As an "ordering combinator", we can define the _maximum_ of two natural numbers by recursion: The maximum of zero and a successor (on either side) is the successor, and the maximum of successors is the successor of diff --git a/src/Data/Nat/Order.lagda.md b/src/Data/Nat/Order.lagda.md index 72d0a3e5e..1c5b26477 100644 --- a/src/Data/Nat/Order.lagda.md +++ b/src/Data/Nat/Order.lagda.md @@ -44,11 +44,6 @@ naturals automatically. --> ```agda -≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z -≤-trans 0≤x 0≤x = 0≤x -≤-trans 0≤x (s≤s q) = 0≤x -≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q) - ≤-antisym : ∀ {x y : Nat} → x ≤ y → y ≤ x → x ≡ y ≤-antisym 0≤x 0≤x = refl ≤-antisym (s≤s p) (s≤s q) = ap suc (≤-antisym p q) @@ -62,13 +57,6 @@ As a minor convenience, we prove that the constructor `s≤s`{.Agda} is an equivalence between $x \le y$ and $(1 + x) \le (1 + y)$. ```agda -≤-peel : ∀ {x y : Nat} → suc x ≤ suc y → x ≤ y -≤-peel (s≤s p) = p - -≤-sucr : ∀ {x y : Nat} → x ≤ y → x ≤ suc y -≤-sucr 0≤x = 0≤x -≤-sucr (s≤s p) = s≤s (≤-sucr p) - ≤-ascend : ∀ {x} → x ≤ suc x ≤-ascend = ≤-sucr ≤-refl ``` @@ -108,9 +96,6 @@ instance <-irrefl {zero} {suc y} p _ = absurd (zero≠suc p) <-irrefl {suc x} {suc y} p (s≤s q) = <-irrefl (suc-inj p) q -<-weaken : ∀ {x y} → x < y → x ≤ y -<-weaken {x} {suc y} p = ≤-sucr (≤-peel p) - ≤-strengthen : ∀ {x y} → x ≤ y → (x ≡ y) ⊎ (x < y) ≤-strengthen {zero} {zero} 0≤x = inl refl ≤-strengthen {zero} {suc y} 0≤x = inr (s≤s 0≤x) diff --git a/src/Data/Nat/Prime.lagda.md b/src/Data/Nat/Prime.lagda.md index 4c6ff0f25..da27bdf9b 100644 --- a/src/Data/Nat/Prime.lagda.md +++ b/src/Data/Nat/Prime.lagda.md @@ -16,6 +16,7 @@ open import Data.Nat.Order open import Data.Fin.Base renaming (_≤_ to _≤ᶠ_) hiding (_<_) open import Data.Nat.Base open import Data.Dec +open import Data.Irr open import Data.Sum ``` --> @@ -149,7 +150,7 @@ distinct-primes→coprime {a@(suc a')} {b@(suc b')} apr bpr a≠b = record ```agda is-prime-or-composite : ∀ n → 1 < n → is-prime n ⊎ is-composite n is-prime-or-composite n@(suc (suc m)) (s≤s p) - with Fin-omniscience {n = n} (λ k → 1 < to-nat k × to-nat k ∣ n) + with Fin-omniscience {n = n} (λ k → 1 < k .lower × k .lower ∣ n) ... | inr prime = inl record { prime≠1 = suc≠zero ∘ suc-inj ; primality = no-divisors→prime } where no-divisors→prime : ∀ d → d ∣ n → d ≡ 1 ⊎ d ≡ n no-divisors→prime d div with d ≡? 1 @@ -161,40 +162,28 @@ is-prime-or-composite n@(suc (suc m)) (s≤s p) ord : d < n ord = proper-divisor-< ¬d=n div - coh : d ≡ to-nat (from-ℕ< (d , ord)) - coh = sym (ap fst (to-from-ℕ< (d , ord))) - no = case d return (λ x → ¬ x ≡ 1 → x ∣ n → 1 < x) of λ where 0 p1 div → absurd (<-irrefl (sym div) (s≤s 0≤x)) 1 p1 div → absurd (p1 refl) (suc (suc n)) p1 div → s≤s (s≤s 0≤x) - in absurd (prime (from-ℕ< (d , ord)) ((subst (1 <_) coh (no ¬d=1 div)) , subst (_∣ n) coh div)) + in absurd (prime (from-ℕ< (d , ord)) (no ¬d=1 div , div)) ... | inl (ix , (proper , div) , least) = inr record { p-prime = prime ; q-proper = proper' ; factors = path ; least = least' } where open Σ (∣→fibre div) renaming (fst to quot ; snd to path) abstract - least' : (p' : Nat) → 1 < p' → p' ∣ n → to-nat ix ≤ p' + least' : (p' : Nat) → 1 < p' → p' ∣ n → ix .lower ≤ p' least' p' x div with ≤-strengthen (m∣n→m≤n div) - ... | inl same = ≤-trans ≤-ascend (subst (to-nat ix <_) (sym same) (to-ℕ< ix .snd)) - ... | inr less = - let - it : ℕ< n - it = p' , less - - coh : p' ≡ to-nat (from-ℕ< it) - coh = sym (ap fst (to-from-ℕ< it)) - - orig = least (from-ℕ< it) (subst (1 <_) coh x , subst (_∣ n) coh div) - in ≤-trans orig (subst (to-nat (from-ℕ< it) ≤_) (sym coh) ≤-refl) + ... | inl same = ≤-trans ≤-ascend (subst (ix .lower <_) (sym same) (to-ℕ< ix .snd)) + ... | inr less = least (from-ℕ< (p' , less)) (x , div) - prime : is-prime (to-nat ix) - prime = least-divisor→is-prime (to-nat ix) n proper div least' + prime : is-prime (ix .lower) + prime = least-divisor→is-prime (ix .lower) n proper div least' proper' : 1 < quot proper' with quot | path ... | 0 | q = absurd (<-irrefl q (s≤s 0≤x)) - ... | 1 | q = absurd (<-irrefl (sym (+-zeror (to-nat ix)) ∙ q) (to-ℕ< ix .snd)) + ... | 1 | q = absurd (<-irrefl (sym (+-zeror (ix .lower)) ∙ q) (to-ℕ< ix .snd)) ... | suc (suc n) | p = s≤s (s≤s 0≤x) record Factorisation (n : Nat) : Type where diff --git a/src/Data/Nat/Solver.lagda.md b/src/Data/Nat/Solver.lagda.md index 83eaa06e8..db9387758 100644 --- a/src/Data/Nat/Solver.lagda.md +++ b/src/Data/Nat/Solver.lagda.md @@ -169,8 +169,9 @@ We also define the identity monomials $X_i \in A[X_0]\cdots[X_n]$. ```agda X[_] : Fin n → Poly Nat n -X[_] fzero = 1ₚ *X+ 0ₚ -X[_] (fsuc i) = 0ₚ *X+ X[ i ] +X[ i ] with fin-view i +... | zero = 1ₚ *X+ 0ₚ +... | suc i = 0ₚ *X+ X[ i ] ``` Now, onto addition of polynomials. This is more or less what one would @@ -269,12 +270,13 @@ monomial $X_i$. ```agda sound-X[_] : ∀ i → (env : Vec Nat n) → ⟦ X[ i ] ⟧ₚ env ≡ lookup env i -sound-X[ fzero ] (x₀ ∷ env) = +sound-X[ i ] _ with fin-view i +sound-X[ .fzero ] (x₀ ∷ env) | zero = ⟦ constₚ 1 ⟧ₚ env * x₀ + ⟦ 0ₚ ⟧ₚ env ≡⟨ ap₂ (λ ϕ ψ → ϕ * x₀ + ψ) (sound-constₚ 1 env) (sound-0ₚ env) ⟩ 1 * x₀ + 0 ≡⟨ +-zeror (1 * x₀) ⟩ 1 * x₀ ≡⟨ *-onel x₀ ⟩ x₀ ∎ -sound-X[ fsuc i ] (_ ∷ env) = sound-X[ i ] env +sound-X[ .(fsuc i) ] (_ ∷ env) | suc i = sound-X[ i ] env ``` Now, for something more involved: let's show that addition of @@ -504,9 +506,9 @@ private pattern nat-lit n = def (quote Number.fromNat) (_ ∷ _ ∷ _ ∷ (lit (nat n)) v∷ _) pattern “zero” = - con (quote zero) [] + con (quote Nat.zero) [] pattern “suc” x = - con (quote suc) (x v∷ []) + con (quote Nat.suc) (x v∷ []) pattern _“+”_ x y = def (quote _+_) (x v∷ y v∷ _) pattern _“*”_ x y = diff --git a/src/Data/Rational/Base.lagda.md b/src/Data/Rational/Base.lagda.md index 317167932..e0ece9806 100644 --- a/src/Data/Rational/Base.lagda.md +++ b/src/Data/Rational/Base.lagda.md @@ -579,13 +579,15 @@ common-denominator (suc sz) fs with (c , c≠0 , nums , prfs) ← common-denomin c'≠0 = *ℤ-positive d≠0 c≠0 nums' : Fin (suc sz) → Int - nums' fzero = n *ℤ c - nums' (fsuc n) = nums n *ℤ d + nums' i with fin-view i + ... | zero = n *ℤ c + ... | suc n = nums n *ℤ d abstract prfs' : (n : Fin (suc sz)) → fs n ≈ (nums' n / c' [ c'≠0 ]) - prfs' fzero = ≈.reflᶜ' prf ≈.∙ᶜ L.inc c c≠0 (solve 3 (λ c n d → c :* n :* (d :* c) ≔ c :* (n :* c) :* d) c n d refl) - prfs' (fsuc n) = prfs n ≈.∙ᶜ L.inc d d≠0 (solve 3 (λ c n d → d :* n :* (d :* c) ≔ d :* (n :* d) :* c) c (nums n) d refl) + prfs' i with fin-view i + ... | zero = ≈.reflᶜ' prf ≈.∙ᶜ L.inc c c≠0 (solve 3 (λ c n d → c :* n :* (d :* c) ≔ c :* (n :* c) :* d) c n d refl) + ... | suc n = prfs n ≈.∙ᶜ L.inc d d≠0 (solve 3 (λ c n d → d :* n :* (d :* c) ≔ d :* (n :* d) :* c) c (nums n) d refl) -- Induction principle for n-tuples of rational numbers which reduces to -- the case of n fractions /with the same denominator/. The type is diff --git a/src/Data/Vec/Base.lagda.md b/src/Data/Vec/Base.lagda.md index c65168a5c..93a80a9ce 100644 --- a/src/Data/Vec/Base.lagda.md +++ b/src/Data/Vec/Base.lagda.md @@ -43,8 +43,9 @@ private variable n k : Nat lookup : Vec A n → Fin n → A -lookup (x ∷ xs) fzero = x -lookup (x ∷ xs) (fsuc i) = lookup xs i +lookup (x ∷ xs) n with fin-view n +... | zero = x +... | suc i = lookup xs i ```