diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 7f305992a..1300a2439 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -58,7 +58,7 @@ jobs: - name: Typecheck 👩‍🏫 run: | nix-shell --run "$build_command" - # Run Agda as a separate stage so it doesn't have to be subject to + # Run Mikan as a separate stage so it doesn't have to be subject to # the absolutely spartan GC tuning parameters we run the build in # CI with env: @@ -66,7 +66,7 @@ jobs: build_command: | set -eu 1lab-shake _build/all-pages.agda - agda-nodebug _build/all-pages.agda -j4 +RTS -s -RTS + mikan-nodebug _build/all-pages.agda -j4 +RTS -s -RTS - name: Build 🛠️ run: | diff --git a/1lab.agda-lib b/1lab.agda-lib index 015a9c8f9..5beab3325 100644 --- a/1lab.agda-lib +++ b/1lab.agda-lib @@ -4,12 +4,8 @@ include: wip _build flags: - --cubical + --prop --no-load-primitives --postfix-projections - --rewriting - --guardedness - --two-level -W noUnsupportedIndexedMatch - -W noRewriteVariablesBoundInSingleton --experimental-lazy-instances diff --git a/cabal.project b/cabal.project index ae9320da1..4b383a523 100644 --- a/cabal.project +++ b/cabal.project @@ -1,12 +1,12 @@ packages: support/shake/1lab-shake.cabal -- To build outside of the Nix shell, uncomment the following stanza --- and replace `master` with the `rev` field from `support/nix/dep/Agda/github.json`. +-- and replace `main` with the `rev` field from `support/nix/dep/mikan/github.json`. -- -- If you want to avoid polluting your Git tree, you can move this to -- `cabal.project.local`, which is ignored by Git. -- source-repository-package -- type: git --- location: https://github.com/agda/agda.git +-- location: https://codeberg.org/1lab/mikan.git -- tag: master diff --git a/default.nix b/default.nix index 42a6c5b31..e5762ab2e 100644 --- a/default.nix +++ b/default.nix @@ -98,7 +98,7 @@ in passthru = { inherit pkgs shakefile deps sort-imports nodeModules; - inherit (pkgs.labHaskellPackages) Agda; + inherit (pkgs.labHaskellPackages) Mikan; texlive = our-texlive; }; } diff --git a/shell.nix b/shell.nix index c7127f62e..2cfc9e9bc 100644 --- a/shell.nix +++ b/shell.nix @@ -11,10 +11,10 @@ the1lab.overrideAttrs (old: { nativeBuildInputs = old.nativeBuildInputs or [] ++ [ (with pkgs.labHaskellPackages; pkgs.symlinkJoin { - name = "agda-nodebug"; - paths = [ Agda sort-imports ]; + name = "mikan"; + paths = [ Mikan sort-imports ]; postBuild = '' - ln -sf ${Agda.nodebug}/bin/agda $out/bin/agda-nodebug + ln -sf ${Mikan.nodebug}/bin/mikan $out/bin/mikan-nodebug ''; }) ]; diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md index c6f756ad6..c5040e8a6 100644 --- a/src/1Lab/Equiv.lagda.md +++ b/src/1Lab/Equiv.lagda.md @@ -118,9 +118,7 @@ inverse is again an isomorphism. ```agda inverse : is-iso from - inverse .from = f - inverse .rinv = linv - inverse .linv = rinv + inverse = record { from = f ; rinv = linv ; linv = rinv } ``` + +## Built-in type formers -Additionally, we define the empty type: +The `Type`{.Agda} universes are closed under `Σ`{.Agda}, and the lowest +universe contains both the [[natural numbers]] `Nat`{.Agda} and the +[[booleans]] `Bool`{.Agda}. + -¬_ : ∀ {ℓ} → Type ℓ → Type ℓ -¬ A = A → ⊥ -infix 6 ¬_ +```agda +_ : ∀ {ℓ ℓ'} (A : Type ℓ) → (A → Type ℓ') → Type (ℓ ⊔ ℓ') +_ = Σ ``` :::{.definition #product-type} -The non-dependent product type `_×_`{.Agda} can be defined in terms of -the dependent sum type: +The non-dependent **product type** `_×_`{.Agda} can be defined in terms +of the dependent sum type, `Σ`{.Agda}. ::: ```agda @@ -64,59 +109,158 @@ A × B = Σ[ _ ∈ A ] B infixr 5 _×_ ``` -## Lifting +# Auxilliary universes -There is a function which lifts a type to a higher universe: +Our type theory has a couple more families of universes that serve to +support the formalisation. Above, we wrote down a function type where +the *universe* at which the codomain lives depends on the input value. +These "large" products are classified in `Typeω`. These "limit" +universes are themselves organised into a hierarchy, but, unlike +`Type`{.Agda}, the indexing of this hierarchy is *external*: the +subscript in `Typeω₁`{.Agda} is a literal number, and not shorthand for +a value of some type. ```agda -record Lift {a} ℓ (A : Type a) : Type (a ⊔ ℓ) where - constructor lift - field - lower : A +_ : Typeω +_ = (ℓ : Level) → Type (lsuc ℓ) + +_ : Typeω₁ +_ = Typeω ``` - -## Function composition +The empty `Type`{.Agda}, `⊥`{.Agda}, is defined by lifting the empty +`SProp`{.Agda}. Since `⊥`{.Agda} is an `eta-equality record`{.Agda} +type, it "inherits" definitional irrelevance from `⊥ˢ`{.Agda}. + +```agda +record ⊥ : Type where + constructor liftˢ + field lowerˢ : ⊥ˢ +``` -Since the following definitions are fundamental, they deserve a place in -this module: +Even defined like this, the empty type has an elimination principle into +arbitrary types. We define an eliminator `absurd`{.Agda} valued in small +fibrant types. To demonstrate that the codomain can be arbitrary, we can +also define `absurdω`{.Agda}. ```agda -_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : (x : A) → B x → Type ℓ₃} - → (∀ {x} → (y : B x) → C x y) - → (f : ∀ x → B x) - → ∀ x → C x (f x) -f ∘ g = λ z → f (g z) +absurd : ∀ {ℓ} {A : Type ℓ} → ⊥ → A +absurd () + +absurdω : {A : Typeω} → ⊥ → A +absurdω () +``` + +The **negation** of a type $A$ is, as usual, the type of functions $A +\to \bot$. With our setup, the negation of an arbitrary type is +definitionally proof-irrelevant. + +```agda +¬_ : ∀ {ℓ} → Type ℓ → Type ℓ +¬ A = A → ⊥ +infix 6 ¬_ +``` + + -infixr 40 _∘_ + +# Basic syntactic niceties + +We close out this module with the definition of a couple helpers which +do not depend on anything other than quantification over types. First, +we have (dependent) function composition `_∘_`{.Agda}, and the identity +function `id`{.Agda}. + +```agda +_∘_ + : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : (x : A) → B x → Type ℓ₃} + → (f : ∀ {x} → (y : B x) → C x y) (g : ∀ x → B x) + → ∀ x → C x (g x) +(f ∘ g) z = f (g z) id : ∀ {ℓ} {A : Type ℓ} → A → A id x = x -{-# INLINE id #-} +``` + +We also define two helpers for function application. The first, +`_$_`{.Agda}, is familiar from Haskell, and serves simply to adjust +precedence: one can write `f $ g x` instead of `f (g x)`. -infixr -1 _$_ _$ᵢ_ _$ₛ_ +```agda +infixr -1 _$_ -_$_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂} → ((x : A) → B x) → ((x : A) → B x) +_$_ : ∀ {a b} {A : Type a} {B : A → Type b} → ((x : A) → B x) → ((x : A) → B x) f $ x = f x +``` + +The second, `case_of_`{.Agda}, is a mixfix operator which constraints +its function argument to be nondependent, which enables type inference. +When given a pattern-matching lambda as its second argument, +`case_of_`{.Agda} can be used to scrutinise a value in an expression +context. + +```agda +case_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A → (A → B) → B +case x of f = f x + +_ : Bool → Bool +_ = λ x → case x of λ where + true → false + false → true +``` + +Finally, the 1Lab makes extensive use of instance arguments for +automation. A convenient entry point to this automation is the +`auto`{.Agda} function, which can be used to call instance search where +a visible argument is expected. + +```agda +auto : ∀ {ℓ} {A : Type ℓ} → ⦃ A ⦄ → A +auto ⦃ a ⦄ = a +``` + + diff --git a/src/Algebra/Ring/Module/Multilinear.lagda.md b/src/Algebra/Ring/Module/Multilinear.lagda.md index b6224938d..16f1888b1 100644 --- a/src/Algebra/Ring/Module/Multilinear.lagda.md +++ b/src/Algebra/Ring/Module/Multilinear.lagda.md @@ -1,6 +1,5 @@ diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md index 1440d0c80..d2598b91b 100644 --- a/src/Cat/Displayed/Instances/Subobjects.lagda.md +++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md @@ -359,7 +359,7 @@ _≤ₘ_ = ≤-over id open Sub renaming (_≅_ to infix 7 _≅ₘ_) - using () + using (to ; from ; inverses) public infix 7 _≤ₘ_ diff --git a/src/Cat/Displayed/Solver.agda b/src/Cat/Displayed/Solver.agda index d9094fc27..f5e886773 100644 --- a/src/Cat/Displayed/Solver.agda +++ b/src/Cat/Displayed/Solver.agda @@ -138,10 +138,10 @@ module Reflection where module Cat = Cat.Solver.Reflection pattern displayed-field-args xs = - _ hm∷ _ hm∷ -- Base Levels - _ hm∷ -- Base Category - _ hm∷ _ hm∷ -- Displayed Levels - _ v∷ xs -- Displayed Category + _ h∷ _ h∷ -- Base Levels + _ h∷ -- Base Category + _ h∷ _ h∷ -- Displayed Levels + _ v∷ xs -- Displayed Category pattern displayed-fn-args xs = _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ v∷ xs diff --git a/src/Cat/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md index dc0c67976..0500baa79 100644 --- a/src/Cat/Displayed/Univalence/Thin.lagda.md +++ b/src/Cat/Displayed/Univalence/Thin.lagda.md @@ -1,6 +1,5 @@ + By construction, this is a [[univalent|univalent category]] [[groupoid|pregroupoid]]: ```agda Disc-is-category : ∀ {A : Type ℓ} {A-grpd} → is-category (Disc A A-grpd) -Disc-is-category .to-path is = is .to -Disc-is-category .to-path-over is = ≅-pathp _ _ _ λ i j → is .to (i ∧ j) +Disc-is-category .to-path is = Id≃path.to (is .to) +Disc-is-category .to-path-over {a = a} is with is .to in w +... | reflᵢ = ≅-pathp _ _ _ (Id≃path.to (symᵢ w)) Disc-is-groupoid : ∀ {A : Type ℓ} {A-grpd} → is-pregroupoid (Disc A A-grpd) -Disc-is-groupoid p = make-invertible _ (sym p) (∙-invl p) (∙-invr p) -``` - -We can lift any function between the underlying types to a functor -between discrete categories. This is because every function -automatically respects equality in a functorial way. - -```agda -lift-disc - : ∀ {A : Set ℓ} {B : Set ℓ'} - → (∣ A ∣ → ∣ B ∣) - → Functor (Disc' A) (Disc' B) -lift-disc f .F₀ = f -lift-disc f .F₁ = ap f -lift-disc f .F-id = refl -lift-disc f .F-∘ p q = ap-∙ f q p +Disc-is-groupoid p = make-invertible _ (symᵢ p) (∙ᵢ-invl p) (∙ᵢ-invr p) ``` + : ∀ {ℓ} {X : Type ℓ} {xh} ⦃ _ : H-Level X 2 ⦄ + → (F : C .Ob → ⌞ X ⌟) + → (F₁ : ∀ {x y} → C .Hom x y → F x ≡ᵢ F y) + → Functor C (Disc X xh) +Disc-into F F₁ .F₀ = F +Disc-into F F₁ .F₁ = F₁ +Disc-into F F₁ .F-id = hlevel! +Disc-into F F₁ .F-∘ _ _ = hlevel! - diff --git a/src/Cat/Instances/Presheaf/Omega.lagda.md b/src/Cat/Instances/Presheaf/Omega.lagda.md index 6885ed849..19dadf73c 100644 --- a/src/Cat/Instances/Presheaf/Omega.lagda.md +++ b/src/Cat/Instances/Presheaf/Omega.lagda.md @@ -86,9 +86,9 @@ psh-name {P} so .is-natural x y f = ext λ x {V} f → Ω-ua PSh-omega : Subobject-classifier (PSh ℓ C) PSh-omega .Subobject-classifier.Ω = Sieves -PSh-omega .Subobject-classifier.true .Sub.dom = _ -PSh-omega .Subobject-classifier.true .Sub.map = tru -PSh-omega .Subobject-classifier.true .Sub.monic _ _ _ = ext λ _ _ → refl +PSh-omega .Subobject-classifier.true .dom = _ +PSh-omega .Subobject-classifier.true .map = tru +PSh-omega .Subobject-classifier.true .monic _ _ _ = ext λ _ _ → refl PSh-omega .generic .name = psh-name ``` --> diff --git a/src/Cat/Instances/Shape/Two.lagda.md b/src/Cat/Instances/Shape/Two.lagda.md index 40e8426d7..f56cfb2ea 100644 --- a/src/Cat/Instances/Shape/Two.lagda.md +++ b/src/Cat/Instances/Shape/Two.lagda.md @@ -22,7 +22,7 @@ useful for expressing binary [[products]] and [[coproducts]] as ```agda 2-object-category : Precategory _ _ -2-object-category = Disc' (el! Bool) +2-object-category = Disc! Bool ``` A diagram of shape $\twocat$ in $\cC$ simply consists of two objects of @@ -62,17 +62,7 @@ defined above. p false = refl p true = refl - q : ∀ {x y} (f : x ≡ y) → _ - q {false} {false} p = - F .F₁ p ≡⟨ ap (F .F₁) prop! ⟩ - F .F₁ refl ≡⟨ F .F-id ⟩ - id ≡˘⟨ transport-refl id ⟩ - transport refl id ∎ - q {true} {true} p = - F .F₁ p ≡⟨ ap (F .F₁) prop! ⟩ - F .F₁ refl ≡⟨ F .F-id ⟩ - id ≡˘⟨ transport-refl id ⟩ - transport refl id ∎ - q {false} {true} p = absurd (true≠false (sym p)) - q {true} {false} p = absurd (true≠false p) + q : ∀ {x y} (f : x ≡ᵢ y) → _ + q {true} reflᵢ = F .F-id + q {false} reflᵢ = F .F-id ``` diff --git a/src/Cat/Instances/Slice.lagda.md b/src/Cat/Instances/Slice.lagda.md index 793f4262a..5d134fab0 100644 --- a/src/Cat/Instances/Slice.lagda.md +++ b/src/Cat/Instances/Slice.lagda.md @@ -604,7 +604,7 @@ Let's begin. The `Total-space`{.Agda} functor gets out of our way very fast: ```agda - Total-space : Functor Cat[ Disc' I , Sets ℓ ] (Slice (Sets ℓ) I) + Total-space : Functor Cat[ Disc! I , Sets ℓ ] (Slice (Sets ℓ) I) Total-space .F₀ F .dom = el! (Σ _ (∣_∣ ⊙ F₀ F)) Total-space .F₀ F .map = fst @@ -640,10 +640,10 @@ dependent function is automatically a natural transformation. nt : F => G nt .η = eta - nt .is-natural _ _ = J (λ _ p → eta _ ⊙ F .F₁ p ≡ G .F₁ p ⊙ eta _) $ - eta _ ⊙ F .F₁ refl ≡⟨ ap (eta _ ⊙_) (F .F-id) ⟩ - eta _ ≡˘⟨ ap (_⊙ eta _) (G .F-id) ⟩ - G .F₁ refl ⊙ eta _ ∎ + nt .is-natural _ _ reflᵢ = + eta _ ⊙ F .F₁ reflᵢ ≡⟨ ap (eta _ ⊙_) (F .F-id) ⟩ + eta _ ≡˘⟨ ap (_⊙ eta _) (G .F-id) ⟩ + G .F₁ reflᵢ ⊙ eta _ ∎ ``` - Fortunately the triangle identities are straightforwardly checked. ```agda - adj .zig {x} = Functor-path (λ x i → x) λ f → x .is-tr _ _ _ _ + adj .zig {x} = Functor-path (λ x i → x) λ f → prop! adj .zag = refl ``` @@ -185,10 +163,10 @@ both directions: Γ⊣Codisc : Γ ⊣ Codisc {ℓ} Γ⊣Codisc = adj where adj : _ ⊣ _ - adj .unit = - NT (λ x → record { F₀ = λ x → x ; F₁ = λ _ → lift tt - ; F-id = refl ; F-∘ = λ _ _ → refl }) - λ x y f → Functor-path (λ _ → refl) λ _ → refl + adj .unit = record where + η x = record + { F₀ = λ x → x ; F₁ = λ _ → lift tt ; F-id = refl ; F-∘ = λ _ _ → refl } + is-natural x y f = Functor-path (λ _ → refl) λ _ → refl adj .counit = NT (λ _ x → x) λ x y f i o → f o adj .zig = refl adj .zag = Functor-path (λ _ → refl) λ _ → refl @@ -311,8 +289,8 @@ quotient. Π₀⊣Disc : Π₀ ⊣ Disc {ℓ} Π₀⊣Disc = adj where adj : _ ⊣ _ - adj .unit .η x = Disc-into _ inc quot - adj .unit .is-natural x y f = Functor-path (λ x → refl) λ _ → squash _ _ _ _ + adj .unit .η x = Disc-into inc λ m → Id≃path.from (quot m) + adj .unit .is-natural x y f = Functor-path (λ x → refl) λ _ → prop! ``` The adjunction `counit`{.Agda} is an assignment of functions @@ -321,7 +299,7 @@ isomorphism: the set of connected components of a discrete category is the same set we started with. ```agda - adj .counit .η X = Quot-elim (λ _ → X .is-tr) (λ x → x) λ x y r → r + adj .counit .η X = Quot-elim (λ _ → X .is-tr) (λ x → x) λ x y r → Id≃path.to r adj .counit .is-natural x y f = ext λ _ → refl ``` @@ -329,7 +307,7 @@ The triangle identities are again straightforwardly checked. ```agda adj .zig {x} = ext λ _ → refl - adj .zag = Functor-path (λ x → refl) λ f → refl + adj .zag = Functor-path (λ x → refl) λ f → prop! ``` Furthermore, we can prove that the connected components of a product diff --git a/src/Cat/Internal/Functor/Outer.lagda.md b/src/Cat/Internal/Functor/Outer.lagda.md index 119c3f174..66db171c0 100644 --- a/src/Cat/Internal/Functor/Outer.lagda.md +++ b/src/Cat/Internal/Functor/Outer.lagda.md @@ -240,17 +240,17 @@ covariant construction, performed above. src-coh = sym (ap (src ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom g) .has-src) - outf .P-id fₓ = - sym $ unique (sym (ap ihom (idri _))) (sym (!-unique _)) - outf .P-∘ fₓ g h = - unique - (p₁∘universal - ∙ ap ihom (associ _ _ _) - ∙ ∘i-ihom refl - (sym (ap (src ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-src)) - (sym (ap (tgt ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-tgt)) - (sym p₁∘universal) refl) - p₂∘universal + outf .P-id fₓ = sym $ unique + (sym (ap ihom (ap₂ _∘i_ refl op-ihom-involutive ∙ idri _))) + (sym (!-unique _)) + outf .P-∘ fₓ g h = unique + (p₁∘universal + ∙ ap ihom (ap₂ _∘i_ refl op-ihom-involutive ∙ associ _ _ _) + ∙ ∘i-ihom refl + (sym (ap (src ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-src)) + (sym (ap (tgt ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-tgt)) + (sym p₁∘universal) refl) + p₂∘universal outf .P₀-nat fₓ σ = sym (assoc _ _ _) ∙ ap (src ∘_) (sym (assoc _ _ _)) diff --git a/src/Cat/Internal/Opposite.lagda.md b/src/Cat/Internal/Opposite.lagda.md index 2571ba8fb..b051ac42c 100644 --- a/src/Cat/Internal/Opposite.lagda.md +++ b/src/Cat/Internal/Opposite.lagda.md @@ -45,13 +45,11 @@ op-ihom-nat f _ = Internal-hom-path refl @@ -69,9 +67,17 @@ Internal-cat-on-opi ℂ = icat-opi-on where icat-opi-on : Internal-cat-on _ _ icat-opi-on .idi x = op-ihom (ℂ.idi x) icat-opi-on ._∘i_ f g = op-ihom (op-ihom g ℂ.∘i op-ihom f) - icat-opi-on .idli f = ap op-ihom (ℂ.idri _) - icat-opi-on .idri f = ap op-ihom (ℂ.idli _) - icat-opi-on .associ f g h = ap op-ihom (sym (ℂ.associ _ _ _)) + icat-opi-on .idli f = + op-ihom (op-ihom f ℂ.∘i ⌜ op-ihom (op-ihom (ℂ.idi _)) ⌝) ≡⟨ ap! op-ihom-involutive ⟩ + op-ihom ⌜ op-ihom f ℂ.∘i ℂ.idi _ ⌝ ≡⟨ ap! (ℂ.idri (op-ihom f)) ⟩ + op-ihom (op-ihom f) ≡⟨ op-ihom-involutive ⟩ + f ∎ + icat-opi-on .idri f = ap op-ihom (ap₂ ℂ._∘i_ op-ihom-involutive refl ∙ ℂ.idli _) ∙ op-ihom-involutive + icat-opi-on .associ f g h = + op-ihom (⌜ op-ihom (op-ihom (op-ihom h ℂ.∘i op-ihom g)) ⌝ ℂ.∘i op-ihom f) ≡⟨ ap! op-ihom-involutive ⟩ + op-ihom ⌜ (op-ihom h ℂ.∘i op-ihom g) ℂ.∘i op-ihom f ⌝ ≡⟨ ap! (sym (ℂ.associ _ _ _)) ⟩ + op-ihom ⌜ op-ihom h ℂ.∘i op-ihom g ℂ.∘i op-ihom f ⌝ ≡⟨ ap¡ (sym op-ihom-involutive) ⟩ + op-ihom (op-ihom h ℂ.∘i ⌜ op-ihom (op-ihom (op-ihom g ℂ.∘i op-ihom f)) ⌝) ∎ icat-opi-on .idi-nat σ = op-ihom-nat (ℂ.idi _) σ ∙ ap op-ihom (ℂ.idi-nat σ) icat-opi-on .∘i-nat f g σ = diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md index 27558f84d..6651976c3 100644 --- a/src/Cat/Morphism.lagda.md +++ b/src/Cat/Morphism.lagda.md @@ -503,9 +503,7 @@ record is-invertible (f : Hom a b) : Type h where open Inverses inverses public op : is-invertible inv - op .inv = f - op .inverses .Inverses.invl = invr inverses - op .inverses .Inverses.invr = invl inverses + op = record { inv = f ; inverses = record { invl = invr inverses ; invr = invl inverses }} record _≅_ (a b : Ob) : Type h where field diff --git a/src/Cat/Solver.lagda.md b/src/Cat/Solver.lagda.md index 144e5df55..1978b2de2 100644 --- a/src/Cat/Solver.lagda.md +++ b/src/Cat/Solver.lagda.md @@ -129,7 +129,7 @@ hom-sets, then they represent the same morphism. module Reflection where pattern category-args xs = - _ hm∷ _ hm∷ _ v∷ xs + _ h∷ _ h∷ _ v∷ xs pattern “id” = def (quote Precategory.id) (category-args (_ h∷ [])) diff --git a/src/Cat/Univalent/Rezk/Universal.lagda.md b/src/Cat/Univalent/Rezk/Universal.lagda.md index 23df623ab..ab7c09ddd 100644 --- a/src/Cat/Univalent/Rezk/Universal.lagda.md +++ b/src/Cat/Univalent/Rezk/Universal.lagda.md @@ -1,6 +1,5 @@ @@ -612,6 +620,9 @@ instance Finite-PathP : ∀ {A : I → Type ℓ} ⦃ s : Finite (A i1) ⦄ {x y} → Finite (PathP A x y) + Finite-≡ᵢ + : ∀ {A : Type ℓ} ⦃ s : Finite A ⦄ {x y : A} + → Finite (x ≡ᵢ y) Finite-∥-∥ : ⦃ _ : Dec A ⦄ → Finite ∥ A ∥ ``` @@ -651,6 +662,10 @@ instance a ← fa pure (Listing-PathP ⦃ a ⦄) + Finite-≡ᵢ ⦃ fa ⦄ = do + a ← fa + pure (Listing-≡ᵢ ⦃ a ⦄) + Finite-Lift ⦃ fa ⦄ = do a ← fa pure (Listing-Lift ⦃ a ⦄) diff --git a/src/Data/Fin/Product.lagda.md b/src/Data/Fin/Product.lagda.md index f833e59f9..3d90cc1aa 100644 --- a/src/Data/Fin/Product.lagda.md +++ b/src/Data/Fin/Product.lagda.md @@ -20,7 +20,7 @@ with strictly curried (non-dependent) functions whose domain is a finite product. The construction is maximally universe-polymorphic, in that it supports sequences whose universe level varies between components, and is valued in their finite supremum, giving universes for products more -precise than `Setω`{.Agda}. +precise than `Typeω`{.Agda}. @@ -22,25 +25,47 @@ private variable ``` --> -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. +As with how the [[propositional truncation]] freely generates a +[[proposition]] from a type, we can define a *strict* truncation +modality which freely generates a *definitionally irrelevant* type from +a type. + +This is a secondary notion in our type theory, since this type former +does not have a well-behaved elimination principle. However, its +presence in the theory allows defining `record`{.Agda} types with finer +control over definitional equality, which can be a notable optimisation; +and the resulting types are essentially well-behaved as long as we only +wrap [[decidable]] [[propositions]]. + +The construction proceeds in two stages: first, we define `Irrˢ`{.Agda}, +living in `SProp`{.Agda}, generated by $A$. This type is then wrapped in +the `record`{.Agda} `Irr`{.Agda} to bring it back to the correct +universe of [[fibrant]] types. ```agda +data Irrˢ {ℓ} (A : Type ℓ) : SProp ℓ where + forgetˢ : A → Irrˢ A + record Irr {ℓ} (A : Type ℓ) : Type ℓ where - constructor forget - field - @irr lower : A + constructor liftˢ + field lowerˢ : Irrˢ 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$. +As promised, `Irr`{.Agda} is definitionally irrelevant, as can be +demonstrated by checking that the `refl`{.Agda}exive path connects the +*a priori* distinct variables $x$ and $y$. ```agda instance H-Level-Irr : ∀ {n} → H-Level (Irr A) (suc n) - H-Level-Irr {n} = prop-instance λ _ _ → refl + H-Level-Irr {n} = prop-instance λ x y → refl ``` + +## Recovering decidable propositions + +As mentioned above, `Irr`{.Agda} does not have a well-behaved +elimination principle. However, since `⊥`{.Agda} is a strict +proposition, we can show that $\operatorname{Irr}(A)$ implies $\neg \neg +A$. + +```agda +Irr→not-not : ∀ {ℓ} {A : Type ℓ} → Irr A → ¬ ¬ A +Irr→not-not {A = A} (liftˢ aˢ) f = liftˢ (go aˢ f) where + go : Irrˢ A → (A → ⊥) → ⊥ˢ + go (forgetˢ a) ¬a = ¬a a .⊥.lowerˢ +``` + +Therefore, if the type being truncated is [[decidable]], we can recover +a legitimate $A$ given only knowledge of $\operatorname{Irr}(A)$, using +the result above to refute the `no`{.Agda} case. + +```agda +recover : ∀ {ℓ} {A : Type ℓ} ⦃ d : Dec A ⦄ → Irr A → A +recover ⦃ yes x ⦄ _ = x +recover ⦃ no ¬x ⦄ ¬¬x = absurd (Irr→not-not ¬¬x ¬x) +``` diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md index 37ab91c71..824d8bab2 100644 --- a/src/Data/Nat/Base.lagda.md +++ b/src/Data/Nat/Base.lagda.md @@ -115,8 +115,6 @@ abstract from-prim-eq-refl {zero} = refl from-prim-eq-refl {suc x} = ap (ap suc) (from-prim-eq-refl {x}) - {-# REWRITE from-prim-eq-refl #-} - to-prim-eq : ∀ {x y} → x ≡ y → So (x == y) to-prim-eq {zero} {zero} p = oh to-prim-eq {zero} {suc y} p = absurd (zero≠suc p) diff --git a/src/Data/Nat/DivMod.lagda.md b/src/Data/Nat/DivMod.lagda.md index 9b607f82b..3837ab6d6 100644 --- a/src/Data/Nat/DivMod.lagda.md +++ b/src/Data/Nat/DivMod.lagda.md @@ -80,8 +80,9 @@ $$ $$ ```agda - divide-pos (suc a) b | divmod q' r' (forget p) s | inl r'+1 @@ -255,4 +249,5 @@ instance n∣r : (q' - q) * n ≡ r n∣r = monus-distribr q' q n ∙ sym (monus-swapl _ _ _ (sym (p ∙ recover α))) in <-≤-asym β (m∣sn→m≤sn (q' - q , n∣r)) + {-# INCOHERENT Dec-∣ #-} ``` diff --git a/src/Data/Nat/Divisible/GCD.lagda.md b/src/Data/Nat/Divisible/GCD.lagda.md index 2d4aa7ab2..7cccf9e89 100644 --- a/src/Data/Nat/Divisible/GCD.lagda.md +++ b/src/Data/Nat/Divisible/GCD.lagda.md @@ -11,6 +11,7 @@ open import Data.Nat.Order open import Data.Dec.Base open import Data.Nat.Base open import Data.Sum.Base +open import Data.Irr ``` --> @@ -165,10 +166,10 @@ sense of $<$) than the original input. ```agda euclid-< : ∀ y x → x < y → GCD y x euclid-< = Wf-induction _ <-wf _ λ where - x rec zero p → x , is-gcd-0 - x rec (suc y) p → + x rec zero p → x , is-gcd-0 + x rec (suc y) p → let (d , step) = rec (suc y) p (x % suc y) (x%y diff --git a/src/Data/Nat/Range.lagda.md b/src/Data/Nat/Range.lagda.md index 9b12fada9..5a3e92527 100644 --- a/src/Data/Nat/Range.lagda.md +++ b/src/Data/Nat/Range.lagda.md @@ -217,7 +217,7 @@ range-upper → i ∈ range x y → i < y range-upper {x = x} {y = y} {i = i} i∈xy = - ≤-trans (count-up-upper i∈xy) $ ≤-refl' $ᵢ + ≤-trans (count-up-upper i∈xy) $ ≤-refl' $ monus-+r-inverse y x $ <-weaken (nonempty-range→< (has-member→nonempty i∈xy)) ``` @@ -240,7 +240,7 @@ range-∈ → x ≤ i → i < y → i ∈ range x y range-∈ {x = x} {y = y} {i = i} x≤i i