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.lagda.md b/src/Algebra/Group.lagda.md index c0c2180e1..e591d25df 100644 --- a/src/Algebra/Group.lagda.md +++ b/src/Algebra/Group.lagda.md @@ -271,8 +271,8 @@ record make-group {ℓ} (G : Type ℓ) : Type ℓ where idl : ∀ x → mul unit x ≡ x private - inverser : ∀ x → mul x (inv x) ≡ unit - inverser x = + invr : ∀ x → mul x (inv x) ≡ unit + invr x = mul x (inv x) ≡˘⟨ idl _ ⟩ mul unit (mul x (inv x)) ≡˘⟨ ap₂ mul (invl _) refl ⟩ mul (mul (inv (inv x)) (inv x)) (mul x (inv x)) ≡˘⟨ assoc _ _ _ ⟩ @@ -282,23 +282,26 @@ record make-group {ℓ} (G : Type ℓ) : Type ℓ where mul (inv (inv x)) (inv x) ≡⟨ invl _ ⟩ unit ∎ - to-group-on : Group-on G - to-group-on .Group-on._⋆_ = mul - to-group-on .Group-on.has-is-group .is-group.unit = unit - to-group-on .Group-on.has-is-group .is-group.inverse = inv - to-group-on .Group-on.has-is-group .is-group.inversel = invl _ - to-group-on .Group-on.has-is-group .is-group.inverser = inverser _ - to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x - to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idr {x} = + to-is-group : is-group mul + to-is-group .is-group.unit = unit + to-is-group .is-group.inverse = inv + to-is-group .is-group.inversel = invl _ + to-is-group .is-group.inverser = invr _ + to-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x + to-is-group .is-group.has-is-monoid .is-monoid.idr {x} = mul x ⌜ unit ⌝ ≡˘⟨ ap¡ (invl x) ⟩ mul x (mul (inv x) x) ≡⟨ assoc _ _ _ ⟩ - mul ⌜ mul x (inv x) ⌝ x ≡⟨ ap! (inverser x) ⟩ + mul ⌜ mul x (inv x) ⌝ x ≡⟨ ap! (invr x) ⟩ mul unit x ≡⟨ idl x ⟩ x ∎ - to-group-on .Group-on.has-is-group .is-group.has-is-monoid .has-is-semigroup = + to-is-group .is-group.has-is-monoid .has-is-semigroup = record { has-is-magma = record { has-is-set = group-is-set } ; associative = λ {x y z} → assoc x y z } -open make-group using (to-group-on) public + to-group-on : Group-on G + to-group-on .Group-on._⋆_ = mul + to-group-on .Group-on.has-is-group = to-is-group + +open make-group using (to-is-group; to-group-on) public ``` diff --git a/src/Algebra/Group/Ab.lagda.md b/src/Algebra/Group/Ab.lagda.md index e0c3af059..1c8f76285 100644 --- a/src/Algebra/Group/Ab.lagda.md +++ b/src/Algebra/Group/Ab.lagda.md @@ -153,15 +153,18 @@ record make-abelian-group (T : Type ℓ) : Type ℓ where mg .make-group.invl = invl mg .make-group.idl = idl + to-is-abelian-group : is-abelian-group mul + to-is-abelian-group .is-abelian-group.has-is-group = + to-is-group make-abelian-group→make-group + to-is-abelian-group .is-abelian-group.commutes = + comm _ _ + to-group-on-ab : Group-on T to-group-on-ab = to-group-on make-abelian-group→make-group to-abelian-group-on : Abelian-group-on T to-abelian-group-on .Abelian-group-on._*_ = mul - to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.has-is-group = - Group-on.has-is-group to-group-on-ab - to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.commutes = - comm _ _ + to-abelian-group-on .Abelian-group-on.has-is-ab = to-is-abelian-group to-ab : Abelian-group ℓ ∣ to-ab .fst ∣ = T @@ -191,7 +194,7 @@ Grp→Ab→Grp G c = Σ-pathp refl go where go i .Group-on._⋆_ = G .snd .Group-on._⋆_ go i .Group-on.has-is-group = G .snd .Group-on.has-is-group -open make-abelian-group using (make-abelian-group→make-group ; to-group-on-ab ; to-abelian-group-on ; to-ab) public +open make-abelian-group using (make-abelian-group→make-group ; to-group-on-ab ; to-is-abelian-group ; to-abelian-group-on ; to-ab) public open Functor 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≃ℕ + By turning the operation parameter into an additional piece of data, we get the notion of a **magma structure** on a type, as well as the notion of a magma in general by doing the same to the carrier type. diff --git a/src/Algebra/Magma/Unital/EckmannHilton.lagda.md b/src/Algebra/Magma/Unital/EckmannHilton.lagda.md index 5140eee04..99e176bd8 100644 --- a/src/Algebra/Magma/Unital/EckmannHilton.lagda.md +++ b/src/Algebra/Magma/Unital/EckmannHilton.lagda.md @@ -102,8 +102,8 @@ unitality allows us to prove that the operation is a monoid. x ⋆ (y ⋆ z) ∎) ⋆-is-monoid : is-monoid e _⋆_ - ⋆-is-monoid .has-is-semigroup .has-is-magma = unital-mgm .has-is-magma - ⋆-is-monoid .has-is-semigroup .associative = ⋆-associative _ _ _ + ⋆-is-monoid .has-is-semigroup .is-semigroup.has-is-magma = unital-mgm .has-is-magma + ⋆-is-monoid .has-is-semigroup .is-semigroup.associative = ⋆-associative _ _ _ ⋆-is-monoid .idl = unital-mgm .idl ⋆-is-monoid .idr = unital-mgm .idr ``` diff --git a/src/Algebra/Monoid.lagda.md b/src/Algebra/Monoid.lagda.md index 7b0fefe8f..4125ac027 100644 --- a/src/Algebra/Monoid.lagda.md +++ b/src/Algebra/Monoid.lagda.md @@ -80,8 +80,6 @@ record Monoid-on (A : Type ℓ) : Type ℓ where Monoid : (ℓ : Level) → Type (lsuc ℓ) Monoid ℓ = Σ (Type ℓ) Monoid-on - -open Monoid-on ``` There is also a predicate which witnesses when an equivalence between @@ -125,7 +123,7 @@ First, we show that every monoid is a unital magma: ```agda module _ {id : A} {_⋆_ : A → A → A} where is-monoid→is-unital-magma : is-monoid id _⋆_ → is-unital-magma id _⋆_ - is-monoid→is-unital-magma mon .has-is-magma = mon .has-is-semigroup .has-is-magma + is-monoid→is-unital-magma mon .has-is-magma = mon .has-is-magma is-monoid→is-unital-magma mon .idl = mon .idl is-monoid→is-unital-magma mon .idr = mon .idr ``` @@ -172,3 +170,33 @@ monoid-inverse-unique {1M = 1M} {_⋆_} m e x y li1 ri2 = 1M ⋆ y ≡⟨ m .idl ⟩ y ∎ ``` + +# Constructing monoids + +The interface to `Monoid-on`{.Agda} is contains some annoying nesting, +so we provide an interface that arranges the data in a more user-friendly +way. + +```agda +record make-monoid {ℓ} (A : Type ℓ) : Type ℓ where + field + monoid-is-set : is-set A + _⋆_ : A → A → A + 1M : A + ⋆-assoc : ∀ x y z → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z + ⋆-idl : ∀ x → 1M ⋆ x ≡ x + ⋆-idr : ∀ x → x ⋆ 1M ≡ x + + to-is-monoid : is-monoid 1M _⋆_ + to-is-monoid .has-is-semigroup .is-semigroup.has-is-magma = record { has-is-set = monoid-is-set } + to-is-monoid .has-is-semigroup .is-semigroup.associative = ⋆-assoc _ _ _ + to-is-monoid .idl = ⋆-idl _ + to-is-monoid .idr = ⋆-idr _ + + to-monoid-on : Monoid-on A + to-monoid-on .Monoid-on.identity = 1M + to-monoid-on .Monoid-on._⋆_ = _⋆_ + to-monoid-on .Monoid-on.has-is-monoid = to-is-monoid + +open make-monoid using (to-is-monoid; to-monoid-on) public +``` diff --git a/src/Algebra/Quasigroup.lagda.md b/src/Algebra/Quasigroup.lagda.md new file mode 100644 index 000000000..e3e2b46d0 --- /dev/null +++ b/src/Algebra/Quasigroup.lagda.md @@ -0,0 +1,899 @@ +--- +description: | + Quasigroups. +--- + + +```agda +module Algebra.Quasigroup where +``` + +# Quasigroups + +Traditionally, [[groups]] are defined as [[monoids]] where every element +has a ([necessarily unique]) inverse. However, there is another path to +the theory of groups that emphasizes division/subtraction over inverses. +This perspective is especially interesting when generalizing groups to +non-associative settings; axioms of the form $xx^{-1} = 1$ are rather +ill-behaved without associativity, as inverses are no longer necessarily +unique! + +[necessarily unique]: Algebra.Monoid.html#inverses + + + +## Right quasigroups + +For the sake of maximum generality, we will build up to the definition +of quasigroups in stages, starting with right quasigroups. + +:::{.definition #right-quasigroup} +Let $\star : A \to A \to A$ be a binary operator. $(A, \star)$ is a +**right quasigroup** if $(A, \star)$ is a [[magma]], and there is some +binary operator $/ : A \to A A$, subject to the following axioms: + +- For all $x, y : A$, $(y / x) \star x = y$ +- For all $x, y : A$, $(y \star x) / x = y$ +::: + +```agda +record is-right-quasigroup {ℓ} {A : Type ℓ} (_⋆_ : A → A → A) : Type ℓ where + no-eta-equality + field + _/_ : A → A → A + /-invl : ∀ x y → (x / y) ⋆ y ≡ x + /-invr : ∀ x y → (x ⋆ y) / y ≡ x + has-is-magma : is-magma _⋆_ + + open is-magma has-is-magma public +``` + +Intuitively, the $/ : A \to A \to A$ operation acts like a sort of +right-biased division. This is further cemented by noting that +the existence of such an operation implies that every $x : A$, the action +$- \star x : A \to A$ is an [[equivalence]]. + +```agda + ⋆-equivr : ∀ x → is-equiv (_⋆ x) + ⋆-equivr x .is-eqv y .centre = y / x , /-invl y x + ⋆-equivr x .is-eqv y .paths (l , lx=y) = + Σ-prop-path (λ l → has-is-set (l ⋆ x) y) $ + y / x ≡˘⟨ ap (_/ x) lx=y ⟩ + (l ⋆ x) / x ≡⟨ /-invr l x ⟩ + l ∎ +``` + +This in turn implies that $- / x : A \to A$ is an equivalence. + +```agda + /-equivr : ∀ x → is-equiv (_/ x) + /-equivr x = inverse-is-equiv (⋆-equivr x) +``` + +As easy corollaries, we get that multiplication and division in $A$ are +right-cancellative. + + +```agda + opaque + ⋆-cancelr : ∀ {x y} (z : A) → x ⋆ z ≡ y ⋆ z → x ≡ y + ⋆-cancelr z = Equiv.injective (_⋆ z , ⋆-equivr z) + + /-cancelr : ∀ {x y} (z : A) → x / z ≡ y / z → x ≡ y + /-cancelr z = Equiv.injective (_/ z , /-equivr z) +``` + +It turns out that $- \star x$ being an equivalence is a sufficient condition +for a $A$ to be a right quasigroup, provided that $A$ is a [[set]]. + +```agda +⋆-equivr→is-right-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-set A + → (∀ x → is-equiv (_⋆ x)) + → is-right-quasigroup _⋆_ +``` + +The proof is an exercise in unrolling definitions. If $- \star x$ is an +equivalence, then $(- \star y)^{-1}(x)$ serves as a perfectly valid +definition of $x / y$; both axioms follow directly from the +unit and counit of the equivalence. + +```agda +⋆-equivr→is-right-quasigroup {_⋆_ = _⋆_} A-set ⋆-eqv = + ⋆-right-quasi + where + open is-right-quasigroup + + module ⋆-eqv x = Equiv (_⋆ x , ⋆-eqv x) + + ⋆-right-quasi : is-right-quasigroup _⋆_ + ⋆-right-quasi ._/_ x y = ⋆-eqv.from y x + ⋆-right-quasi ./-invl x y = ⋆-eqv.ε y x + ⋆-right-quasi ./-invr x y = ⋆-eqv.η y x + ⋆-right-quasi .has-is-magma .is-magma.has-is-set = A-set +``` + +We can upgrade this correspondence to an equivalence, as we definitionally +get back the same division operation we started with after round-tripping. + +```agda +is-right-quasigroup≃⋆-equivr + : ∀ {_⋆_ : A → A → A} + → is-right-quasigroup _⋆_ ≃ (is-set A × (∀ x → is-equiv (_⋆ x))) +is-right-quasigroup≃⋆-equivr {_⋆_ = _⋆_} = + Iso→Equiv $ + ⟨ has-is-set , ⋆-equivr ⟩ , + iso (uncurry ⋆-equivr→is-right-quasigroup) + (λ _ → prop!) + (λ ⋆-right-quasi → + let open is-right-quasigroup ⋆-right-quasi in + Iso.injective eqv (refl ,ₚ prop!)) + where + open is-right-quasigroup + unquoteDecl eqv = declare-record-iso eqv (quote is-right-quasigroup) +``` + +Crucially, this means that the division operation $/ : A \to A \to A$ +is actually a [[property]] rather than structure, as both `is-equiv`{.Agda} and +`is-set`{.Agda} are propositions. + +```agda +is-right-quasigroup-is-prop + : ∀ {_⋆_ : A → A → A} + → is-prop (is-right-quasigroup _⋆_) +is-right-quasigroup-is-prop {A = A} = + Equiv→is-hlevel 1 is-right-quasigroup≃⋆-equivr (hlevel 1) +``` + + + +### Right quasigroup homomorphisms + +In the previous section, we proved that the existence of a right division +operation was actually a property of a magma, rather than structure. We shall now see +that right division is automatically preserved by magma homomorphisms. + +We start by defining the corresponding notion of structure for right +quasigroups. + +:::{.definition #right-quasigroup-structure} +A **right quasigroup structure** on a type $A$ is a binary operation +$\star : A \to A \to A$ such that $(A, \star)$ is a right quasigroup. +::: + +```agda +record Right-quasigroup-on {ℓ} (A : Type ℓ) : Type ℓ where + no-eta-equality + field + _⋆_ : A → A → A + has-is-right-quasigroup : is-right-quasigroup _⋆_ + + open is-right-quasigroup has-is-right-quasigroup public + +``` + +:::{.definition #right-quasigroup-homomorphism} +A **right quasigroup homomorphism** between two right quasigroups $A, B$ +is a function $f : A \to B$ such that $f (x \star y) = f x \star f y$. +::: + +```agda +record is-right-quasigroup-hom + {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + (f : A → B) + (S : Right-quasigroup-on A) (T : Right-quasigroup-on B) + : Type (ℓ ⊔ ℓ') + where + no-eta-equality + private + module A = Right-quasigroup-on S + module B = Right-quasigroup-on T + field + pres-⋆ : ∀ x y → f (x A.⋆ y) ≡ f x B.⋆ f y +``` + +Preservation of right division follows almost immediately from +right-cancellativity. + + +```agda + pres-/ : ∀ x y → f (x A./ y) ≡ f x B./ f y + pres-/ x y = + B.⋆-cancelr (f y) $ + f (x A./ y) B.⋆ f y ≡˘⟨ pres-⋆ (x A./ y) y ⟩ + f ((x A./ y) A.⋆ y) ≡⟨ ap f (A./-invl x y) ⟩ + f x ≡˘⟨ B./-invl (f x) (f y) ⟩ + (f x B./ f y) B.⋆ f y ∎ +``` + + + + + +Right quasigroups are algebraic structures, so they form a [[thin structure]] +over $\Sets$. + +```agda + Right-quasigroup-structure : ∀ ℓ → Thin-structure ℓ Right-quasigroup-on + Right-quasigroup-structure ℓ .is-hom f A B .∣_∣ = + is-right-quasigroup-hom f A B + Right-quasigroup-structure ℓ .is-hom f A B .is-tr = + is-right-quasigroup-hom-is-prop + Right-quasigroup-structure ℓ .id-is-hom .pres-⋆ x y = + refl + Right-quasigroup-structure ℓ .∘-is-hom f g f-hom g-hom .pres-⋆ x y = + ap f (g-hom .pres-⋆ x y) ∙ f-hom .pres-⋆ (g x) (g y) + Right-quasigroup-structure ℓ .id-hom-unique {A} {S} {T} p q = + Right-quasigroup-on-pathp (ext (p .pres-⋆)) + +``` + +This observation lets us neatly organize right quasigroups into a [[category]]. + +```agda +Right-quasigroups : ∀ ℓ → Precategory (lsuc ℓ) ℓ +Right-quasigroups ℓ = Structured-objects (Right-quasigroup-structure ℓ) + +module Right-quasigroups {ℓ} = Cat.Reasoning (Right-quasigroups ℓ) + +Right-quasigroup : (ℓ : Level) → Type (lsuc ℓ) +Right-quasigroup ℓ = Right-quasigroups.Ob {ℓ} +``` + + + + +## Left quasigroups + +We can dualise the definition of right quasigroups to arrive at the +notion of a **left quasigroup**. + +:::{.definition #left-quasigroup} +Let $\star : A \to A \to A$ be a binary operator. $(A, \star)$ is a +**left quasigroup** if $(A, \star)$ is a [[magma]], and there is some +binary operator $\backslash : A \to A \to A$, subject to the following axioms: + +- For all $x, y : A$, $x \star (x \backslash y) = y$ +- For all $x, y : A$, $x \backslash (x \star y) = y$ +::: + + +```agda +record is-left-quasigroup {ℓ} {A : Type ℓ} (_⋆_ : A → A → A) : Type ℓ where + no-eta-equality + field + _⧵_ : A → A → A + ⧵-invr : ∀ x y → x ⋆ (x ⧵ y) ≡ y + ⧵-invl : ∀ x y → x ⧵ (x ⋆ y) ≡ y + has-is-magma : is-magma _⋆_ + + open is-magma has-is-magma public +``` + +Intuitively, we should think of $x \backslash y$ as "$y$ divided by $x$" or +"$y$ over $x$". This is reinforced by the fact that for every $x : A$, the action +$x \star - : A \to A$ is an [[equivalence]]. + +```agda + ⋆-equivl : ∀ x → is-equiv (x ⋆_) + ⋆-equivl x .is-eqv y .centre = x ⧵ y , ⧵-invr x y + ⋆-equivl x .is-eqv y .paths (r , xr=y) = + Σ-prop-path (λ r → has-is-set (x ⋆ r) y) $ + x ⧵ y ≡˘⟨ ap (x ⧵_) xr=y ⟩ + x ⧵ (x ⋆ r) ≡⟨ ⧵-invl x r ⟩ + r ∎ + + ⧵-equivl : ∀ x → is-equiv (x ⧵_) + ⧵-equivl x = inverse-is-equiv (⋆-equivl x) +``` + +This implies that that multiplication and division in $A$ is left-cancellative. + +```agda + opaque + ⋆-cancell : ∀ (x : A) {y z} → x ⋆ y ≡ x ⋆ z → y ≡ z + ⋆-cancell x = Equiv.injective (x ⋆_ , ⋆-equivl x) + + ⧵-cancell : ∀ (x : A) {y z} → x ⧵ y ≡ x ⧵ z → y ≡ z + ⧵-cancell x = Equiv.injective (x ⧵_ , ⧵-equivl x) +``` + +Next, we shall show that left quasigroups are formally dual to right quasigroups. + +```agda +is-left-quasigroup≃op-is-right-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-left-quasigroup _⋆_ ≃ is-right-quasigroup (λ x y → y ⋆ x) +``` + +
+The proof of this fact is rather tedious, so we will omit the +details. + + +```agda +is-left-quasigroup→op-is-right-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-left-quasigroup _⋆_ → is-right-quasigroup (λ x y → y ⋆ x) + +is-right-quasigroup→op-is-left-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-right-quasigroup _⋆_ → is-left-quasigroup (λ x y → y ⋆ x) + +is-left-quasigroup→op-is-right-quasigroup {_⋆_ = _⋆_} A-quasi = A-op-quasi + where + open is-left-quasigroup A-quasi + open is-right-quasigroup + + A-op-quasi : is-right-quasigroup (λ x y → y ⋆ x) + A-op-quasi ._/_ x y = y ⧵ x + A-op-quasi ./-invr = flip ⧵-invl + A-op-quasi ./-invl = flip ⧵-invr + A-op-quasi .has-is-magma .is-magma.has-is-set = hlevel 2 + +is-right-quasigroup→op-is-left-quasigroup {_⋆_ = _⋆_} A-quasi = A-op-quasi + where + open is-right-quasigroup A-quasi + open is-left-quasigroup + + A-op-quasi : is-left-quasigroup (λ x y → y ⋆ x) + A-op-quasi ._⧵_ x y = y / x + A-op-quasi .⧵-invr = flip /-invl + A-op-quasi .⧵-invl = flip /-invr + A-op-quasi .has-is-magma .is-magma.has-is-set = hlevel 2 + +is-left-quasigroup≃op-is-right-quasigroup = + Iso→Equiv $ + is-left-quasigroup→op-is-right-quasigroup , + iso is-right-quasigroup→op-is-left-quasigroup + (λ _ → prop!) + (λ ⋆-left-quasi → + let open is-left-quasigroup ⋆-left-quasi in + Iso.injective eqv (refl ,ₚ prop!)) + where + private unquoteDecl eqv = declare-record-iso eqv (quote is-left-quasigroup) +``` +
+ + +This in turn means that being a left quasigroup is a property of a binary +operation. + +```agda +is-left-quasigroup-is-prop + : ∀ {_⋆_ : A → A → A} + → is-prop (is-left-quasigroup _⋆_) +is-left-quasigroup-is-prop {A = A} = + Equiv→is-hlevel 1 (is-left-quasigroup≃op-is-right-quasigroup) (hlevel 1) +``` + + + + + +### Left quasigroup homomorphisms + +We can continue dualizing to define a notion of homomorphism for +left quasigroups, though we shall be much more terse in our development. +Following the pattern of right quasigroups, we begin by defining +**left quasigroup structures**. + + +:::{.definition #left-quasigroup-structure} +A **left quasigroup structure** on a type $A$ is a binary operation +$\star : A \to A \to A$ such that $(A, \star)$ is a left quasigroup. +::: + +```agda +record Left-quasigroup-on {ℓ} (A : Type ℓ) : Type ℓ where + no-eta-equality + field + _⋆_ : A → A → A + has-is-left-quasigroup : is-left-quasigroup _⋆_ + + open is-left-quasigroup has-is-left-quasigroup public +``` + + +:::{.definition #left-quasigroup-homomorphism} +A **left quasigroup homomorphism** between two left quasigroups $A, B$ +is a function $f : A \to B$ such that $f (x \star y) = f x \star f y$. +::: + +```agda +record is-left-quasigroup-hom + {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + (f : A → B) + (S : Left-quasigroup-on A) (T : Left-quasigroup-on B) + : Type (ℓ ⊔ ℓ') + where + no-eta-equality + private + module A = Left-quasigroup-on S + module B = Left-quasigroup-on T + field + pres-⋆ : ∀ x y → f (x A.⋆ y) ≡ f x B.⋆ f y +``` + +Dual to right quasigroups, preservation of left division follows from +left-cancellativity. + +```agda + pres-⧵ : ∀ x y → f (x A.⧵ y) ≡ f x B.⧵ f y + pres-⧵ x y = + B.⋆-cancell (f x) $ + f x B.⋆ f (x A.⧵ y) ≡˘⟨ pres-⋆ x (x A.⧵ y) ⟩ + f (x A.⋆ (x A.⧵ y)) ≡⟨ ap f (A.⧵-invr x y) ⟩ + f y ≡˘⟨ B.⧵-invr (f x) (f y) ⟩ + f x B.⋆ (f x B.⧵ f y) ∎ +``` + + + +Left quasigroups are algebraic structures, so they form a [[thin structure]] +over $\Sets$. + + + +```agda + Left-quasigroup-structure : ∀ ℓ → Thin-structure ℓ Left-quasigroup-on + Left-quasigroup-structure ℓ .is-hom f A B .∣_∣ = + is-left-quasigroup-hom f A B + Left-quasigroup-structure ℓ .is-hom f A B .is-tr = + is-left-quasigroup-hom-is-prop + Left-quasigroup-structure ℓ .id-is-hom .pres-⋆ x y = + refl + Left-quasigroup-structure ℓ .∘-is-hom f g f-hom g-hom .pres-⋆ x y = + ap f (g-hom .pres-⋆ x y) ∙ f-hom .pres-⋆ (g x) (g y) + Left-quasigroup-structure ℓ .id-hom-unique p q = + Left-quasigroup-on-pathp (ext (p .pres-⋆)) +``` + +This observation lets us assemble left quasigroups into a [[category]]. + +```agda +Left-quasigroups : ∀ ℓ → Precategory (lsuc ℓ) ℓ +Left-quasigroups ℓ = Structured-objects (Left-quasigroup-structure ℓ) + +module Left-quasigroups {ℓ} = Cat.Reasoning (Left-quasigroups ℓ) + +Left-quasigroup : (ℓ : Level) → Type (lsuc ℓ) +Left-quasigroup ℓ = Left-quasigroups.Ob {ℓ} +``` + + + + +## Quasigroups + +:::{.definition #quasigroup} +A type $A$ equipped with a binary operation $\star : A \to A \to A$ is +a **quasigroup** if it is a [[left quasigroup]] and a [[right quasigroup]]. +::: + + +```agda +record is-quasigroup {ℓ} {A : Type ℓ} (_⋆_ : A → A → A) : Type ℓ where + no-eta-equality + field + has-is-left-quasigroup : is-left-quasigroup _⋆_ + has-is-right-quasigroup : is-right-quasigroup _⋆_ +``` + + + +Quasigroups obey the **latin square property**: for every $x, y : A$, +there exists a unique pair $l, r : A$ such that $l \star x = y$ and $x \star r = y$. + +```agda + ⋆-latin : ∀ x y → is-contr (Σ[ l ∈ A ] Σ[ r ∈ A ] (l ⋆ x ≡ y × x ⋆ r ≡ y)) +``` + +The proof is an exercise in equivalence yoga: by definition, a quasigroup +is both a left and right quasigroup, so multiplication on the left and right +is an equivalence, so the types $\Sigma (l : A) l \star x = y$ and +$\Sigma (r : A) r \star x = y$ are both contractible. Moreover, +$(\Sigma (l : A) l \star x = y) \times (\Sigma (r : A) r \star x = y)$ is +equivalent to $\Sigma (l : A) \Sigma (r : A) (l \star x = y \times x \star r = y)$, +so the latter must also be contractible. + +```agda + ⋆-latin x y = + Equiv→is-hlevel 0 + latin-eqv + (×-is-hlevel 0 (⋆-equivr x .is-eqv y) (⋆-equivl x .is-eqv y)) + where + latin-eqv + : (Σ[ l ∈ A ] Σ[ r ∈ A ] (l ⋆ x ≡ y × x ⋆ r ≡ y)) + ≃ ((Σ[ l ∈ A ] l ⋆ x ≡ y) × (Σ[ r ∈ A ] x ⋆ r ≡ y)) + latin-eqv = + Σ[ l ∈ A ] Σ[ r ∈ A ] (l ⋆ x ≡ y × x ⋆ r ≡ y) ≃⟨ Σ-ap id≃ (λ l → Σ-swap₂) ⟩ + Σ[ l ∈ A ] (l ⋆ x ≡ y × (Σ[ r ∈ A ] (x ⋆ r) ≡ y)) ≃⟨ Σ-assoc ⟩ + (Σ[ l ∈ A ] l ⋆ x ≡ y) × (Σ[ r ∈ A ] x ⋆ r ≡ y) ≃∎ +``` + +We also have the following pair of useful identities that relate +left and right division. + +```agda + /-⧵-cancelr : ∀ x y → x / (y ⧵ x) ≡ y + /-⧵-cancelr x y = + x / (y ⧵ x) ≡˘⟨ ap (_/ (y ⧵ x)) (⧵-invr y x) ⟩ + (y ⋆ (y ⧵ x)) / (y ⧵ x) ≡⟨ /-invr y (y ⧵ x) ⟩ + y ∎ + + /-⧵-cancell : ∀ x y → (x / y) ⧵ x ≡ y + /-⧵-cancell x y = + (x / y) ⧵ x ≡˘⟨ ap ((x / y) ⧵_) (/-invl x y) ⟩ + (x / y) ⧵ ((x / y) ⋆ y) ≡⟨ ⧵-invl (x / y) y ⟩ + y ∎ +``` + + + +### Quasigroup homomorphisms + +:::{.definition #quasigroup-structure} +A **quasigroup structure** on a type $A$ is a binary operation +$\star : A \to A \to A$ such that $(A, \star)$ is a quasigroup. +::: + +```agda +record Quasigroup-on {ℓ} (A : Type ℓ) : Type ℓ where + no-eta-equality + field + _⋆_ : A → A → A + has-is-quasigroup : is-quasigroup _⋆_ + + open is-quasigroup has-is-quasigroup public +``` + + + +:::{.definition #quasigroup-homomorphism} +A **quasigroup homomorphism** between two quasigroups $A, B$ +is a function $f : A \to B$ such that $f (x \star y) = f x \star f y$. +::: + + +```agda +record is-quasigroup-hom + {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + (f : A → B) + (S : Quasigroup-on A) (T : Quasigroup-on B) + : Type (ℓ ⊔ ℓ') + where + no-eta-equality + private + module A = Quasigroup-on S + module B = Quasigroup-on T + field + pres-⋆ : ∀ x y → f (x A.⋆ y) ≡ f x B.⋆ f y +``` + + + + + + + +Quasigroups and quasigroup homomorphisms form a [[thin structure]]. + +```agda + Quasigroup-structure : ∀ ℓ → Thin-structure ℓ Quasigroup-on +``` + +
+ + + +```agda + Quasigroup-structure ℓ .is-hom f A B .∣_∣ = + is-quasigroup-hom f A B + Quasigroup-structure ℓ .is-hom f A B .is-tr = + is-quasigroup-hom-is-prop + Quasigroup-structure ℓ .id-is-hom .pres-⋆ x y = + refl + Quasigroup-structure ℓ .∘-is-hom f g f-hom g-hom .pres-⋆ x y = + ap f (g-hom .pres-⋆ x y) ∙ f-hom .pres-⋆ (g x) (g y) + Quasigroup-structure ℓ .id-hom-unique p q = + Quasigroup-on-pathp (ext (p .pres-⋆)) +``` +
+ +This gives us a tidy way to construct the category of quasigroups. + +```agda +Quasigroups : ∀ ℓ → Precategory (lsuc ℓ) ℓ +Quasigroups ℓ = Structured-objects (Quasigroup-structure ℓ) + +module Quasigroups {ℓ} = Cat.Reasoning (Quasigroups ℓ) + +Quasigroup : (ℓ : Level) → Type (lsuc ℓ) +Quasigroup ℓ = Quasigroups.Ob {ℓ} +``` + + + +## Constructing quasigroups + +The interfaces for `is-quasigroup`{.Agda} and `Quasigroup-on`{.Agda} are +deeply nested and contain some duplication, so we introduce some helper +functions for constructing them. + +```agda +record make-quasigroup {ℓ} (A : Type ℓ) : Type ℓ where + field + quasigroup-is-set : is-set A + _⋆_ : A → A → A + _⧵_ : A → A → A + _/_ : A → A → A + + /-invl : ∀ x y → (x / y) ⋆ y ≡ x + /-invr : ∀ x y → (x ⋆ y) / y ≡ x + ⧵-invr : ∀ x y → x ⋆ (x ⧵ y) ≡ y + ⧵-invl : ∀ x y → x ⧵ (x ⋆ y) ≡ y +``` + + diff --git a/src/Algebra/Quasigroup/Instances/Group.lagda.md b/src/Algebra/Quasigroup/Instances/Group.lagda.md new file mode 100644 index 000000000..2b157e6d9 --- /dev/null +++ b/src/Algebra/Quasigroup/Instances/Group.lagda.md @@ -0,0 +1,169 @@ +--- +description: | + Groups and quasigroups +--- + +```agda +module Algebra.Quasigroup.Instances.Group where +``` + +# Groups and quasigroups + + + +Every [[group]] is a [[quasigroup]], as multiplication in a group is +an equivalence. + +```agda +is-group→is-left-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-group _⋆_ + → is-left-quasigroup _⋆_ +is-group→is-left-quasigroup {_⋆_ = _⋆_} ⋆-group = + ⋆-equivl→is-left-quasigroup (hlevel 2) ⋆-equivl + where open is-group ⋆-group + +is-group→is-right-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-group _⋆_ + → is-right-quasigroup _⋆_ +is-group→is-right-quasigroup {_⋆_ = _⋆_} ⋆-group = + ⋆-equivr→is-right-quasigroup (hlevel 2) ⋆-equivr + where open is-group ⋆-group + +is-group→is-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-group _⋆_ + → is-quasigroup _⋆_ +is-group→is-quasigroup {_⋆_ = _⋆_} ⋆-group .is-quasigroup.has-is-left-quasigroup = + is-group→is-left-quasigroup ⋆-group +is-group→is-quasigroup {_⋆_ = _⋆_} ⋆-group .is-quasigroup.has-is-right-quasigroup = + is-group→is-right-quasigroup ⋆-group +``` + +## Associative quasigroups as groups + +Conversely, if a quasigroup $(A, \star)$ is merely inhabited and associative, +then it is a group. + +```agda +associative+is-quasigroup→is-group + : ∀ {_⋆_ : A → A → A} + → ∥ A ∥ + → (∀ x y z → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z) + → is-quasigroup _⋆_ + → is-group _⋆_ +``` + +We start by observing that `is-group` is an h-prop, so it suffices to +consider the case where $A$ is inhabited. + +```agda +associative+is-quasigroup→is-group {A = A} {_⋆_ = _⋆_} ∥a∥ ⋆-assoc ⋆-quasi = + rec! (λ a → to-is-group (⋆-group a)) ∥a∥ +``` + + + +Next, a useful technical lemma: if $a \star x = b \star y$, then +$x \backslash a = b / y$. + +```agda + ⧵-/-comm + : ∀ {a b x y} + → x ⋆ b ≡ a ⋆ y + → x ⧵ a ≡ b / y +``` + +The proof is an elegant bit of algebra. Recall that in a quasigroup, +$\star$ is left and right cancellative, so it suffices to show that: + +$$(x \star (x \backslash a)) \star y = (x \star (b / y)) \star y$$ + +Next, $(x \star (x \backslash a)) \star y = a \star y$, and $a \star y = x \star b$, +so it remains to show that $x \star b = (x \star (b / y)) \star y$. Crucially, +$\star$ is associative, so: + +$$ +(x \star (b / y)) \star y = x \star ((b / y) \star y) = x \star b +$$ + +which completes the proof. + +```agda + ⧵-/-comm {a} {b} {x} {y} comm = + ⋆-cancell x $ ⋆-cancelr y $ + (x ⋆ (x ⧵ a)) ⋆ y ≡⟨ ap (_⋆ y) (⧵-invr x a) ⟩ + a ⋆ y ≡˘⟨ comm ⟩ + x ⋆ b ≡˘⟨ ap (x ⋆_) (/-invl b y) ⟩ + x ⋆ ((b / y) ⋆ y) ≡⟨ ⋆-assoc x (b / y) y ⟩ + (x ⋆ (b / y)) ⋆ y ∎ +``` + +With that out of the way, we shall show that + +$$(A, \star, (a \backslash a), (\lambda x. (a \backslash a) / x))$$ + +forms a group for any $a : A$. + +```agda + ⋆-group : A → make-group A + ⋆-group a .group-is-set = hlevel 2 + ⋆-group a .unit = a ⧵ a + ⋆-group a .mul x y = x ⋆ y + ⋆-group a .inv x = (a ⧵ a) / x +``` + +Associativity is one of our hypotheses, so all that remains is left +inverses and left identities. Next, note that + +$$ +(a \backslash a), (\lambda x. (a \backslash a) / x)) \star x = (a \backslash a) +$$ + +is just one of the quasigroup axioms. Finally, our lemma gives us +$a \backslash a = x / x$, so we have: + +$$ +(a \backslash a) \star x = (x / x) \star x = x +$$ + +which completes the proof. + +```agda + ⋆-group a .assoc x y z = + ⋆-assoc x y z + ⋆-group a .invl x = + /-invl (a ⧵ a) x + ⋆-group a .idl x = + (a ⧵ a) ⋆ x ≡⟨ ap (_⋆ x) (⧵-/-comm refl) ⟩ + (x / x) ⋆ x ≡⟨ /-invl x x ⟩ + x ∎ +``` + +Taking a step back, this result demonstrates that associative quasigroups +behave like potentially empty groups. diff --git a/src/Algebra/Quasigroup/Instances/Initial.lagda.md b/src/Algebra/Quasigroup/Instances/Initial.lagda.md new file mode 100644 index 000000000..ad84c437a --- /dev/null +++ b/src/Algebra/Quasigroup/Instances/Initial.lagda.md @@ -0,0 +1,80 @@ +--- +description: | + The initial quasigroup. +--- + + +```agda +module Algebra.Quasigroup.Instances.Initial where +``` + +# The initial quasigroup {defines="initial-quasigroup empty-quasigroup"} + +The empty type trivially forms a [[quasigroup]]. + + + +```agda +Empty-quasigroup : ∀ {ℓ} → Quasigroup ℓ +Empty-quasigroup = to-quasigroup ⊥-quasigroup where + open make-quasigroup + + ⊥-quasigroup : make-quasigroup (Lift _ ⊥) + ⊥-quasigroup .quasigroup-is-set = hlevel 2 + ⊥-quasigroup ._⋆_ () + ⊥-quasigroup ._⧵_ () + ⊥-quasigroup ._/_ () + ⊥-quasigroup ./-invl () + ⊥-quasigroup ./-invr () + ⊥-quasigroup .⧵-invr () + ⊥-quasigroup .⧵-invl () +``` + +Moreover, the empty quasigroup is an [[initial object]] in the category +of quasigroups, as there is a unique function out of the empty type. + +```agda +Empty-quasigroup-is-initial : is-initial (Quasigroups ℓ) Empty-quasigroup +Empty-quasigroup-is-initial A .centre .hom () +Empty-quasigroup-is-initial A .centre .preserves .is-quasigroup-hom.pres-⋆ () +Empty-quasigroup-is-initial A .paths f = ext λ () + +Initial-quasigroup : Initial (Quasigroups ℓ) +Initial-quasigroup .Initial.bot = Empty-quasigroup +Initial-quasigroup .Initial.has⊥ = Empty-quasigroup-is-initial +``` + +In fact, the empty quasigroup is a [[strict initial object]]. + +```agda +Initial-quasigroup-is-strict + : is-strict-initial (Quasigroups ℓ) Initial-quasigroup +Initial-quasigroup-is-strict = + make-is-strict-initial (Quasigroups _) Initial-quasigroup $ λ A f → ext λ a → + absurd (Lift.lower (f # a)) +``` + + diff --git a/src/Algebra/Ring.lagda.md b/src/Algebra/Ring.lagda.md index 167777f48..77f320e93 100644 --- a/src/Algebra/Ring.lagda.md +++ b/src/Algebra/Ring.lagda.md @@ -231,37 +231,35 @@ record make-ring {ℓ} (R : Type ℓ) : Type ℓ where diff --git a/src/Algebra/Ring/Module/Multilinear.lagda.md b/src/Algebra/Ring/Module/Multilinear.lagda.md index 57a075561..20b3dd6cc 100644 --- a/src/Algebra/Ring/Module/Multilinear.lagda.md +++ b/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 diff --git a/src/Algebra/Ring/Solver.agda b/src/Algebra/Ring/Solver.agda index 33cec2c3d..a53d36ade 100644 --- a/src/Algebra/Ring/Solver.agda +++ b/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 ρ) diff --git a/src/Algebra/Semigroup.lagda.md b/src/Algebra/Semigroup.lagda.md index 02c0759a8..d830498c7 100644 --- a/src/Algebra/Semigroup.lagda.md +++ b/src/Algebra/Semigroup.lagda.md @@ -34,7 +34,7 @@ equipped with a choice of _associative_ binary operation `⋆`. open is-magma has-is-magma public -open is-semigroup public +open is-semigroup ``` To see why the [[set truncation]] is really necessary, it helps to @@ -147,7 +147,7 @@ open import Data.Nat.Order open import Data.Nat.Base Nat-min : is-semigroup min -Nat-min .has-is-magma .has-is-set = Nat-is-set +Nat-min .has-is-magma .is-magma.has-is-set = Nat-is-set Nat-min .associative = min-assoc _ _ _ ``` @@ -164,3 +164,27 @@ private sucx≤x = subst (λ e → e ≤ x) (id (suc x)) (min-≤l x (suc x)) in ¬sucx≤x x sucx≤x ``` + +# Constructing semigroups + +The interface to `Semigroup-on`{.Agda} is contains some annoying nesting, +so we provide an interface that arranges the data in a more user-friendly +way. + +```agda +record make-semigroup {ℓ} (A : Type ℓ) : Type ℓ where + field + semigroup-is-set : is-set A + _⋆_ : A → A → A + ⋆-assoc : ∀ x y z → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z + + to-is-semigroup : is-semigroup _⋆_ + to-is-semigroup .has-is-magma .is-magma.has-is-set = semigroup-is-set + to-is-semigroup .associative = ⋆-assoc _ _ _ + + to-semigroup-on : Semigroup-on A + to-semigroup-on .fst = _⋆_ + to-semigroup-on .snd = to-is-semigroup + +open make-semigroup using (to-is-semigroup; to-semigroup-on) public +``` diff --git a/src/Cat/Diagram/Initial.lagda.md b/src/Cat/Diagram/Initial.lagda.md index 12256894d..db090ac2c 100644 --- a/src/Cat/Diagram/Initial.lagda.md +++ b/src/Cat/Diagram/Initial.lagda.md @@ -93,7 +93,7 @@ a proposition: (x1 .has⊥ ob) (x2 .has⊥ ob) i ``` -## Strictness +## Strictness {defines="strict-initial-object"} An initial object is said to be *[strict]* if every morphism into it is an *iso*morphism. This is a categorical generalization of the fact that if one can write a function $X \to \bot$ then $X$ must itself be empty. @@ -121,6 +121,19 @@ Strictness is a property of, not structure on, an initial object. is-strict-initial-is-prop i = hlevel 1 ``` +As maps out of initial objects are unique, it suffices to show that +every map $\text{!`} \circ f = id$ for every $f : X \to \bot$ to establish that $\bot$ is a +strict initial object. + +```agda + make-is-strict-initial + : (i : Initial) + → (∀ x → (f : Hom x (i .bot)) → (¡ i) ∘ f ≡ id) + → is-strict-initial i + make-is-strict-initial i p x f = + make-invertible (¡ i) (¡-unique₂ i (f ∘ ¡ i) id) (p x f) +``` + -# Thinly displayed structures +# Thinly displayed structures {defines=thin-structure} The HoTT Book's version of the structure identity principle can be seen as a very early example of [[displayed category]] theory. Their diff --git a/src/Cat/Instances/Shape/Cospan.lagda.md b/src/Cat/Instances/Shape/Cospan.lagda.md index 1475920bf..34f28cc5f 100644 --- a/src/Cat/Instances/Shape/Cospan.lagda.md +++ b/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 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/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md b/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md index 370ca9a92..9cb4c5e6c 100644 --- a/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md +++ b/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md @@ -92,12 +92,13 @@ $$. ```agda Mon→Hom-mon : ∀ {m} (x : Ob) → C-Monoid m → Monoid-on (Hom x m) - Mon→Hom-mon {m} x mon = hom-mon where - has-semigroup : is-semigroup λ f g → mon .μ ∘ ⟨ f , g ⟩ - hom-mon : Monoid-on (Hom x m) + Mon→Hom-mon {m} x mon = to-monoid-on hom-mon where + open make-monoid - hom-mon .Monoid-on.identity = mon .η ∘ ! - hom-mon .Monoid-on._⋆_ f g = mon .μ ∘ ⟨ f , g ⟩ + hom-mon : make-monoid (Hom x m) + hom-mon .monoid-is-set = hlevel 2 + hom-mon ._⋆_ f g = mon .μ ∘ ⟨ f , g ⟩ + hom-mon .1M = mon .η ∘ ! ```
@@ -105,24 +106,21 @@ $$. diagram "relativize" to each $\hom$-set. ```agda - hom-mon .Monoid-on.has-is-monoid .has-is-semigroup = has-semigroup - hom-mon .Monoid-on.has-is-monoid .mon-idl {f} = + hom-mon .⋆-assoc f g h = + mon .μ ∘ ⟨ f , mon .μ ∘ ⟨ g , h ⟩ ⟩ ≡⟨ products! C prod ⟩ + mon .μ ∘ (id ⊗₁ mon .μ) ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≡⟨ extendl (mon .μ-assoc) ⟩ + mon .μ ∘ ((mon .μ ⊗₁ id) ∘ ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩) ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≡⟨ products! C prod ⟩ + mon .μ ∘ ⟨ mon .μ ∘ ⟨ f , g ⟩ , h ⟩ ∎ + hom-mon .⋆-idl f = mon .μ ∘ ⟨ mon .η ∘ ! , f ⟩ ≡⟨ products! C prod ⟩ mon .μ ∘ (mon .η ⊗₁ id) ∘ ⟨ ! , f ⟩ ≡⟨ pulll (mon .μ-unitl) ⟩ π₂ ∘ ⟨ ! , f ⟩ ≡⟨ π₂∘⟨⟩ ⟩ f ∎ - hom-mon .Monoid-on.has-is-monoid .mon-idr {f} = + hom-mon .⋆-idr f = mon .μ ∘ ⟨ f , mon .η ∘ ! ⟩ ≡⟨ products! C prod ⟩ mon .μ ∘ (id ⊗₁ mon .η) ∘ ⟨ f , ! ⟩ ≡⟨ pulll (mon .μ-unitr) ⟩ π₁ ∘ ⟨ f , ! ⟩ ≡⟨ π₁∘⟨⟩ ⟩ f ∎ - - has-semigroup .has-is-magma .has-is-set = Hom-set _ _ - has-semigroup .associative {f} {g} {h} = - mon .μ ∘ ⟨ f , mon .μ ∘ ⟨ g , h ⟩ ⟩ ≡⟨ products! C prod ⟩ - mon .μ ∘ (id ⊗₁ mon .μ) ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≡⟨ extendl (mon .μ-assoc) ⟩ - mon .μ ∘ ((mon .μ ⊗₁ id) ∘ ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩) ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≡⟨ products! C prod ⟩ - mon .μ ∘ ⟨ mon .μ ∘ ⟨ f , g ⟩ , h ⟩ ∎ ```
@@ -385,7 +383,7 @@ object $M : \cC$. : ∀ (P : Functor (C ^op) (Monoids ℓ)) → (P-rep : Representation {C = C} (Mon↪Sets F∘ P)) → C-Monoid (P-rep .rep) - RepPshMon→Mon P P-rep = Hom-mon→Mon hom-mon η*-nat μ*-nat + RepPshMon→Mon P P-rep = Hom-mon→Mon (λ x → to-monoid-on (hom-mon x)) η*-nat μ*-nat module RepPshMon→Mon where ``` @@ -453,14 +451,13 @@ the monoid structure $P(x)$ to a monoid structure on $x \to M$. diff --git a/src/Data/Dec/Base.lagda.md b/src/Data/Dec/Base.lagda.md index e4bf2476b..4aa0a1fb9 100644 --- a/src/Data/Dec/Base.lagda.md +++ b/src/Data/Dec/Base.lagda.md @@ -153,6 +153,7 @@ instance Dec-→ {Q = _} ⦃ yes p ⦄ ⦃ yes q ⦄ = yes λ _ → q Dec-→ {Q = _} ⦃ yes p ⦄ ⦃ no ¬q ⦄ = no λ pq → ¬q (pq p) Dec-→ {Q = _} ⦃ no ¬p ⦄ ⦃ q ⦄ = yes λ p → absurd (¬p p) + {-# INCOHERENT Dec-→ #-} Dec-⊤ : Dec ⊤ Dec-⊤ = yes tt 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 ```