From 9321ce68647574e1108099ce1402e3b36623579d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia?= Date: Wed, 3 Apr 2024 09:03:07 -0300 Subject: [PATCH] chore: bump agda (#371) Still need to merge my WIP branch that kills `Extensionality` and the bulk of the hlevel tactic, but I want to get a CI run. --- .github/workflows/build.yml | 4 +- src/1Lab/Classical.lagda.md | 14 +- src/1Lab/Equiv/HalfAdjoint.lagda.md | 1 - src/1Lab/Extensionality.agda | 465 +++++---- src/1Lab/Function/Surjection.lagda.md | 8 +- src/1Lab/HIT/Truncation.lagda.md | 45 +- src/1Lab/HLevel/Closure.lagda.md | 5 + src/1Lab/HLevel/Universe.lagda.md | 9 - src/1Lab/Reflection/Deriving/Show.agda | 4 +- src/1Lab/Reflection/HLevel.agda | 937 +++++------------- src/1Lab/Reflection/Signature.agda | 12 +- src/1Lab/Resizing.lagda.md | 55 +- src/Algebra/Group.lagda.md | 4 +- src/Algebra/Group/Ab/Abelianisation.lagda.md | 2 +- src/Algebra/Group/Ab/Tensor.lagda.md | 22 +- src/Algebra/Group/Action.lagda.md | 2 +- .../Group/Cat/FinitelyComplete.lagda.md | 2 +- src/Algebra/Group/Concrete.lagda.md | 2 +- src/Algebra/Group/Free.lagda.md | 2 +- src/Algebra/Group/Homotopy/BAut.lagda.md | 2 +- src/Algebra/Group/Notation.agda | 2 + src/Algebra/Group/Subgroup.lagda.md | 24 +- src/Algebra/Monoid.lagda.md | 2 +- src/Algebra/Ring.lagda.md | 2 - src/Algebra/Ring/Module.lagda.md | 24 +- src/Algebra/Ring/Module/Action.lagda.md | 10 +- src/Algebra/Ring/Module/Free.lagda.md | 35 +- src/Cat/Allegory/Base.lagda.md | 4 +- src/Cat/Allegory/Instances/Mat.lagda.md | 4 +- src/Cat/Allegory/Reasoning.lagda.md | 2 +- src/Cat/Base.lagda.md | 88 +- src/Cat/Bi/Diagram/Monad/Spans.lagda.md | 3 +- src/Cat/Bi/Instances/Relations.lagda.md | 6 +- src/Cat/Bi/Instances/Spans.lagda.md | 4 +- src/Cat/CartesianClosed/Instances/PSh.agda | 4 +- src/Cat/Connected.lagda.md | 6 +- src/Cat/Diagram/Colimit/Cocone.lagda.md | 2 +- src/Cat/Diagram/Initial.lagda.md | 2 +- src/Cat/Diagram/Limit/Cone.lagda.md | 2 +- src/Cat/Diagram/Monad.lagda.md | 23 +- src/Cat/Diagram/Monad/Relative.lagda.md | 11 +- src/Cat/Displayed/Base.lagda.md | 29 + src/Cat/Displayed/Cartesian/Discrete.lagda.md | 3 +- src/Cat/Displayed/Cartesian/Street.lagda.md | 11 +- src/Cat/Displayed/Doctrine/Frame.lagda.md | 32 +- src/Cat/Displayed/GenericObject.lagda.md | 12 +- src/Cat/Displayed/Instances/Elements.lagda.md | 2 +- src/Cat/Displayed/Instances/Family.lagda.md | 2 +- src/Cat/Displayed/Instances/Identity.lagda.md | 6 +- src/Cat/Displayed/Instances/Lifting.lagda.md | 22 +- src/Cat/Displayed/Instances/Opposite.lagda.md | 2 +- src/Cat/Displayed/Instances/Slice.lagda.md | 7 +- .../Displayed/Instances/Subobjects.lagda.md | 29 +- .../Displayed/Instances/TotalProduct.lagda.md | 4 +- src/Cat/Displayed/Solver.agda | 2 - src/Cat/Displayed/Total.lagda.md | 8 +- src/Cat/Displayed/Univalence.lagda.md | 1 - src/Cat/Displayed/Univalence/Thin.lagda.md | 34 +- src/Cat/Functor/Adjoint.lagda.md | 1 - src/Cat/Functor/Base.lagda.md | 10 +- src/Cat/Functor/Equivalence.lagda.md | 10 +- src/Cat/Functor/Equivalence/Path.lagda.md | 9 +- src/Cat/Functor/Hom/Representable.lagda.md | 1 - src/Cat/Functor/Kan/Nerve.lagda.md | 1 - src/Cat/Functor/Morphism.lagda.md | 4 +- src/Cat/Functor/Naturality.lagda.md | 1 - src/Cat/Functor/Subcategory.lagda.md | 13 +- src/Cat/Functor/WideSubcategory.lagda.md | 32 +- src/Cat/Gaunt.lagda.md | 16 +- src/Cat/Instances/Comma.lagda.md | 6 +- src/Cat/Instances/Elements.lagda.md | 31 +- src/Cat/Instances/Elements/Covariant.lagda.md | 28 +- src/Cat/Instances/Free.lagda.md | 2 +- src/Cat/Instances/InternalFunctor.lagda.md | 2 +- src/Cat/Instances/Karoubi.lagda.md | 1 - src/Cat/Instances/Lift.lagda.md | 1 - src/Cat/Instances/Localisation.lagda.md | 20 +- src/Cat/Instances/OFE.lagda.md | 50 +- src/Cat/Instances/OFE/Closed.lagda.md | 1 - src/Cat/Instances/OFE/Complete.lagda.md | 3 +- src/Cat/Instances/OFE/Coproduct.lagda.md | 6 +- src/Cat/Instances/OFE/Product.lagda.md | 7 +- src/Cat/Instances/OuterFunctor.lagda.md | 2 +- src/Cat/Instances/Poly.lagda.md | 3 +- src/Cat/Instances/Product.lagda.md | 2 +- src/Cat/Instances/Sets/Cocomplete.lagda.md | 2 +- src/Cat/Instances/Sets/Complete.lagda.md | 4 +- .../Sets/Counterexamples/SelfDual.lagda.md | 17 +- src/Cat/Instances/Shape/Involution.lagda.md | 2 +- src/Cat/Instances/Shape/Isomorphism.lagda.md | 4 +- src/Cat/Instances/Shape/Join.lagda.md | 4 +- src/Cat/Instances/Simplex.lagda.md | 7 +- src/Cat/Instances/Slice.lagda.md | 25 +- src/Cat/Instances/Slice/Presheaf.lagda.md | 2 +- src/Cat/Instances/StrictCat.lagda.md | 10 +- src/Cat/Instances/StrictCat/Cohesive.lagda.md | 2 +- src/Cat/Instances/Twisted.lagda.md | 6 +- src/Cat/Internal/Base.lagda.md | 20 +- src/Cat/Internal/Functor/Outer.lagda.md | 12 +- src/Cat/Monoidal/Diagram/Monoid.lagda.md | 16 +- .../Diagram/Monoid/Representable.lagda.md | 1 - src/Cat/Monoidal/Instances/Day.lagda.md | 45 +- src/Cat/Morphism.lagda.md | 71 +- src/Cat/Morphism/Extensionality.agda | 23 - src/Cat/Morphism/Factorisation.lagda.md | 2 +- src/Cat/Morphism/Instances.agda | 32 + src/Cat/Morphism/StrongEpi.lagda.md | 2 +- src/Cat/Prelude.agda | 2 +- src/Cat/Regular/Image.lagda.md | 4 +- src/Cat/Restriction/Reasoning.lagda.md | 11 +- src/Cat/Univalent.lagda.md | 5 +- src/Cat/Univalent/Rezk.lagda.md | 2 +- src/Cat/Univalent/Rezk/Universal.lagda.md | 38 +- src/Data/Dec/Path.lagda.md | 3 - src/Data/Fin/Finite.lagda.md | 14 +- src/Data/Fin/Finite/Listed.lagda.md | 4 +- src/Data/Fin/Indexed.lagda.md | 2 +- src/Data/Id/Base.lagda.md | 37 +- src/Data/Image.lagda.md | 1 - src/Data/List/Properties.lagda.md | 10 +- src/Data/Maybe/Properties.lagda.md | 9 +- src/Data/Nat/Base.lagda.md | 10 + src/Data/Nat/Divisible.lagda.md | 1 + src/Data/Partial/Base.lagda.md | 30 +- src/Data/Partial/Properties.lagda.md | 3 - src/Data/Power.lagda.md | 10 - src/Data/Power/Complemented.lagda.md | 4 +- src/Data/Set/Coequaliser.lagda.md | 39 +- src/Data/Set/Material.lagda.md | 22 +- src/Data/Set/Surjection.lagda.md | 14 +- src/Data/Set/Truncation.lagda.md | 1 + src/Data/Sum/Properties.lagda.md | 9 +- src/HoTT.lagda.md | 7 +- src/Homotopy/Connectedness.lagda.md | 14 +- src/Homotopy/Space/Delooping.lagda.md | 11 +- .../Space/Suspension/Properties.lagda.md | 10 +- src/Homotopy/Truncation.lagda.md | 31 +- .../Classical/Compactness.lagda.md | 6 +- src/Order/Base.lagda.md | 43 +- src/Order/DCPO.lagda.md | 16 +- src/Order/DCPO/Free.lagda.md | 38 +- src/Order/Diagram/Bottom.lagda.md | 2 +- src/Order/Diagram/Glb.lagda.md | 19 +- src/Order/Diagram/Join.lagda.md | 10 +- src/Order/Diagram/Lub.lagda.md | 23 +- src/Order/Diagram/Meet.lagda.md | 10 +- src/Order/Diagram/Top.lagda.md | 2 +- src/Order/Frame.lagda.md | 19 +- src/Order/Frame/Free.lagda.md | 2 +- src/Order/Frame/Reasoning.lagda.md | 2 +- src/Order/Instances/Coproduct.lagda.md | 4 +- src/Order/Instances/Discrete.lagda.md | 2 +- src/Order/Instances/Disjoint.lagda.md | 4 +- src/Order/Instances/Int.lagda.md | 2 +- src/Order/Instances/Pointwise.lagda.md | 4 +- src/Order/Instances/Product.lagda.md | 2 +- src/Order/Instances/Props.lagda.md | 2 +- src/Order/Lattice.lagda.md | 23 +- src/Order/Semilattice/Join.lagda.md | 16 +- src/Order/Semilattice/Meet.lagda.md | 17 +- src/Order/Univalent.lagda.md | 4 +- support/nix/dep/Agda/github.json | 4 +- support/shake/app/HTML/Backend.hs | 2 +- 163 files changed, 1175 insertions(+), 2096 deletions(-) delete mode 100644 src/Cat/Morphism/Extensionality.agda create mode 100644 src/Cat/Morphism/Instances.agda diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index d37e9ce8e..c6b43640c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -48,8 +48,8 @@ jobs: uses: actions/cache@v4 with: path: _build - key: shake-4-${{ env.shake_version }}-${{ github.run_id }} - restore-keys: shake-4-${{ env.shake_version }}- + key: shake-5-${{ env.shake_version }}-${{ github.run_id }} + restore-keys: shake-5-${{ env.shake_version }}- - name: Build 🛠️ run: | diff --git a/src/1Lab/Classical.lagda.md b/src/1Lab/Classical.lagda.md index bc58cea3b..f29ad8023 100644 --- a/src/1Lab/Classical.lagda.md +++ b/src/1Lab/Classical.lagda.md @@ -46,16 +46,16 @@ We show that these two statements are equivalent propositions. ```agda LEM-is-prop : is-prop LEM -LEM-is-prop = hlevel! +LEM-is-prop = hlevel 1 DNE-is-prop : is-prop DNE -DNE-is-prop = hlevel! +DNE-is-prop = hlevel 1 LEM→DNE : LEM → DNE LEM→DNE lem P = Dec-elim _ (λ p _ → p) (λ ¬p ¬¬p → absurd (¬¬p ¬p)) (lem P) DNE→LEM : DNE → LEM -DNE→LEM dne P = dne (el (Dec ∣ P ∣) hlevel!) λ k → k (no λ p → k (yes p)) +DNE→LEM dne P = dne (el (Dec ∣ P ∣) (hlevel 1)) λ k → k (no λ p → k (yes p)) LEM≃DNE : LEM ≃ DNE LEM≃DNE = prop-ext LEM-is-prop DNE-is-prop LEM→DNE DNE→LEM @@ -84,7 +84,7 @@ The weak law of excluded middle is also a proposition. ```agda WLEM-is-prop : is-prop WLEM -WLEM-is-prop = hlevel! +WLEM-is-prop = hlevel 1 ``` ## The axiom of choice {defines="axiom-of-choice"} @@ -151,7 +151,7 @@ gives us a section $\Sigma P \to 2$. ```agda module _ (split : Surjections-split) (P : Ω) where section : ∥ ((x : Susp ∣ P ∣) → fibre 2→Σ x) ∥ - section = split Bool-is-set (Susp-prop-is-set hlevel!) 2→Σ 2→Σ-surjective + section = split Bool-is-set (Susp-prop-is-set (hlevel 1)) 2→Σ 2→Σ-surjective ``` But a section is always injective, and the booleans are [[discrete]], so we can @@ -160,11 +160,11 @@ is equivalent to $P$, this concludes the proof. ```agda Discrete-ΣP : Discrete (Susp ∣ P ∣) - Discrete-ΣP = ∥-∥-rec (Dec-is-hlevel 1 (Susp-prop-is-set hlevel! _ _)) + Discrete-ΣP = ∥-∥-rec (Dec-is-hlevel 1 (Susp-prop-is-set (hlevel 1) _ _)) (λ f → Discrete-inj (fst ∘ f) (right-inverse→injective 2→Σ (snd ∘ f)) Discrete-Bool) section AC→LEM : Dec ∣ P ∣ - AC→LEM = Dec-≃ (Susp-prop-path hlevel!) Discrete-ΣP + AC→LEM = Dec-≃ (Susp-prop-path (hlevel 1)) Discrete-ΣP ``` diff --git a/src/1Lab/Equiv/HalfAdjoint.lagda.md b/src/1Lab/Equiv/HalfAdjoint.lagda.md index e7271ede0..9d1ff2742 100644 --- a/src/1Lab/Equiv/HalfAdjoint.lagda.md +++ b/src/1Lab/Equiv/HalfAdjoint.lagda.md @@ -7,7 +7,6 @@ description: | --- diff --git a/src/1Lab/HIT/Truncation.lagda.md b/src/1Lab/HIT/Truncation.lagda.md index f287ecb9b..bdc5e8eb6 100644 --- a/src/1Lab/HIT/Truncation.lagda.md +++ b/src/1Lab/HIT/Truncation.lagda.md @@ -88,13 +88,13 @@ whenever it is a family of propositions, by providing a case for (go x z) (go x₁ z) i ∥-∥-rec : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} - → is-prop P - → (A → P) - → (x : ∥ A ∥) → P + → is-prop P + → (A → P) + → (x : ∥ A ∥) → P ∥-∥-rec pprop = ∥-∥-elim (λ _ → pprop) -∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → is-prop A → ∥ A ∥ → A -∥-∥-proj ap = ∥-∥-rec ap λ x → x +∥-∥-out : ∀ {ℓ} {A : Type ℓ} → is-prop A → ∥ A ∥ → A +∥-∥-out ap = ∥-∥-rec ap λ x → x ∥-∥-rec₂ : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ''} {P : Type ℓ'} → is-prop P @@ -102,15 +102,18 @@ whenever it is a family of propositions, by providing a case for → (x : ∥ A ∥) (y : ∥ B ∥) → P ∥-∥-rec₂ pprop = ∥-∥-elim₂ (λ _ _ → pprop) +∥-∥-elim! + : ∀ {ℓ ℓ'} {A : Type ℓ} {P : ∥ A ∥ → Type ℓ'} ⦃ _ : ∀ {x} → H-Level (P x) 1 ⦄ + → (∀ x → P (inc x)) → ∀ x → P x +∥-∥-elim! = ∥-∥-elim (λ _ → hlevel 1) + ∥-∥-rec! - : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} - → {@(tactic hlevel-tactic-worker) pprop : is-prop P} - → (A → P) - → (x : ∥ A ∥) → P -∥-∥-rec! {pprop = pprop} = ∥-∥-elim (λ _ → pprop) - -∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A -∥-∥-proj! {ap = ap} = ∥-∥-proj ap + : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} ⦃ _ : H-Level P 1 ⦄ + → (A → P) → (x : ∥ A ∥) → P +∥-∥-rec! = ∥-∥-elim (λ _ → hlevel 1) + +∥-∥-out! : ∀ {ℓ} {A : Type ℓ} ⦃ _ : H-Level A 1 ⦄ → ∥ A ∥ → A +∥-∥-out! = ∥-∥-out (hlevel 1) ``` --> @@ -176,7 +179,7 @@ nothing: ```agda is-prop→equiv∥-∥ : ∀ {ℓ} {P : Type ℓ} → is-prop P → P ≃ ∥ P ∥ -is-prop→equiv∥-∥ pprop = prop-ext pprop squash inc (∥-∥-proj pprop) +is-prop→equiv∥-∥ pprop = prop-ext pprop squash inc (∥-∥-out pprop) ``` In fact, an alternative definition of `is-prop`{.Agda} is given by "being @@ -288,6 +291,19 @@ truncation onto a set using a constant map. (λ _ → is-constant→image-is-prop bset f fconst) (f-image f) x .fst ``` + + ## Maps into groupoids We can push this idea further: as discussed in [@Kraus:2015], in general, @@ -466,6 +482,5 @@ instance go : ∥ A ∥ → (A → ∥ B ∥) → ∥ B ∥ go (inc x) f = f x go (squash x y i) f = squash (go x f) (go y f) i - ``` --> diff --git a/src/1Lab/HLevel/Closure.lagda.md b/src/1Lab/HLevel/Closure.lagda.md index e9e95d851..85f76c9ab 100644 --- a/src/1Lab/HLevel/Closure.lagda.md +++ b/src/1Lab/HLevel/Closure.lagda.md @@ -394,6 +394,11 @@ instance opaque H-Level-is-contr : ∀ {n} {ℓ} {T : Type ℓ} → H-Level (is-contr T) (suc n) H-Level-is-contr = prop-instance is-contr-is-prop + + H-Level-is-equiv + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {n} + → H-Level (is-equiv f) (suc n) + H-Level-is-equiv = prop-instance (is-equiv-is-prop _) ``` diff --git a/src/1Lab/Reflection/Deriving/Show.agda b/src/1Lab/Reflection/Deriving/Show.agda index 09a432883..99e9927b7 100644 --- a/src/1Lab/Reflection/Deriving/Show.agda +++ b/src/1Lab/Reflection/Deriving/Show.agda @@ -167,11 +167,11 @@ private derive-show : Name → Name → TC ⊤ derive-show nm dat = do is-defined nm >>= λ where - false → declare (argI nm) =<< instance-type (quote Show) dat + false → declare (argI nm) =<< instance-type (it Show ##_) dat true → pure tt cons ← get-type-constructors dat - (tel , as) ← instance-telescope (quote Show) dat + (tel , as) ← instance-telescope (it Show ##_) dat let ty = unpi-view tel $ itₙ Fun (it Precedence) (itₙ Fun (def dat as) (it ShowS)) work ← helper-function nm "go" ty [] diff --git a/src/1Lab/Reflection/HLevel.agda b/src/1Lab/Reflection/HLevel.agda index 51c35b213..5b3daef2e 100644 --- a/src/1Lab/Reflection/HLevel.agda +++ b/src/1Lab/Reflection/HLevel.agda @@ -1,6 +1,7 @@ -{-# OPTIONS -vtactic.hlevel:20 -vtc.def:10 #-} +open import 1Lab.Reflection.Signature open import 1Lab.Function.Embedding open import 1Lab.Reflection.Record +open import 1Lab.Reflection.Subst open import 1Lab.HLevel.Universe open import 1Lab.HLevel.Closure open import 1Lab.Reflection @@ -11,6 +12,7 @@ open import 1Lab.Path open import 1Lab.Type open import Data.List.Base +open import Data.Nat.Base open import Data.Id.Base open import Data.Bool @@ -21,83 +23,56 @@ open import Prim.Data.Nat module 1Lab.Reflection.HLevel where {- -Tactic for generating readable h-level proofs automatically. Contains an -essential reimplementation of the instance search mechanism, with -support for arbitrary level offsets (`level-minus) and searching under -binders (`search-under). Ambiguity is explicitly supported: the first -goal for which we can complete a proof tree is the one we go with. - -The tactic works in a naïve way, trying h-level lemmas until one -succeeds. There are three ways of making progress: Using a *projection -hint*, using a *decomposition hint*, or by falling back to instance -selection. The instance selection fallback is self-explanatory. - -Projection hints handle the situation is-hlevel (X .p) n, where X -inhabits a record that contains evidence of its hlevel. If there is a -projection hint with `underlying-type == p`, then we use `has-level -(get-argument (X .p))` as the solution. Being a base case, projection -hints also handle raising h-levels: If `get-level (X .p) < n`, we solve -by raising `has-level ...` the appropriate amount. - -Decomposition hints are slightly more interesting. Decomposition hints -apply to a type, say P, and instruct the tactic on how to build an -application of type (is-hlevel P n). The way this application is built -is customizable. - -Finding rules -------------- - -Rules are found using instance search, specifically for the -'hlevel-decomposition' and 'hlevel-projection' types. The -hlevel-projection type is flat, so the runtime of -projection-decomposition is *linear in the number of possible -projections*. - -The hlevel-decomposition type is more interesting, since it is indexed -by the type that it can decompose. That way, we can use Agda's own -instance selection mechanism to narrow down to relevant decompositions. - -Nondeterminism --------------- - -In case more than one projection and/or decomposition hint is possible, -they will all be tried in order. This allows the tactic to generate -sensible-looking code, by trying simpler decompositions first. As an -example, the non-dependent lemmas for → and × will be tried before those -for Π and Σ, just like a human would. --} +Further automation of h-level proofs +------------------------------------ + +This module expands the setup for automation of h-level proofs that is +bootstrapped in 1Lab.HLevel.Closure with the following extra features: + +* Establishing the h-level of 'is-hlevel' itself; at the base-case, this + boils down to instances for `H-Level (is-prop A) (suc n)`. + +* Support for computing h-levels of projections. + +The second bullet point might seem a bit surprising: Agda has native +support for marking some projections as instances ("instance fields"), +so why not use that? The reason is twofold: + +1. + The fields would have to have type ∀ {k} → H-Level X (n + k), where n + is the actual truncation level. + + This is not a big problem, since an n-truncated type is + (n + k)-truncated, but it is slightly unnatural when compared to + having is-hlevel X n. + +2. + Instance fields work by eta-expanding variables in the context. Put + concretely, if we have + + record Set : Type₁ where + field + it : Type₀ + prf : H-Level it 2 + + then the following *would* work, + + module _ {X : Set} where + _ : is-set (X .it) + _ = hlevel 2 + + but the following would not, since 'Y x' is not a variable in the + context. --- | Specifies how an argument should be filled in during elaboration of --- an h-level lemma. -data Arg-spec : Type where - `level-minus : (n : Nat) → Arg-spec - -- ^ Insert the level we're solving for minus the given offset (note - -- that this is the wonky subtraction operation, "monus") at this - -- argument position - - `search-under : (n : Nat) → Arg-spec - -- ^ Recursively search for an h-level witness, under @n@ visible - -- lambdas. This is suitable for lemmas of type - -- (∀ x y z → is-hlevel ...) → is-hlevel ... - - `term : Term → Arg-spec - -- ^ Insert a literal term at this argument position. No search will be - -- performed if this is a meta, so it must be solved from the context in - -- which the lemma is used. - --- Common patterns: Keep the level, search in the current scope. -pattern `search = `search-under 0 -pattern `level = `level-minus 0 -pattern `meta = `term unknown - --- | A specification for how to decompose the type @T@ into --- sub-components, to establish an h-level result. -data hlevel-decomposition {ℓ} (T : Type ℓ) : Type where - decomp - : (h-level-lemma : Name) (arguments : List Arg-spec) - → hlevel-decomposition T - -- To prove that T has a given h-level, we can invoke the - -- @h-level-lemma@ with the specified @arguments@. + module _ {X : Type} {Y : X → Set} where + _ : ∀ {x} → is-hlevel (Y x .it) + _ = hlevel 2 + +To handle this extended situation, we extend the graph of H-Level +instances with a very generic H-Level-projection instance which uses +tactic arguments to decompose (Y x .it) into an application of (.it) + +the argument (Y x). +-} -- | How to decompose an application of a record selector into something -- which might have an h-level. @@ -112,6 +87,7 @@ record hlevel-projection (proj : Name) : Type where -- type have? Necessary for computing lifts. get-argument : List (Arg Term) → TC Term -- ^ Extract the argument out from under the application. + {- Using projections ----------------- @@ -138,668 +114,223 @@ is-hlevel-suc. -} open hlevel-projection -private - -- Throw an empty type error to try another alternative, stating the - -- purpose of backtracking for debugging: - backtrack : ∀ {ℓ} {A : Type ℓ} → List ErrorPart → TC A - backtrack note = do - debugPrint "tactic.hlevel" 10 $ "Backtracking search... " ∷ note - typeError $ "Search hit a dead-end: " ∷ note - - -- A list of names which we should not reduce while trying to invert - -- an application of is-hlevel/is-prop/is-set into an 'underlying - -- type' and level arguments. - hlevel-types : List Name - hlevel-types = quote is-hlevel ∷ quote is-prop ∷ quote is-set ∷ quote is-groupoid ∷ [] - - pattern nat-lit n = - def (quote Number.fromNat) (_ ∷ _ ∷ _ ∷ lit (nat n) v∷ _) - - -- Decompose an application of is-hlevel and/or one of the other - -- 'hlevel-types' into its constituent parts. Invariant: - -- - -- decompose-is-hlevel' t = (a , n) ⊢ t = is-hlevel a n - decompose-is-hlevel' : Term → TC (Term × Term) - - -- Infer the type of the given term, and decompose it according to - -- decompose-is-hlevel'. - decompose-is-hlevel : Term → TC (Term × Term) - decompose-is-hlevel goal = do - ty ← withReduceDefs (false , hlevel-types) $ infer-type goal >>= reduce - decompose-is-hlevel' ty - - decompose-is-hlevel' ty = do - def (quote is-hlevel) (_ ∷ ty v∷ lv v∷ []) ← pure ty - where - -- Handle the ones with special names: - def (quote is-groupoid) (_ ∷ ty v∷ []) → do - ty ← wait-just-a-bit ty - pure (ty , lit (nat 3)) - - def (quote is-set) (_ ∷ ty v∷ []) → do - ty ← wait-just-a-bit ty - pure (ty , lit (nat 2)) - - def (quote is-prop) (_ ∷ ty v∷ []) → do - ty ← wait-just-a-bit ty - pure (ty , lit (nat 1)) - - def (quote is-contr) (_ ∷ ty v∷ []) → do - ty ← wait-just-a-bit ty - pure (ty , lit (nat 0)) - - _ → backtrack "Goal type isn't is-hlevel" - - -- To support having bare hlevel! in the source file, we need to - -- block decomposition on having a rigid-ish type at the - -- top-level. Otherwise the first hint that matches will get - -- matched endlessly until we run out of fuel! - ty ← wait-just-a-bit ty - lv ← wait-just-a-bit lv - pure (ty , lv) - - -- Wait for the "principal argument" of a term, i.e. the (principal - -- argument of) the first visible argument in the spine of a - -- definition. - wait-principal-arg : Term → TC ⊤ - wait-principal-arg topl = go topl where - go : Term → TC ⊤ - go* : List (Arg Term) → TC ⊤ - - go mv@(meta m _) = do - debugPrint "tactic.hlevel" 30 - [ "wait-principal-arg: blocking on meta " , termErr mv , " in principal arguments of\n " - , termErr topl - ] - block-on-meta m - go (def d ds) = go* ds - go t = pure tt - - go* (arg (arginfo visible _) t ∷ as) = go t - go* (arg (arginfo instance' _) t ∷ as) = go t - go* (_ ∷ as) = go* as - go* [] = pure tt - -{- -Lifting n-Types ---------------- - -The n-types are the leaves of the hlevel solving process, so they're -pretty much our only opportunity to adjust levels in a big way. Suppose -you have - - T = def (quote X) as - -with - get-level (get-argument T) = n - w : is-hlevel T n -but what you want is a witness of is-hlevel T (k + n), where k is some -numeral? Well, the solution is obvious: we can compute k - n and lift -T's witness (k - n) levels. Right? - -No: we're dealing with potential open naturals, so we have to be careful -about performing ‘symbolic’ subtractions. The way we do this is with, -essentially, a loop: If w doesn't work, then try +is-hlevel-le : ∀ {ℓ} {A : Type ℓ} n k → n ≤ k → is-hlevel A n → is-hlevel A k +is-hlevel-le 0 k 0≤x p = + is-contr→is-hlevel k p +is-hlevel-le 1 1 (s≤s 0≤x) p = p +is-hlevel-le 1 (suc (suc k)) (s≤s 0≤x) p x y = + is-prop→is-hlevel-suc (is-prop→is-set p x y) +is-hlevel-le (suc (suc n)) (suc (suc k)) (s≤s le) p x y = + is-hlevel-le (suc n) (suc k) le (p x y) + +hlevel-proj : ∀ {ℓ} → Type ℓ → Nat → Term → TC ⊤ +hlevel-proj A want goal = do + want ← quoteTC want >>= normalise + + def head args ← reduce =<< quoteTC A + where ty → typeError [ "H-Level: I do not know how to show that\n " , termErr ty , "\nhas h-level\n", termErr want ] + debugPrint "tactic.hlevel" 30 [ "H-Level: trying projections for term:\n " , termErr (def head args), "\nwith head symbol ", nameErr head ] + + projection ← resetting do + (mv , _) ← new-meta' (def (quote hlevel-projection) (argN (lit (name head)) ∷ [])) + get-instances mv >>= λ where + [] → typeError + [ "H-Level: There are no hints for treating the name" , nameErr head , "as a projection." + , "When showing that the type\n " , termErr (def head args) + , "\nhas h-level " , termErr want , ".\n" + ] - is-hlevel-suc n w : is-hlevel T (suc n) + (tm ∷ []) → unquoteTC {A = hlevel-projection head} =<< normalise tm -until you reach a sucᵏ n = k + n. Actually, slightly more efficient, we -keep around a counter k' for the number of tries, and transfer successors -from the wanted level (k + n) until is-hlevel-+ n (sucᵏ' n) w works. --} - lift-sol : Term → Term → Nat → Term - lift-sol tm _ 0 = tm - lift-sol tm l1 l = def (quote is-hlevel-+) (l1 v∷ lit (nat l) v∷ tm v∷ []) - - pred-term : Term → Maybe Term - pred-term (con (quote suc) (x v∷ [])) = just x - pred-term (lit (nat n)) with n - ... | suc k = just (lit (nat k)) - ... | _ = nothing - pred-term _ = nothing - - {-# TERMINATING #-} - lifting-loop : Nat → Term → Term → Term → Term → TC ⊤ - lifting-loop it solution goal l1 l2 = - let's-hope <|> do - (just l2') ← pred-term <$> normalise l2 where - nothing → backtrack "Lifting loop reached its end with no success" - lifting-loop (suc it) solution goal l1 l2' - where - let's-hope : TC ⊤ - let's-hope = do - debugPrint "tactic.hlevel" 30 $ "Lifting loop: Trying " ∷ termErr (lift-sol solution l1 it) ∷ " for level " ∷ termErr l2 ∷ [] - unify goal (lift-sol solution l1 it) - - -- Projection decomposition. - treat-as-n-type : ∀ {n} → hlevel-projection n → Term → TC ⊤ - treat-as-n-type projection goal = do - -- First we must be looking at a goal which is of the type is-hlevel - -- A n. We'll need both n and A. - (ty , wanted-level) ← decompose-is-hlevel goal - debugPrint "tactic.hlevel" 10 $ - "Attempting to treat as " ∷ termErr wanted-level ∷ "-Type: " ∷ termErr ty ∷ [] - ty ← reduce ty - - -- Reduce the type to whnf and check whether the outermost term - -- constructor is an application of the projection we're looking - -- for. - def namen args ← pure ⦃ Idiom-TC ⦄ ty - where what → backtrack $ "Thing isn't an application, it is " ∷ termErr what ∷ [] - - it ← projection .get-argument args - - -- And compute the level of the projected thing, in addition to a - -- numeral form of the wanted level. - actual-level ← infer-type it >>= projection .get-level - - debugPrint "tactic.hlevel" 10 $ - "... but it's actually a(n) " ∷ termErr actual-level ∷ "-Type" ∷ [] - - lv ← normalise wanted-level - lv' ← normalise actual-level - lifting-loop 0 (def (projection .has-level) (it v∷ [])) goal lv' lv - - commitTC - - -- Fall back to Agda's instance search mechanism. This isn't as - -- straightforward as just using the 'hlevel' function for a couple of - -- reasons. - use-instance-search : Bool → Term → TC ⊤ - use-instance-search has-alts goal = run-speculative $ do - (ty , lv) ← decompose-is-hlevel goal - (mv , solved) ← new-meta' (def (quote H-Level) (ty v∷ lv v∷ [])) - instances ← get-instances mv - - t ← quoteTC instances - debugPrint "tactic.hlevel" 10 $ - "Using instance search for\n" ∷ termErr ty ∷ - "\nFound candidates\n " ∷ termErr t ∷ [] - - -- We actually want to manage the instance searching ourselves, - -- sorta, to avoid getting into situations where the macro has - -- committed to instance search but Agda will disagree with it. - let - go : List Term → TC (⊤ × Bool) - go = λ where - -- If there is *exactly* one instance candidate for this goal, - -- then we can go ahead and solve it. That's because having - -- exactly one instance means Agda will solve using that - -- instance! - (x ∷ []) → do - -- Note that, since get-instances works by creating a new meta, - -- we have to commit to the instance ourselves. - unify solved x - withReduceDefs (false , quote hlevel ∷ []) $ withReconstructed true $ - unify goal (def (quote hlevel) (lv v∷ [])) - pure (tt , true) - - -- If there are any more alternatives to be tried after this - -- one, then we fail (backtrack). Otherwise, we discard the TC - -- state but indicate success: this will cause the meta to be - -- solved with an interaction point (if using - -- elaborate-and-give). - [] → if has-alts - then backtrack "No possible instances, but have other decompositions to try" - else pure (tt , false) - - _ → backtrack "Too many possible instances; will not use instance search for this goal" - go instances - - -- Entry point for calling the tactic. - search : Bool → Term → Nat → Term → TC ⊤ - -- Give up if we're out of fuel: - search has-alts _ zero goal = unify goal unknown - - -- Actual main loop: try using the hints database, try treating the - -- goal as an n-type, fall back to instance search. - search has-alts level (suc n) goal = - use-projections - <|> use-hints - <|> use-instance-search has-alts goal - <|> typeError "Search failed!!" - where - open hlevel-projection - - -- Nondeterministically use a projection for establishing the - -- result. This follows the approach described in [Using - -- projections]. - use-projections : TC ⊤ - use-projections = do - def qn _ ← (fst <$> decompose-is-hlevel goal) >>= reduce - where tm → backtrack $ "Term " ∷ termErr tm ∷ " is not headed by a definition; ignoring projections." - - goalt ← infer-type goal - debugPrint "tactic.hlevel" 20 $ - "Will attempt to use projections for goal\n " ∷ termErr goalt ∷ [] - - (solved , instances) ← run-speculative $ do - (mv , solved) ← new-meta' (def (quote hlevel-projection) (lit (name qn) v∷ [])) - - -- If there are some hints, then great, otherwise we discard - -- the TC state. - (x ∷ xs) ← get-instances mv - where [] → pure ((unknown , []) , false) - - pure ((solved , x ∷ xs) , true) - - nondet (eff List) instances λ a → do - projection ← unquoteTC {A = hlevel-projection qn} a - ty ← withReduceDefs (false , hlevel-types) (infer-type goal >>= reduce) - debugPrint "tactic.hlevel" 20 $ - "Outer type: " ∷ termErr ty ∷ [] - treat-as-n-type projection goal >> unify solved a - - -- Get rid of any invisible binders that lead the term. - remove-invisible : Term → Term → TC Term - remove-invisible - (lam _ (abs _ t)) - (pi (arg (arginfo invisible _) _) (abs _ ret)) - = remove-invisible t ret - remove-invisible inner _ = pure inner - - -- Search using decompositions involves manipulating the scope, - -- which is why it's spread over so many functions, and even then, - -- some are too big. - - -- Wrap the given term in a series of visible lambdas. - wrap-lams : Nat → Term → Term - wrap-lams zero r = r - wrap-lams (suc x) r = lam visible $ abs "a" $ wrap-lams x r - - -- Compute a continuation which extends the context by n visible - -- variables, all typed 'unknown'. - extend-n : ∀ {ℓ} → Nat → TC ((A : Type ℓ) → TC A → TC A) - extend-n zero = pure λ _ x → x - extend-n (suc n) = do - rest ← extend-n n - lift mv ← rest (Lift _ Term) $ lift <$> new-meta unknown - let domain = arg (arginfo visible (modality relevant quantity-ω)) mv - pure λ a k → rest a $ extend-context "a" domain $ k - - -- Given a list of argument specs, actually unify the goal with - -- the solution of decomposition, and call a continuation to - -- perform any outstanding searches. - gen-args - : Bool -- ^ Are there any alternatives after this one? - → Term -- ^ What level are we searching for? - - → Name -- ^ Name of the lemma, - → List Arg-spec -- ^ and the arguments we should invent. - - → List (Arg Term) - -- ^ Accumulator: computed arguments (criminally, in reverse - -- order) - → TC ⊤ - -- ^ Accumulator/continuation: what do we need to do after - -- unifying the goal with the lemma?. This is both - -- continuation (it can be used to run something after the - -- arguments are built) and accumulator (searching recursively - -- is done last). - → TC ⊤ -- ^ Returns nada - gen-args has-alts level defn [] accum cont = do - -- If we have no arguments to generate, then we can go ahead and - -- use the accumulator as-is. - unify goal (def defn (reverse accum)) - debugPrint "tactic.hlevel" 10 $ - "Committed to solution: " ∷ termErr (def defn (reverse accum)) ∷ [] - cont - - gen-args has-alts level defn (x ∷ args) accum cont with x - -- If we got asked for the level without an adjustment (i.e. monus - -- by zero), then we may as well not bother *trying* to adjust it. - -- Saves a bit of computation. - ... | `level-minus 0 = gen-args has-alts level defn args (level v∷ accum) cont - -- If we have to insert the level minus some offset, then we need - -- to do the computation: - ... | `level-minus n@(suc _) = - do - level ← normalise level - debugPrint "tactic.hlevel" 10 $ - "Hint demands offset, performing symbolic monus, subtracting from\n " ∷ termErr level ∷ [] - level'' ← monus level n - -- Reduce otherwise we get Number.fromNat as the term - gen-args has-alts level defn args (level'' v∷ accum) cont - where - -- A 'symbolic' monus function. If we're looking at an actual - -- number, then we can just do the computation in TC, but - -- otherwise we have to reimplement the builtin subtraction, - -- where the minuend is a *term* rather than a number. In - -- addition to being a bad operation (monus, grr), it's - -- *partial*. We can end up backtracking while subtracting. - monus : Term → Nat → TC Term - monus (lit (nat n)) k = pure $ lit (nat (n - k)) - monus tm zero = pure tm - monus thezero@(con (quote zero) []) (suc it) = pure thezero - monus (con (quote suc) (x v∷ [])) (suc it) = do - x ← reduce x - monus x it - monus tm (suc it) = do - debugPrint "tactic.hlevel" 10 $ "Dunno how to take 1 from " ∷ termErr tm ∷ [] - typeError [] - - ... | `term t = gen-args has-alts level defn args (t v∷ accum) cont - - ... | `search-under under = do - -- To search under some variables, we work in a scope extended - -- by 'under'-many variables. The metavariable lives in that - -- scope, so we have to quantify over the variables we - -- introduced to use it outside, i.e., in the actual (outer) - -- search problem. - debugPrint "tactic.hlevel" 10 $ "Going under " ∷ termErr (lit (nat under)) ∷ [] - gounder ← extend-n under - mv ← gounder Term $ do - debugPrint "tactic.hlevel" 10 $ "In extended context" - new-meta unknown - debugPrint "tactic.hlevel" 10 $ "Metavariable: " ∷ termErr (wrap-lams under mv) ∷ [] - -- After we've put the mv wrapped under some lambdas in the - -- argument list, - gen-args has-alts level defn args (wrap-lams under mv v∷ accum) $ do - -- On our way back up, we do any more searching that needed to - -- get done, and.. - cont - -- go back under the new scope to recursively search for - -- levels. - gounder ⊤ $ search has-alts unknown n mv - - -- Try all the candidate hints in order. This is a version of - -- 'nondet' which additionally threads whether we're looking at - -- last alternative. - use-decomp-hints : (Term × Term) → Term → List Term → TC (⊤ × Bool) - use-decomp-hints (goal-ty , lv) solved (c1 ∷ cs) = do - ty ← infer-type c1 - c1' ← reduce c1 - (remove-invisible c1' ty >>= λ where - - -- If we have an actual decomp constructor, then we can try - -- using its argument specification to construct a little - -- h-level lemma - (con (quote decomp) (_ ∷ _ ∷ nm v∷ argspec v∷ [])) → do - debugPrint "tactic.hlevel" 10 $ - "Using " ∷ termErr nm ∷ " decomposition for:\n " - ∷ termErr (def (quote is-hlevel) (goal-ty v∷ lv v∷ [])) ∷ [] - - nm' ← unquoteTC nm - argsp ← unquoteTC argspec - -- Generate the argument spine, and discard the instance - -- search meta. - gen-args (not (length cs == 0)) lv nm' argsp [] (pure tt) - unify solved c1 - - pure (tt , true) - - -- It's possible that this particular hint was a bust, i.e. - -- because someone wasn't being careful with what - -- hlevel-decomposition instances they've defined. That's no - -- matter: we can just ignore it. - _ → backtrack "Non-canonical hint") - -- If we didn't manage to get the hint to work, for any - -- reason, try again with the rest of the hints. - <|> use-decomp-hints (goal-ty , lv) solved cs - - use-decomp-hints (goal-ty , _) _ [] = - backtrack $ "Ran out of decomposition hints for " ∷ termErr goal-ty ∷ [] - - -- Using the hints involving querying Agda for potential - -- instances, then trying each in order. - use-hints : TC ⊤ - use-hints = run-speculative $ do - (ty , lv) ← decompose-is-hlevel goal - - -- We have to block on any metavariable here which is blocking - -- head-normalisation of the goal type. Unfortunately the - -- reflection interface does not let us reduce with a blocker. - -- - -- The reason is twofold: - -- - -- (a) if the type is a bare meta, the tactic may go into a tailspin. - -- - -- (b) if the type a projection blocked on a meta, - -- e.g. .Pathᵉ (_123 ...) ..., - -- then we may commit to an incorrect solution too early, - -- preventing the extensionality tactic from doing *its* - -- job. - wait-principal-arg ty - - -- Create a meta of type hlevel-decomposition to find any possible hints.. - (mv , solved) ← new-meta' (def (quote hlevel-decomposition) (ty v∷ [])) - instances ← get-instances mv - - t ← quoteTC instances - debugPrint "tactic.hlevel" 10 $ - "Finding decompositions for\n" ∷ - termErr ty ∷ - "\nFound candidates\n " ∷ - termErr t ∷ [] - - -- And try using the hints. - use-decomp-hints (ty , lv) solved instances - - -- At the top-level, our goal doesn't need to have literally the type - -- is-hlevel A n. It can be under any number of Πs, both implicit and - -- explicit. This means that a goal like (∀ x → is-hlevel T n) can be - -- solved using just hlevel!, rather than λ _ → hlevel!. Of course, - -- the effect is the same. - decompose-is-hlevel-top - : ∀ {ℓ} {A : Type ℓ} - → Term → TC (Term × Term × (TC A → TC A) × (Term → Term)) - decompose-is-hlevel-top goal = - do - ty ← withReduceDefs (false , hlevel-types) $ - infer-type goal >>= reduce >>= wait-just-a-bit - go ty - where - go : Term → TC _ - go (pi (arg as at) (abs vn cd)) = do - (inner , hlevel , enter , leave) ← go cd - pure $ inner , hlevel , extend-context vn (arg as at) ∘ enter , λ t → lam (ArgInfo.arg-vis as) (abs vn (leave t)) - go tm = do - (inner , hlevel) ← decompose-is-hlevel' tm - pure $ inner , hlevel , (λ x → x) , (λ x → x) - --- This is public so it's usable in tactic attributes. It decomposes the --- top-level goal type and enters the search loop. -hlevel-tactic-worker : Term → TC ⊤ -hlevel-tactic-worker goal = do - ty ← withReduceDefs (false , hlevel-types) $ infer-type goal >>= reduce - (ty , lv , enter , leave) ← decompose-is-hlevel-top goal <|> - typeError - ( "hlevel tactic: goal type is not of the form ``is-hlevel A n'':\n" - ∷ termErr ty - ∷ []) - - -- 10 units of fuel isn't too many but it's enough for any realistic - -- use-case. Note the scope nonsense: we have to 'enter' to get under - -- the Πs (extend the scope with their argument types), then 'leave' - -- (wrap in lambdas) to get back out. - solved ← enter $ do - goal' ← new-meta (def (quote is-hlevel) (ty v∷ lv v∷ [])) - search false lv 10 goal' - pure goal' - unify goal (leave solved) - --- Entry points to the macro ----------------------------- -macro hlevel! = hlevel-tactic-worker - --- In addition to using the macro as a.. well, macro, it can be used as --- a tactic argument, to replace instance search by the more powerful --- decomposition-projection mechanism of the tactic. We provide only --- some of the most common helpers: -el! : ∀ {ℓ} (A : Type ℓ) {n} {@(tactic hlevel-tactic-worker) hl : is-hlevel A n} → n-Type ℓ n -∣ el! A {hl = hl} ∣ = A -el! A {hl = hl} .is-tr = hl + insts@(_ ∷ _ ∷ _) → do + tms ← quoteTC insts >>= normalise + typeError + [ "H-Level: Ambiguous inversions for projection\n " + , nameErr head + , "\nAll of the following apply:\n" + , termErr tms + ] + it ← projection .get-argument args + lvl ← projection .get-level =<< infer-type it -biimp-is-equiv! - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} - {@(tactic hlevel-tactic-worker) aprop : is-hlevel A 1} - {@(tactic hlevel-tactic-worker) bprop : is-hlevel B 1} - → (f : A → B) → (B → A) - → is-equiv f -biimp-is-equiv! {aprop = aprop} {bprop = bprop} = biimp-is-equiv aprop bprop + let + soln = def (quote is-hlevel-le) + [ argN lvl + , argN want + , argN (def (quote auto) []) + , argN (def (projection .has-level) [ argN it ]) + ] -prop-ext! - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} - {@(tactic hlevel-tactic-worker) aprop : is-hlevel A 1} - {@(tactic hlevel-tactic-worker) bprop : is-hlevel B 1} - → (A → B) → (B → A) - → A ≃ B -prop-ext! {aprop = aprop} {bprop = bprop} = prop-ext aprop bprop - -Σ-prop-path! - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} - → {@(tactic hlevel-tactic-worker) bxprop : ∀ x → is-hlevel (B x) 1} - → {x y : Σ A B} - → x .fst ≡ y .fst - → x ≡ y -Σ-prop-path! {bxprop = bxprop} = Σ-prop-path bxprop - -prop! - : ∀ {ℓ} {A : I → Type ℓ} {@(tactic hlevel-tactic-worker) aip : is-hlevel (A i0) 1} - → {x : A i0} {y : A i1} - → PathP (λ i → A i) x y -prop! {A = A} {aip = aip} {x} {y} = - is-prop→pathp (λ i → coe0→i (λ j → is-prop (A j)) i aip) x y - -injective→is-embedding! - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} - {@(tactic hlevel-tactic-worker) bset : is-set B} - → ∀ {f : A → B} - → injective f - → is-embedding f -injective→is-embedding! {bset = bset} {f} inj = injective→is-embedding bset f inj + unify goal soln open hlevel-projection --- Hint database bootstrap --------------------------- --- This instance block contains most of the decompositions we have --- defined in the dependencies of this module. - instance - decomp-lift : ∀ {ℓ ℓ'} {T : Type ℓ} → hlevel-decomposition (Lift ℓ' T) - decomp-lift = decomp (quote Lift-is-hlevel) (`level ∷ `search ∷ []) - - -- h-level types themselves are propositions. These instances should be tried - -- before Π types. - - decomp-is-prop : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (is-prop A) - decomp-is-prop = decomp (quote is-hlevel-is-hlevel-suc) (`level-minus 1 ∷ `term (lit (nat 1)) ∷ []) - - decomp-is-set : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (is-set A) - decomp-is-set = decomp (quote is-hlevel-is-hlevel-suc) (`level-minus 1 ∷ `term (lit (nat 2)) ∷ []) - - decomp-is-groupoid : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (is-groupoid A) - decomp-is-groupoid = decomp (quote is-hlevel-is-hlevel-suc) (`level-minus 1 ∷ `term (lit (nat 3)) ∷ []) + open hlevel-projection + hlevel-proj-n-type : hlevel-projection (quote n-Type.∣_∣) + hlevel-proj-n-type .has-level = quote n-Type.is-tr + hlevel-proj-n-type .get-level ty = do + def (quote n-Type) (ell v∷ lv't v∷ []) ← reduce ty + where _ → typeError $ "Type of thing isn't n-Type, it is " ∷ termErr ty ∷ [] + normalise lv't + hlevel-proj-n-type .get-argument (_ ∷ _ ∷ it v∷ []) = pure it + hlevel-proj-n-type .get-argument _ = typeError [] - {- - Since `is-prop A` starts with a Π, the decomp-piⁿ instances below could "bite" into - it and make decomp-is-prop inapplicable. To avoid this, we handle those situations explicitly: - -} +instance + H-Level-projection + : ∀ {ℓ} {A : Type ℓ} {n : Nat} + → {@(tactic hlevel-proj A n) inst : is-hlevel A n} + → H-Level A n + H-Level-projection {inst = inst} = hlevel-instance inst - decomp-pi²-is-prop : ∀ {ℓa ℓb ℓc} {A : Type ℓa} {B : A → Type ℓb} {C : ∀ a (b : B a) → Type ℓc} - → hlevel-decomposition (∀ a b → is-prop (C a b)) - decomp-pi²-is-prop = decomp (quote Π-is-hlevel²) (`level ∷ `search-under 2 ∷ []) + H-Level-n-Type : ∀ {ℓ n k} ⦃ _ : suc n ≤ k ⦄ → H-Level (n-Type ℓ n) k + H-Level-n-Type {n = n} {k} = hlevel-instance (is-hlevel-le (suc n) k auto (n-Type-is-hlevel n)) - decomp-pi-is-prop : ∀ {ℓa ℓb} {A : Type ℓa} {B : A → Type ℓb} - → hlevel-decomposition (∀ a → is-prop (B a)) - decomp-pi-is-prop = decomp (quote Π-is-hlevel) (`level ∷ `search-under 1 ∷ []) + h-level-is-prop : ∀ {ℓ} {A : Type ℓ} {n : Nat} ⦃ _ : 1 ≤ n ⦄ → H-Level (is-prop A) n + h-level-is-prop ⦃ s≤s _ ⦄ = hlevel-instance (is-prop→is-hlevel-suc is-prop-is-prop) - -- -- Non-dependent Π and Σ for readability first: + {-# INCOHERENT H-Level-projection #-} + {-# OVERLAPPING h-level-is-prop #-} - -- decomp-fun = decomp (quote fun-is-hlevel) (`level ∷ `search ∷ []) +open Data.Nat.Base using (0≤x ; s≤s' ; x≤x ; x≤sucy) public - -- decomp-prod : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → hlevel-decomposition (A × B) - -- decomp-prod = decomp (quote ×-is-hlevel) (`level ∷ `search ∷ `search ∷ []) +private module _ {ℓ} {A : n-Type ℓ 2} {B : ∣ A ∣ → n-Type ℓ 3} where + some-def = ∣ A ∣ - -- Dependent type formers: + _ : is-hlevel (∣ A ∣ → ∣ A ∣) 2 + _ = hlevel {T = _ → _} 2 - decomp-pi³ - : ∀ {ℓa ℓb ℓc ℓd} {A : Type ℓa} {B : A → Type ℓb} {C : ∀ x (y : B x) → Type ℓc} - → {D : ∀ x y (z : C x y) → Type ℓd} - → hlevel-decomposition (∀ a b c → D a b c) - decomp-pi³ = decomp (quote Π-is-hlevel³) (`level ∷ `search-under 3 ∷ []) + _ : is-hlevel (Σ some-def λ x → ∣ B x ∣) 3 + _ = hlevel 3 - decomp-pi² - : ∀ {ℓa ℓb ℓc} {A : Type ℓa} {B : A → Type ℓb} {C : ∀ x (y : B x) → Type ℓc} - → hlevel-decomposition (∀ a b → C a b) - decomp-pi² = decomp (quote Π-is-hlevel²) (`level ∷ `search-under 2 ∷ []) + _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 5 + _ = λ a → hlevel 5 - decomp-pi : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (∀ a → B a) - decomp-pi = decomp (quote Π-is-hlevel) (`level ∷ `search-under 1 ∷ []) + _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 3 + _ = λ a → hlevel 3 - decomp-impl-pi : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (∀ {a} → B a) - decomp-impl-pi = decomp (quote Π-is-hlevel') (`level ∷ `search-under 1 ∷ []) + _ : is-hlevel ∣ A ∣ 2 + _ = hlevel 2 - decomp-sigma : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (Σ A B) - decomp-sigma = decomp (quote Σ-is-hlevel) (`level ∷ `search ∷ `search-under 1 ∷ []) + _ : ∀ n → is-hlevel (n-Type ℓ n) (suc n) + _ = λ n → hlevel (suc n) - -- Path decomposition rules we have in scope. Note the use of - -- nondeterminism: the following three instances both compete for - -- solving the same goals --- but generally only one will be - -- applicable. That way we don't have to juggle h-levels quite as - -- much. - decomp-path' : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ b) - decomp-path' = decomp (quote Path-is-hlevel') (`level ∷ `search ∷ `meta ∷ `meta ∷ []) + _ : ∀ n (x : n-Type ℓ n) → is-hlevel ∣ x ∣ (2 + n) + _ = λ n x → hlevel (2 + n) - decomp-path : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ b) - decomp-path = decomp (quote Path-is-hlevel) (`level ∷ `search ∷ []) + _ : ∀ k {ℓ} {A : n-Type ℓ k} → is-hlevel ∣ A ∣ (4 + k) + _ = λ k → hlevel (4 + k) - decomp-id : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ᵢ b) - decomp-id = decomp (quote Id-is-hlevel) (`level ∷ `search ∷ []) + _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x : A) → is-prop A) + _ = hlevel 1 - decomp-id' : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ᵢ b) - decomp-id' = decomp (quote Id-is-hlevel') (`level ∷ `search ∷ []) + _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x y : A) → is-prop A) + _ = hlevel 1 - decomp-univalence : ∀ {ℓ} {A B : Type ℓ} → hlevel-decomposition (A ≡ B) - decomp-univalence = decomp (quote ≡-is-hlevel) (`level ∷ `search ∷ `search ∷ [] ) + _ : ∀ {ℓ} {A : Type ℓ} → is-groupoid (is-hlevel A 5) + _ = hlevel 3 - -- This one really ought to work with instance selection only, but - -- Agda has trouble with the (1 + k + n) level in H-Level-n-Type. The - -- decomposition here is a bit more flexible. - decomp-ntype : ∀ {ℓ} {n} → hlevel-decomposition (n-Type ℓ n) - decomp-ntype = decomp (quote n-Type-is-hlevel) (`level-minus 1 ∷ []) +private variable + ℓ ℓ' : Level + A B C : Type ℓ - hlevel-proj-n-type : hlevel-projection (quote n-Type.∣_∣) - hlevel-proj-n-type .has-level = quote n-Type.is-tr - hlevel-proj-n-type .get-level ty = do - def (quote n-Type) (ell v∷ lv't v∷ []) ← reduce ty - where _ → backtrack $ "Type of thing isn't n-Type, it is " ∷ termErr ty ∷ [] - normalise lv't - hlevel-proj-n-type .get-argument (_ ∷ _ ∷ it v∷ []) = pure it - hlevel-proj-n-type .get-argument _ = typeError [] +{- +In addition to the top-level 'hlevel' entry point, there are quite a few +helper functions which simplify use sites by hiding the repetitive +(hlevel n) arguments. +-} -private - module _ {ℓ} {A : n-Type ℓ 2} {B : ∣ A ∣ → n-Type ℓ 3} where - -- some-def = ∣ A ∣ - -- _ : is-hlevel (∣ A ∣ → ∣ A ∣ → ∣ A ∣ → ∣ A ∣) 2 - -- _ = hlevel! +el! : ∀ {ℓ} (A : Type ℓ) {n} ⦃ hl : H-Level A n ⦄ → n-Type ℓ n +el! A .∣_∣ = A +el! A {n} .is-tr = hlevel n - -- _ : is-hlevel (Σ some-def λ x → ∣ B x ∣) 3 - -- _ = hlevel! +biimp-is-equiv! + : ⦃ aprop : H-Level A 1 ⦄ ⦃ bprop : H-Level B 1 ⦄ + → (f : A → B) → (B → A) + → is-equiv f +biimp-is-equiv! = biimp-is-equiv (hlevel 1) (hlevel 1) - _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 5 - _ = hlevel! +prop-ext! + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + → ⦃ aprop : H-Level A 1 ⦄ ⦃ bprop : H-Level B 1 ⦄ + → (A → B) → (B → A) + → A ≃ B +prop-ext! = prop-ext (hlevel 1) (hlevel 1) - _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 3 - _ = hlevel! +Σ-prop-path! + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} + → ⦃ bxprop : ∀ {x} → H-Level (B x) 1 ⦄ + → {x y : Σ A B} + → x .fst ≡ y .fst + → x ≡ y +Σ-prop-path! = Σ-prop-path (λ x → hlevel 1) - _ : is-hlevel ∣ A ∣ 2 - _ = hlevel! +Σ-prop-pathp! + : ∀ {ℓ ℓ'} {A : I → Type ℓ} {B : ∀ i → A i → Type ℓ'} + → ⦃ bxprop : ∀ {i x} → H-Level (B i x) 1 ⦄ + → {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)} + → PathP A (x .fst) (y .fst) + → PathP (λ i → Σ (A i) (B i)) x y +Σ-prop-pathp! = Σ-prop-pathp (λ _ _ → hlevel 1) - _ : ∀ n → is-hlevel (n-Type ℓ n) (suc n) - _ = hlevel! +prop! + : ∀ {ℓ} {A : I → Type ℓ} ⦃ aip : ∀ {i} → H-Level (A i) 1 ⦄ {x y} + → PathP (λ i → A i) x y +prop! {A = A} {x} {y} = + is-prop→pathp (λ i → coe0→i (λ j → is-prop (A j)) i (hlevel 1)) x y - _ : ∀ n (x : n-Type ℓ n) → is-hlevel ∣ x ∣ (2 + n) - _ = hlevel! +injective→is-embedding! + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ bset : H-Level B 2 ⦄ {f : A → B} + → injective f + → is-embedding f +injective→is-embedding! {f = f} inj = injective→is-embedding (hlevel 2) f inj - _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x : A) → is-prop A) - _ = hlevel! +Iso→is-hlevel! : (n : Nat) → Iso B A → ⦃ _ : H-Level A n ⦄ → is-hlevel B n +Iso→is-hlevel! n i = Iso→is-hlevel n i (hlevel n) - _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x y : A) → is-prop A) - _ = hlevel! +{- +Metaprogram for defining instances of H-Level (R x) n, where R x is a +record type whose components can all immediately be seen to have h-level +n. + +That is, this works for things like Cat.Morphism._↪_, since the H-Level +automation already works for showing that its representation as a Σ-type +has hlevel 2, but it does not work for Algebra.Group.is-group, since +that requires specific knowledge about is-group to work. + +Can be used either for unquoteDecl or unquoteDef. In the latter case, it +is possible to give the generated instance a more specific context which +might help to automatically derive instances for more types. +-} - _ : ∀ {ℓ} {A : Type ℓ} → is-groupoid (is-hlevel A 5) - _ = hlevel! +private + record-hlevel-instance + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n : Nat) ⦃ _ : H-Level A n ⦄ + → Iso B A + → ∀ {k} ⦃ p : n ≤ k ⦄ + → H-Level B k + record-hlevel-instance n im ⦃ p ⦄ = hlevel-instance $ + Iso→is-hlevel _ im (is-hlevel-le _ _ p (hlevel _)) + +declare-record-hlevel : (n : Nat) → Name → Name → TC ⊤ +declare-record-hlevel lvl inst rec = do + (rec-tele , _) ← pi-view <$> get-type rec + + eqv ← helper-function-name rec "isom" + declare-record-iso eqv rec + + let + args = reverse $ map-up (λ n (_ , arg i _) → arg i (var₀ n)) 2 (reverse rec-tele) + + head-ty = it H-Level ##ₙ def rec args ##ₙ var₀ 1 + + inst-ty = unpi-view (map (λ (nm , arg _ ty) → nm , argH ty) rec-tele) $ + pi (argH (it Nat)) $ abs "n" $ + pi (argI (it _≤_ ##ₙ lit (nat lvl) ##ₙ var₀ 0)) $ abs "le" $ + head-ty + + declare (argI inst) inst-ty + define-function inst + [ clause [] [] (it record-hlevel-instance ##ₙ lit (nat lvl) ##ₙ def₀ eqv) ] diff --git a/src/1Lab/Reflection/Signature.agda b/src/1Lab/Reflection/Signature.agda index 4d3a058ee..222931d7d 100644 --- a/src/1Lab/Reflection/Signature.agda +++ b/src/1Lab/Reflection/Signature.agda @@ -215,15 +215,15 @@ private make-args : Nat → List (Arg Nat) → List (Arg Term) make-args n xs = reverse $ map (λ (arg ai i) → arg ai (var (n - i - 1) [])) xs - class-for-param : Name → Nat → List (Arg Nat) → Term → Maybe Term + class-for-param : (Arg Term → Term) → Nat → List (Arg Nat) → Term → Maybe Term class-for-param class n xs (agda-sort _) = - just (def class (argN (var n (make-args n xs)) ∷ [])) + just (class (argN (var n (make-args n xs)))) class-for-param class n xs (pi a (abs s b)) = pi (argH (Arg.unarg a)) ∘ abs s <$> class-for-param class (suc n) (arg (Arg.arg-info a) n ∷ xs) b class-for-param _ _ _ _ = nothing - compute-telescope : Name → Nat → List (Arg Nat) → Telescope → Telescope → Telescope × List (Arg Term) + compute-telescope : (Arg Term → Term) → Nat → List (Arg Nat) → Telescope → Telescope → Telescope × List (Arg Term) compute-telescope d n xs is [] = reverse is , make-args (n + length is) xs compute-telescope d n xs is ((x , a) ∷ tel) = let @@ -247,14 +247,14 @@ private -- That is, all the parameters of the data type are bound invisibly, and -- parameters that (end in) a type additionally have corresponding -- instances of the class available. -instance-telescope : Name → Name → TC (Telescope × List (Arg Term)) +instance-telescope : (Arg Term → Term) → Name → TC (Telescope × List (Arg Term)) instance-telescope class dat = do (tele , _) ← pi-view <$> get-type dat pure (compute-telescope class 0 [] [] tele) -- Like `instance-telescope`, but instead return the complete pi-type of -- the derived instance. -instance-type : Name → Name → TC Term +instance-type : (Arg Term → Term) → Name → TC Term instance-type class dat = do (tel , vs) ← instance-telescope class dat - pure $ unpi-view tel $ def class [ argN (def dat vs) ] + pure $ unpi-view tel $ class (argN (def dat vs)) diff --git a/src/1Lab/Resizing.lagda.md b/src/1Lab/Resizing.lagda.md index 3903e58a2..87e0c68f0 100644 --- a/src/1Lab/Resizing.lagda.md +++ b/src/1Lab/Resizing.lagda.md @@ -118,21 +118,12 @@ of any universe. These functions compute on `inc`{.Agda}s, as usual. □-map f (inc x) = inc (f x) □-map f (squash x y i) = squash (□-map f x) (□-map f y) i -□-rec! - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} - → {@(tactic hlevel-tactic-worker) pa : is-prop B} - → (A → B) → □ A → B -□-rec! {pa = pa} f (inc x) = f x -□-rec! {pa = pa} f (squash x y i) = - pa (□-rec! {pa = pa} f x) (□-rec! {pa = pa} f y) i - -out! : ∀ {ℓ} {A : Type ℓ} - → {@(tactic hlevel-tactic-worker) pa : is-prop A} - → □ A → A -out! {pa = pa} = □-rec! {pa = pa} (λ x → x) +□-rec : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is-prop B → (A → B) → □ A → B +□-rec bp f (inc x) = f x +□-rec bp f (squash x y i) = bp (□-rec bp f x) (□-rec bp f y) i elΩ : ∀ {ℓ} (T : Type ℓ) → Ω -∣ elΩ T ∣ = □ T +elΩ T .∣_∣ = □ T elΩ T .is-tr = squash ``` @@ -147,20 +138,40 @@ elΩ T .is-tr = squash □-elim pprop go (squash x y i) = is-prop→pathp (λ i → pprop (squash x y i)) (□-elim pprop go x) (□-elim pprop go y) i +□-elim! + : ∀ {ℓ ℓ'} {A : Type ℓ} {P : □ A → Type ℓ'} ⦃ _ : ∀ {x} → H-Level (P x) 1 ⦄ + → (∀ x → P (inc x)) + → ∀ x → P x +□-elim! = □-elim (λ _ → hlevel 1) + +□-rec! + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + → ⦃ _ : H-Level B 1 ⦄ + → (A → B) → □ A → B +□-rec! = □-rec (hlevel 1) + +□-out : ∀ {ℓ} {A : Type ℓ} → is-prop A → □ A → A +□-out ap = □-rec ap (λ x → x) + +out! : ∀ {ℓ} {A : Type ℓ} + → ⦃ _ : H-Level A 1 ⦄ + → □ A → A +out! = □-rec! λ x → x + □-rec-set : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + → is-set B → (f : A → B) → (∀ x y → f x ≡ f y) - → is-set B → □ A → B -□-rec-set f f-const B-set a = +□-rec-set B-set f f-const a = fst $ □-elim (λ _ → is-constant→image-is-prop B-set f f-const) (λ a → f a , inc (a , refl)) a □-idempotent : ∀ {ℓ} {A : Type ℓ} → is-prop A → □ A ≃ A -□-idempotent aprop = prop-ext squash aprop (out! {pa = aprop}) inc +□-idempotent aprop = prop-ext squash aprop (□-out aprop) inc □-ap : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} @@ -190,7 +201,7 @@ is-set→locally-small : ∀ {ℓ} {A : Type ℓ} → is-set A → is-identity-system {A = A} (λ x y → □ (x ≡ y)) (λ x → inc refl) -is-set→locally-small a-set .to-path = out! {pa = a-set _ _} +is-set→locally-small a-set .to-path = □-rec (a-set _ _) id is-set→locally-small a-set .to-path-over p = is-prop→pathp (λ _ → squash) _ _ to-is-true @@ -225,23 +236,23 @@ infixr 4 _→Ω_ ```agda ⊤Ω : Ω ∣ ⊤Ω ∣ = ⊤ -⊤Ω .is-tr = hlevel! +⊤Ω .is-tr = hlevel 1 ⊥Ω : Ω ∣ ⊥Ω ∣ = ⊥ -⊥Ω .is-tr = hlevel! +⊥Ω .is-tr = hlevel 1 _∧Ω_ : Ω → Ω → Ω ∣ P ∧Ω Q ∣ = ∣ P ∣ × ∣ Q ∣ -(P ∧Ω Q) .is-tr = hlevel! +(P ∧Ω Q) .is-tr = hlevel 1 _∨Ω_ : Ω → Ω → Ω ∣ P ∨Ω Q ∣ = ∥ ∣ P ∣ ⊎ ∣ Q ∣ ∥ -(P ∨Ω Q) .is-tr = hlevel! +(P ∨Ω Q) .is-tr = hlevel 1 _→Ω_ : Ω → Ω → Ω ∣ P →Ω Q ∣ = ∣ P ∣ → ∣ Q ∣ -(P →Ω Q) .is-tr = hlevel! +(P →Ω Q) .is-tr = hlevel 1 ¬Ω_ : Ω → Ω ¬Ω P = P →Ω ⊥Ω diff --git a/src/Algebra/Group.lagda.md b/src/Algebra/Group.lagda.md index 106071979..7b99944d9 100644 --- a/src/Algebra/Group.lagda.md +++ b/src/Algebra/Group.lagda.md @@ -93,7 +93,7 @@ give the unit, both on the left and on the right: { identity = unit ; _⋆_ = _*_ ; has-is-monoid = has-is-monoid } open Cat.Reasoning (B (underlying-monoid .snd)) - hiding (id ; assoc ; idl ; idr ; invr ; invl ; to ; from ; inverses ; _∘_ ; module HLevel-instance) + hiding (id ; assoc ; idl ; idr ; invr ; invl ; to ; from ; inverses ; _∘_) public ``` --> @@ -329,7 +329,7 @@ assumption), and `being an equivalence is a proposition`{.Agdaa ident=is-equiv-is-prop}. ```agda - group-str .group-is-set = hlevel! + group-str .group-is-set = hlevel 2 ``` The associativity and identity laws hold definitionally. diff --git a/src/Algebra/Group/Ab/Abelianisation.lagda.md b/src/Algebra/Group/Ab/Abelianisation.lagda.md index c90bbd1dc..55fb284c0 100644 --- a/src/Algebra/Group/Ab/Abelianisation.lagda.md +++ b/src/Algebra/Group/Ab/Abelianisation.lagda.md @@ -220,7 +220,7 @@ make-free-abelian {ℓ} = go where f # a H.* f # (c G.⋆ b) ≡˘⟨ pres-⋆ _ _ ⟩ f # (a G.⋆ (c G.⋆ b)) ∎ go .universal f .preserves .is-group-hom.pres-⋆ = - Coeq-elim-prop₂ (λ _ _ → hlevel!) λ _ _ → f .preserves .is-group-hom.pres-⋆ _ _ + Coeq-elim-prop₂ (λ _ _ → hlevel 1) λ _ _ → f .preserves .is-group-hom.pres-⋆ _ _ go .commutes f = trivial! go .unique p = ext (p #ₚ_) ``` diff --git a/src/Algebra/Group/Ab/Tensor.lagda.md b/src/Algebra/Group/Ab/Tensor.lagda.md index 61491c787..37efe3cf2 100644 --- a/src/Algebra/Group/Ab/Tensor.lagda.md +++ b/src/Algebra/Group/Ab/Tensor.lagda.md @@ -94,12 +94,10 @@ module _ {A : Abelian-group ℓ} {B : Abelian-group ℓ'} {C : Abelian-group ℓ q i .pres-*r x y z = is-prop→pathp (λ i → C.has-is-set (p x (y B.* z) i) (p x y i C.* p x z i)) (ba .pres-*r x y z) (bb .pres-*r x y z) i - Extensional-bilinear : ∀ {ℓr} ⦃ ef : Extensional (⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟) ℓr ⦄ → Extensional (Bilinear A B C) ℓr - Extensional-bilinear ⦃ ef ⦄ = injection→extensional! (λ h → Bilinear-path (λ x y → h # x # y)) ef - instance - extensionality-bilinear : Extensionality (Bilinear A B C) - extensionality-bilinear = record { lemma = quote Extensional-bilinear } + Extensional-bilinear + : ∀ {ℓr} ⦃ ef : Extensional (⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟) ℓr ⦄ → Extensional (Bilinear A B C) ℓr + Extensional-bilinear ⦃ ef ⦄ = injection→extensional! (λ h → Bilinear-path (λ x y → h # x # y)) ef module _ {ℓ} (A B C : Abelian-group ℓ) where ``` @@ -314,6 +312,16 @@ an equivalence requires appealing to an induction principle of module Bilinear≃Hom = Equiv Bilinear≃Hom module Hom≃Bilinear = Equiv Hom≃Bilinear + +module _ {ℓ} {A B C : Abelian-group ℓ} where instance + Extensional-tensor-hom + : ∀ {ℓr} ⦃ ef : Extensional (⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟) ℓr ⦄ → Extensional (Ab.Hom (A ⊗ B) C) ℓr + Extensional-tensor-hom ⦃ ef ⦄ = + injection→extensional! + {f = λ f x y → f .hom (x , y)} + (λ {x} p → Hom≃Bilinear.injective _ _ _ (ext (subst (ef .Pathᵉ _) p (ef .reflᵉ _)))) + auto + {-# OVERLAPS Extensional-tensor-hom #-} ``` --> @@ -342,8 +350,8 @@ Ab-tensor-functor .F₁ (f , g) = from-bilinear-map _ _ _ bilin where bilin .Bilinear.map x y = f # x , g # y bilin .Bilinear.pres-*l x y z = ap (_, g # z) (f .preserves .is-group-hom.pres-⋆ _ _) ∙ t-pres-*l bilin .Bilinear.pres-*r x y z = ap (f # x ,_) (g .preserves .is-group-hom.pres-⋆ _ _) ∙ t-pres-*r -Ab-tensor-functor .F-id = Hom≃Bilinear.injective _ _ _ trivial! -Ab-tensor-functor .F-∘ f g = Hom≃Bilinear.injective _ _ _ trivial! +Ab-tensor-functor .F-id = trivial! +Ab-tensor-functor .F-∘ f g = trivial! Tensor⊣Hom : (A : Abelian-group ℓ) → Bifunctor.Left Ab-tensor-functor A ⊣ Bifunctor.Right Ab-hom-functor A Tensor⊣Hom A = hom-iso→adjoints to to-eqv nat where diff --git a/src/Algebra/Group/Action.lagda.md b/src/Algebra/Group/Action.lagda.md index 589d2b182..983121d93 100644 --- a/src/Algebra/Group/Action.lagda.md +++ b/src/Algebra/Group/Action.lagda.md @@ -81,7 +81,7 @@ module _ {o ℓ} (C : Precategory o ℓ) where Aut : C.Ob → Group _ Aut X = to-group mg where mg : make-group (X C.≅ X) - mg .make-group.group-is-set = C.≅-is-set + mg .make-group.group-is-set = hlevel 2 mg .make-group.unit = C.id-iso mg .make-group.mul g f = g C.∘Iso f mg .make-group.inv = C._Iso⁻¹ diff --git a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md b/src/Algebra/Group/Cat/FinitelyComplete.lagda.md index 79ed48fc6..f80726dd4 100644 --- a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md +++ b/src/Algebra/Group/Cat/FinitelyComplete.lagda.md @@ -105,7 +105,7 @@ Direct-product (G , Gg) (H , Hg) = to-group G×Hg where module H = Group-on Hg G×Hg : make-group (∣ G ∣ × ∣ H ∣) - G×Hg .make-group.group-is-set = hlevel! + G×Hg .make-group.group-is-set = hlevel 2 G×Hg .make-group.unit = G.unit , H.unit G×Hg .make-group.mul (a , x) (b , y) = a G.⋆ b , x H.⋆ y G×Hg .make-group.inv (a , x) = a G.⁻¹ , x H.⁻¹ diff --git a/src/Algebra/Group/Concrete.lagda.md b/src/Algebra/Group/Concrete.lagda.md index 6b8ec880f..a23eb6cbd 100644 --- a/src/Algebra/Group/Concrete.lagda.md +++ b/src/Algebra/Group/Concrete.lagda.md @@ -136,7 +136,7 @@ ConcreteGroups-Hom-set : (G : ConcreteGroup ℓ) (H : ConcreteGroup ℓ') → is-set (B G →∙ B H) ConcreteGroups-Hom-set G H (f , ptf) (g , ptg) p q = - Σ-set-square hlevel! (funext-square (B-elim-contr G square)) + Σ-set-square (λ _ → hlevel 2) (funext-square (B-elim-contr G square)) where open ConcreteGroup H using (H-Level-B) square : is-contr ((λ j → p j .fst (pt G)) ≡ (λ j → q j .fst (pt G))) diff --git a/src/Algebra/Group/Free.lagda.md b/src/Algebra/Group/Free.lagda.md index f56466010..4784b88c1 100644 --- a/src/Algebra/Group/Free.lagda.md +++ b/src/Algebra/Group/Free.lagda.md @@ -175,7 +175,7 @@ make-free-group .Ml.unit _ = inc make-free-group .Ml.universal f = fold-free-group f make-free-group .Ml.commutes f = refl make-free-group .Ml.unique {y = y} {g = g} p = - ext $ Free-elim-prop _ (λ _ → hlevel!) + ext $ Free-elim-prop _ (λ _ → hlevel 1) (p $ₚ_) (λ a p b q → ap₂ y._⋆_ p q ∙ sym (g .preserves .is-group-hom.pres-⋆ _ _)) (λ a p → ap y.inverse p ∙ sym (is-group-hom.pres-inv (g .preserves))) diff --git a/src/Algebra/Group/Homotopy/BAut.lagda.md b/src/Algebra/Group/Homotopy/BAut.lagda.md index 80987ecc5..6a9df4013 100644 --- a/src/Algebra/Group/Homotopy/BAut.lagda.md +++ b/src/Algebra/Group/Homotopy/BAut.lagda.md @@ -37,7 +37,7 @@ of its interesting information is in its (higher) path spaces: ```agda connected : (x : BAut) → ∥ x ≡ base ∥ connected (b , x) = - ∥-∥-elim {P = λ x → ∥ (b , x) ≡ base ∥} (λ _ → squash) (λ e → inc (p _ _)) x + ∥-∥-elim! {P = λ x → ∥ (b , x) ≡ base ∥} (λ e → inc (p _ _)) x where p : ∀ b e → (b , inc e) ≡ base p _ = EquivJ (λ B e → (B , inc e) ≡ base) refl diff --git a/src/Algebra/Group/Notation.agda b/src/Algebra/Group/Notation.agda index 000f10009..3efb99f52 100644 --- a/src/Algebra/Group/Notation.agda +++ b/src/Algebra/Group/Notation.agda @@ -18,6 +18,7 @@ module Additive-notation = Group-on renaming ; inv-comm to neg-comm ; inv-unit to neg-0 ) + hiding (magma-hlevel) module Multiplicative-notation = Group-on renaming ( _⋆_ to infixl 20 _*_ @@ -30,6 +31,7 @@ module Multiplicative-notation = Group-on renaming ; idr to *-idr ; inv-unit to inv-1 ) + hiding (magma-hlevel) instance Abelian-group-on→Group-on diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md index fbe90b768..cd018fcbe 100644 --- a/src/Algebra/Group/Subgroup.lagda.md +++ b/src/Algebra/Group/Subgroup.lagda.md @@ -1,6 +1,5 @@ diff --git a/src/Algebra/Ring/Module/Action.lagda.md b/src/Algebra/Ring/Module/Action.lagda.md index e3501525b..952e7f871 100644 --- a/src/Algebra/Ring/Module/Action.lagda.md +++ b/src/Algebra/Ring/Module/Action.lagda.md @@ -101,13 +101,13 @@ and ring morphisms $R \to [G,G]$ into the [endomorphism ring] of $G$. Action→Hom G act .hom r .hom = act .Ring-action._⋆_ r Action→Hom G act .hom r .preserves .is-group-hom.pres-⋆ x y = act .Ring-action.⋆-distribl r x y - Action→Hom G act .preserves .is-ring-hom.pres-id = Homomorphism-path λ i → act .Ring-action.⋆-id _ - Action→Hom G act .preserves .is-ring-hom.pres-+ x y = Homomorphism-path λ i → act .Ring-action.⋆-distribr _ _ _ - Action→Hom G act .preserves .is-ring-hom.pres-* r s = Homomorphism-path λ x → sym (act .Ring-action.⋆-assoc _ _ _) + Action→Hom G act .preserves .is-ring-hom.pres-id = ext λ x → act .Ring-action.⋆-id _ + Action→Hom G act .preserves .is-ring-hom.pres-+ x y = ext λ x → act .Ring-action.⋆-distribr _ _ _ + Action→Hom G act .preserves .is-ring-hom.pres-* r s = ext λ x → sym (act .Ring-action.⋆-assoc _ _ _) Action≃Hom : (G : Abelian-group ℓ) → Ring-action (G .snd) ≃ Rings.Hom R (Endo Ab-ab-category G) - Action≃Hom G = Iso→Equiv $ Action→Hom G , iso (Hom→Action G) - (λ x → trivial!) (λ x → refl) + Action≃Hom G = Iso→Equiv $ Action→Hom G + , iso (Hom→Action G) (λ x → trivial!) (λ x → refl) ``` diff --git a/src/Algebra/Ring/Module/Free.lagda.md b/src/Algebra/Ring/Module/Free.lagda.md index 1fa887ab8..fe329fd74 100644 --- a/src/Algebra/Ring/Module/Free.lagda.md +++ b/src/Algebra/Ring/Module/Free.lagda.md @@ -249,34 +249,15 @@ equal-on-basis M {f} {g} p = module g = Linear-map g module M = Module-on (M .snd) -Extensional-linear-map-free - : ∀ {ℓb ℓg ℓr} {T : Type ℓb} {M : Module R ℓg} - → ⦃ ext : Extensional (T → ⌞ M ⌟) ℓr ⦄ - → Extensional (Linear-map (Free-Mod T) M) ℓr -Extensional-linear-map-free {M = M} ⦃ ext ⦄ = - injection→extensional! {f = λ m x → m .map (inc x)} (λ p → equal-on-basis M (happly p)) ext - -Extensional-hom-free - : ∀ {ℓ' ℓr} {T : Type ℓ'} {M : Module R (ℓ ⊔ ℓ')} - → ⦃ ext : Extensional (T → ⌞ M ⌟) ℓr ⦄ - → Extensional (R-Mod.Hom (Free-Mod T) M) ℓr -Extensional-hom-free {M = M} ⦃ ef ⦄ = - injection→extensional! {f = λ m x → m # (inc x)} - (λ {f} {g} p → - let it = equal-on-basis M {hom→linear-map f} {hom→linear-map g} (happly p) - in ext (happly (ap map it))) - ef - instance - extensionality-linear-map-free - : ∀ {ℓb ℓg} {T : Type ℓb} {M : Module R ℓg} - → Extensionality (Linear-map (Free-Mod T) M) - extensionality-linear-map-free = record { lemma = quote Extensional-linear-map-free } - - extensionality-hom-free - : ∀ {ℓ'} {T : Type ℓ'} {M : Module R (ℓ ⊔ ℓ')} - → Extensionality (R-Mod.Hom {ℓm = ℓ ⊔ ℓ'} (Free-Mod T) M) - extensionality-hom-free = record { lemma = quote Extensional-hom-free } + Extensional-linear-map-free + : ∀ {ℓb ℓg ℓr} {T : Type ℓb} {M : Module R ℓg} + → ⦃ ext : Extensional (T → ⌞ M ⌟) ℓr ⦄ + → Extensional (Linear-map (Free-Mod T) M) ℓr + Extensional-linear-map-free {M = M} ⦃ ext ⦄ = + injection→extensional! {f = λ m x → m .map (inc x)} (λ p → equal-on-basis M (happly p)) ext + + {-# OVERLAPS Extensional-linear-map-free #-} ``` --> diff --git a/src/Cat/Allegory/Base.lagda.md b/src/Cat/Allegory/Base.lagda.md index 3a50d7381..9ffd23693 100644 --- a/src/Cat/Allegory/Base.lagda.md +++ b/src/Cat/Allegory/Base.lagda.md @@ -237,7 +237,7 @@ The dual is given by inverting the order of arguments to $R$, and the modular law is given by some pair-shuffling. ```agda -Rel ℓ ._∩_ R S x y = el (∣ R x y ∣ × ∣ S x y ∣) hlevel! +Rel ℓ ._∩_ R S x y = el (∣ R x y ∣ × ∣ S x y ∣) (hlevel 1) Rel ℓ ._† R x y = R y x Rel ℓ .modular R S T x y (α , β) = □-rec! (λ { (z , r , s) → inc (z , (r , inc (y , β , s)) , s) }) α @@ -261,7 +261,7 @@ Rel ℓ .cat .assoc T S R = ext λ x y → Ω-ua (□-rec! λ { (a , b , w) → □-rec! (λ { (c , d , x) → inc (c , inc (a , b , d) , x) }) w }) -Rel ℓ .≤-thin = hlevel! +Rel ℓ .≤-thin = hlevel 1 Rel ℓ .≤-refl x y w = w Rel ℓ .≤-trans x y p q z = y p q (x p q z) Rel ℓ .≤-antisym p q = ext λ x y → Ω-ua (p x y) (q x y) diff --git a/src/Cat/Allegory/Instances/Mat.lagda.md b/src/Cat/Allegory/Instances/Mat.lagda.md index 13784507a..537fa3925 100644 --- a/src/Cat/Allegory/Instances/Mat.lagda.md +++ b/src/Cat/Allegory/Instances/Mat.lagda.md @@ -52,7 +52,7 @@ that this is, indeed, a category: Mat : Precategory (lsuc o) o Mat .Ob = Set o Mat .Hom A B = ∣ A ∣ → ∣ B ∣ → ⌞ L ⌟ - Mat .Hom-set x y = hlevel! + Mat .Hom-set x y = hlevel 2 Mat .id x y = ⋃ λ (_ : x ≡ y) → top Mat ._∘_ {y = y} M N i j = ⋃ λ k → N i k ∩ M k j @@ -90,7 +90,7 @@ a bit more algebra is the verification of the modular law: Matrices .A.cat = Mat Matrices .A._≤_ M N = ∀ i j → M i j ≤ N i j - Matrices .A.≤-thin = hlevel! + Matrices .A.≤-thin = hlevel 1 Matrices .A.≤-refl i j = ≤-refl Matrices .A.≤-trans p q i j = ≤-trans (p i j) (q i j) Matrices .A.≤-antisym p q = ext λ i j → ≤-antisym (p i j) (q i j) diff --git a/src/Cat/Allegory/Reasoning.lagda.md b/src/Cat/Allegory/Reasoning.lagda.md index 1600cce67..e6b6203d1 100644 --- a/src/Cat/Allegory/Reasoning.lagda.md +++ b/src/Cat/Allegory/Reasoning.lagda.md @@ -15,7 +15,7 @@ module Cat.Allegory.Reasoning {o ℓ ℓ'} (A : Allegory o ℓ ℓ') where ```agda open Allegory A public open Cat.Reasoning (A .Allegory.cat) - hiding (module HLevel-instance ; Ob ; Hom ; Hom-set ; id ; idl ; idr ; assoc ; _∘_) + hiding (Ob ; Hom ; Hom-set ; id ; idl ; idr ; assoc ; _∘_) public ``` diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md index 6ad40d081..6ab3b3d0a 100644 --- a/src/Cat/Base.lagda.md +++ b/src/Cat/Base.lagda.md @@ -1,10 +1,12 @@ @@ -492,6 +502,8 @@ module _ where infixr 30 _F∘_ infix 20 _=>_ +unquoteDecl H-Level-Nat = declare-record-hlevel 2 H-Level-Nat (quote _=>_) + module _ {o₁ h₁ o₂ h₂} {C : Precategory o₁ h₁} {D : Precategory o₂ h₂} @@ -515,21 +527,10 @@ natural transformations and a certain $\Sigma$ type; This type can then be shown to be a set using the standard `hlevel`{.Agda} machinery. ```agda - private unquoteDecl eqv = declare-record-iso eqv (quote _=>_) opaque Nat-is-set : is-set (F => G) - Nat-is-set = Iso→is-hlevel 2 eqv (hlevel 2) where - open C.HLevel-instance - open D.HLevel-instance -``` - - Another fundamental lemma is that equality of natural transformations depends only on equality of the family of morphisms, since being natural @@ -580,49 +581,16 @@ instance → Funlike (F => G) ⌞ C ⌟ (λ x → D .Precategory.Hom (F # x) (G # x)) Funlike-natural-transformation = record { _#_ = _=>_.η } -{- -Set-up for using natural transformations with the extensionality tactic; -See the docs in 1Lab.Extensionality for a more detailed explanation of -how it works. - -This function is the actual worker which computes the preferred -identity system for natural transformations. Its type asks for - - ∀ x → Extensional (D.Hom (F # x) (G # x)) - -instead of the more generic ∀ x y → Extensional (D.Hom x y) so that -any specific *instances* for D.Hom involving the object parts of F and G -have a chance to fire. E.g. if G is the product functor on Sets then -(x → y) will only match the funext instance but (x → G # y) will -match funext *and* product extensionality. --} -Extensional-natural-transformation - : ∀ {o ℓ o' ℓ' ℓr} {C : Precategory o ℓ} {D : Precategory o' ℓ'} - → {F G : Functor C D} - → {@(tactic extensionalᶠ {A = ⌞ C ⌟ → Type _} - (λ x → D .Hom (F # x) (G # x))) - sa : ∀ x → Extensional (D .Hom (F # x) (G # x)) ℓr} - → Extensional (F => G) (o ⊔ ℓr) -Extensional-natural-transformation {sa = sa} .Pathᵉ f g = ∀ i → Pathᵉ (sa i) (f .η i) (g .η i) -Extensional-natural-transformation {sa = sa} .reflᵉ x i = reflᵉ (sa i) (x .η i) -Extensional-natural-transformation {sa = sa} .idsᵉ .to-path x = Nat-pathp _ _ λ i → - sa _ .idsᵉ .to-path (x i) -Extensional-natural-transformation {D = D} {sa = sa} .idsᵉ .to-path-over h = - is-prop→pathp - (λ i → Π-is-hlevel 1 - (λ _ → Equiv→is-hlevel 1 (identity-system-gives-path (sa _ .idsᵉ)) (D .Hom-set _ _ _ _))) - _ _ - --- Actually define the loop-breaker instance which tells the --- extensionality tactic what lemma to use for a type of natural --- transformations. - -instance - extensionality-natural-transformation - : ∀ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} - {F G : Functor C D} - → Extensionality (F => G) - extensionality-natural-transformation = record - { lemma = quote Extensional-natural-transformation } + Extensional-natural-transformation + : ∀ {o ℓ o' ℓ' ℓr} {C : Precategory o ℓ} {D : Precategory o' ℓ'} + → {F G : Functor C D} + → ⦃ sa : {x : ⌞ C ⌟} → Extensional (D .Hom (F # x) (G # x)) ℓr ⦄ + → Extensional (F => G) (o ⊔ ℓr) + Extensional-natural-transformation ⦃ sa ⦄ .Pathᵉ f g = ∀ i → Pathᵉ sa (f .η i) (g .η i) + Extensional-natural-transformation ⦃ sa ⦄ .reflᵉ x i = reflᵉ sa (x .η i) + Extensional-natural-transformation ⦃ sa ⦄ .idsᵉ .to-path x = Nat-pathp _ _ λ i → + sa .idsᵉ .to-path (x i) + Extensional-natural-transformation {D = D} ⦃ sa ⦄ .idsᵉ .to-path-over h = + is-prop→pathp (λ i → Π-is-hlevel 1 λ _ → Pathᵉ-is-hlevel 1 sa (hlevel 2)) _ _ ``` --> diff --git a/src/Cat/Bi/Diagram/Monad/Spans.lagda.md b/src/Cat/Bi/Diagram/Monad/Spans.lagda.md index a74ad7194..77168e4df 100644 --- a/src/Cat/Bi/Diagram/Monad/Spans.lagda.md +++ b/src/Cat/Bi/Diagram/Monad/Spans.lagda.md @@ -1,6 +1,6 @@ diff --git a/src/Cat/Diagram/Colimit/Cocone.lagda.md b/src/Cat/Diagram/Colimit/Cocone.lagda.md index c1df591cc..cfbb264eb 100644 --- a/src/Cat/Diagram/Colimit/Cocone.lagda.md +++ b/src/Cat/Diagram/Colimit/Cocone.lagda.md @@ -123,7 +123,7 @@ category, it's immediate that they form a category. cat .idr f = Cocone-hom-path (C.idr (f .hom)) cat .idl f = Cocone-hom-path (C.idl (f .hom)) cat .assoc f g h = Cocone-hom-path (C.assoc (f .hom) (g .hom) (h .hom)) - cat .Hom-set x y = Iso→is-hlevel 2 eqv hlevel! + cat .Hom-set x y = Iso→is-hlevel! 2 eqv ``` --> diff --git a/src/Cat/Diagram/Initial.lagda.md b/src/Cat/Diagram/Initial.lagda.md index 7e4f0e254..b14a40ed0 100644 --- a/src/Cat/Diagram/Initial.lagda.md +++ b/src/Cat/Diagram/Initial.lagda.md @@ -115,5 +115,5 @@ Strictness is a property of, not structure on, an initial object. ```agda is-strict-initial-is-prop : ∀ i → is-prop (is-strict-initial i) -is-strict-initial-is-prop i = hlevel! +is-strict-initial-is-prop i = hlevel 1 ``` diff --git a/src/Cat/Diagram/Limit/Cone.lagda.md b/src/Cat/Diagram/Limit/Cone.lagda.md index 686a37dce..87f0dddaf 100644 --- a/src/Cat/Diagram/Limit/Cone.lagda.md +++ b/src/Cat/Diagram/Limit/Cone.lagda.md @@ -159,7 +159,7 @@ again preserve _all_ the commutativities. @@ -281,8 +275,7 @@ the identity and associativity laws from its underlying category. Eilenberg-Moore .idr f = ext (C.idr _) Eilenberg-Moore .idl f = ext (C.idl _) Eilenberg-Moore .assoc f g h = ext (C.assoc _ _ _) - Eilenberg-Moore .Hom-set X Y = Iso→is-hlevel 2 eqv (hlevel 2) - where open C.HLevel-instance + Eilenberg-Moore .Hom-set X Y = hlevel 2 ``` diff --git a/src/Cat/Diagram/Monad/Relative.lagda.md b/src/Cat/Diagram/Monad/Relative.lagda.md index 0590ec1d3..f5fcd875d 100644 --- a/src/Cat/Diagram/Monad/Relative.lagda.md +++ b/src/Cat/Diagram/Monad/Relative.lagda.md @@ -387,12 +387,9 @@ are closed under identities and composites. All of the equations are trivial. ```agda - Relative-Eilenberg-Moore .Hom[_]-set = hlevel! - Relative-Eilenberg-Moore .idr' _ = - is-prop→pathp (λ i → Π-is-hlevel' 1 λ _ → Π-is-hlevel 1 λ _ → C.Hom-set _ _ _ _) _ _ - Relative-Eilenberg-Moore .idl' _ = - is-prop→pathp (λ i → Π-is-hlevel' 1 λ _ → Π-is-hlevel 1 λ _ → C.Hom-set _ _ _ _) _ _ - Relative-Eilenberg-Moore .assoc' _ _ _ = - is-prop→pathp (λ i → Π-is-hlevel' 1 λ _ → Π-is-hlevel 1 λ _ → C.Hom-set _ _ _ _) _ _ + Relative-Eilenberg-Moore .Hom[_]-set _ _ _ = hlevel 2 + Relative-Eilenberg-Moore .idr' _ = prop! + Relative-Eilenberg-Moore .idl' _ = prop! + Relative-Eilenberg-Moore .assoc' _ _ _ = prop! ``` diff --git a/src/Cat/Displayed/Base.lagda.md b/src/Cat/Displayed/Base.lagda.md index 6c88ff16e..98b2c80ca 100644 --- a/src/Cat/Displayed/Base.lagda.md +++ b/src/Cat/Displayed/Base.lagda.md @@ -1,5 +1,8 @@ diff --git a/src/Cat/Displayed/Cartesian/Discrete.lagda.md b/src/Cat/Displayed/Cartesian/Discrete.lagda.md index 4244427fa..4c37fe499 100644 --- a/src/Cat/Displayed/Cartesian/Discrete.lagda.md +++ b/src/Cat/Displayed/Cartesian/Discrete.lagda.md @@ -356,6 +356,5 @@ it survives automatically. ```agda private unquoteDecl eqv = declare-record-iso eqv (quote Discrete-fibration) hl : ∀ x → is-prop _ - hl x = Equiv→is-hlevel 1 (Iso→Equiv eqv) $ - ×-is-hlevel 1 (Π-is-hlevel 1 λ _ → is-hlevel-is-prop 2) hlevel! + hl x = Iso→is-hlevel! 1 eqv ``` diff --git a/src/Cat/Displayed/Cartesian/Street.lagda.md b/src/Cat/Displayed/Cartesian/Street.lagda.md index 390e0d62e..52a045c8b 100644 --- a/src/Cat/Displayed/Cartesian/Street.lagda.md +++ b/src/Cat/Displayed/Cartesian/Street.lagda.md @@ -37,8 +37,6 @@ module _ {o ℓ o' ℓ'} {E : Precategory o ℓ} {B : Precategory o' ℓ'} (P : module E = Cat.Reasoning E module B = Cat.Reasoning B module P = Functor P - open B.HLevel-instance - open E.HLevel-instance ``` --> @@ -96,12 +94,9 @@ property (rather than data). functor→displayed .id' = E.id , B.elimr P.F-id ∙ B.introl refl functor→displayed ._∘'_ (f , φ) (g , ψ) = f E.∘ g , ap₂ B._∘_ refl (P.F-∘ f g) ∙ B.pulll φ ∙ B.pullr ψ ∙ B.assoc _ _ _ - functor→displayed .idr' f' = Σ-pathp (E.idr _) $ - is-set→squarep (λ _ _ → hlevel 2) _ _ _ _ - functor→displayed .idl' f' = Σ-pathp (E.idl _) $ - is-set→squarep (λ _ _ → hlevel 2) _ _ _ _ - functor→displayed .assoc' f' g' h' = Σ-pathp (E.assoc _ _ _) $ - is-set→squarep (λ _ _ → hlevel 2) _ _ _ _ + functor→displayed .idr' f' = Σ-prop-pathp! (E.idr _) + functor→displayed .idl' f' = Σ-prop-pathp! (E.idl _) + functor→displayed .assoc' f' g' h' = Σ-prop-pathp! (E.assoc _ _ _) ``` We call a functor that gives rise to a Cartesian fibration through this diff --git a/src/Cat/Displayed/Doctrine/Frame.lagda.md b/src/Cat/Displayed/Doctrine/Frame.lagda.md index 217fe4aee..f5dba77c8 100644 --- a/src/Cat/Displayed/Doctrine/Frame.lagda.md +++ b/src/Cat/Displayed/Doctrine/Frame.lagda.md @@ -52,10 +52,6 @@ Indexed-frame {o = o} {ℓ} {κ} F = idx where @@ -73,7 +69,7 @@ the equivalence $(x \le_f y) \equiv (x \le_{\id} f^*y)$ of maps into a disp : Displayed (Sets κ) (o ⊔ κ) (ℓ ⊔ κ) disp .Ob[_] S = ⌞ S ⌟ → ⌞ F ⌟ disp .Hom[_] f g h = ∀ x → g x F.≤ h (f x) - disp .Hom[_]-set f g h = is-prop→is-set isp + disp .Hom[_]-set f g h = hlevel 2 disp .id' x = F.≤-refl disp ._∘'_ p q x = F.≤-trans (q x) (p _) @@ -81,9 +77,9 @@ the equivalence $(x \le_f y) \equiv (x \le_{\id} f^*y)$ of maps into a @@ -102,16 +98,16 @@ function which is constantly the top element. ```agda term : ∀ S → Terminal (Fibre disp S) term S .top _ = F.top - term S .has⊤ f = is-prop∙→is-contr isp (λ i → F.!) + term S .has⊤ f = is-prop∙→is-contr (hlevel 1) (λ i → F.!) ``` ## As a fibration @@ -127,8 +123,8 @@ $gf : X \to F$. cart .has-lift f g .lifting i = F.≤-refl cart .has-lift f g .cartesian = record { universal = λ m p x → p x - ; commutes = λ m h' → isp _ _ - ; unique = λ m p → isp _ _ + ; commutes = λ m h' → prop! + ; unique = λ m p → prop! } ``` @@ -188,8 +184,8 @@ a calculation: g x F.≤⟨ h' x ⟩ u' (m (f x)) F.=⟨ ap u' (ap m p) ⟩ u' (m i) F.≤∎ }) b - lifted .cocartesian .commutes m h = isp _ _ - lifted .cocartesian .unique m x = isp _ _ + lifted .cocartesian .commutes m h = prop! + lifted .cocartesian .unique m x = prop! ``` ## Putting it together @@ -201,9 +197,9 @@ We're ready to put everything together. By construction, we have a idx : Regular-hyperdoctrine (Sets κ) _ _ idx .ℙ = disp idx .has-is-set x = Π-is-hlevel 2 λ _ → F.Ob-is-set - idx .has-is-thin f g = isp + idx .has-is-thin f g = hlevel 1 idx .has-univalence S = set-identity-system - (λ _ _ _ _ → Cat.≅-path (Fibre disp _) (isp _ _)) + (λ _ _ _ _ → Cat.≅-path (Fibre disp _) prop!) λ im → funextP λ i → F.≤-antisym (Cat.to im i) (Cat.from im i) ``` diff --git a/src/Cat/Displayed/GenericObject.lagda.md b/src/Cat/Displayed/GenericObject.lagda.md index d3069e155..a7568a128 100644 --- a/src/Cat/Displayed/GenericObject.lagda.md +++ b/src/Cat/Displayed/GenericObject.lagda.md @@ -180,7 +180,7 @@ is-skeletal-generic-object {t} {t'} gobj = is-skeletal-generic-object-is-prop : ∀ {t} {t' : Ob[ t ]} {gobj : Generic-object t'} → is-prop (is-skeletal-generic-object gobj) -is-skeletal-generic-object-is-prop = hlevel! +is-skeletal-generic-object-is-prop = hlevel 1 ``` --> @@ -235,14 +235,6 @@ gaunt-generic-object→skeletal-generic-object = diff --git a/src/Cat/Displayed/Instances/Elements.lagda.md b/src/Cat/Displayed/Instances/Elements.lagda.md index 28d9e89d9..458005586 100644 --- a/src/Cat/Displayed/Instances/Elements.lagda.md +++ b/src/Cat/Displayed/Instances/Elements.lagda.md @@ -43,7 +43,7 @@ elements, as we obtain the more traditional definition by taking the ∫ : Displayed B s s ∫ .Displayed.Ob[_] X = P ʻ X ∫ .Displayed.Hom[_] f P[X] P[Y] = P.₁ f P[Y] ≡ P[X] -∫ .Displayed.Hom[_]-set _ _ _ = hlevel! +∫ .Displayed.Hom[_]-set _ _ _ = hlevel 2 ∫ .Displayed.id' = happly P.F-id _ ∫ .Displayed._∘'_ {x = x} {y} {z} {f} {g} p q = pf where abstract pf : P.₁ (f ∘ g) z ≡ x diff --git a/src/Cat/Displayed/Instances/Family.lagda.md b/src/Cat/Displayed/Instances/Family.lagda.md index 8300c50fd..0f1af00e5 100644 --- a/src/Cat/Displayed/Instances/Family.lagda.md +++ b/src/Cat/Displayed/Instances/Family.lagda.md @@ -200,7 +200,7 @@ Family-generic-object→Strict-equiv → Σ[ Strict ∈ Precategory h h ] (is-set ⌞ Strict ⌟ × Equivalence Strict C) Family-generic-object→Strict-equiv small = - Strict , hlevel! , eqv module Family-generic-object-strict where + Strict , hlevel 2 , eqv module Family-generic-object-strict where open Globally-small small ``` diff --git a/src/Cat/Displayed/Instances/Identity.lagda.md b/src/Cat/Displayed/Instances/Identity.lagda.md index 85381fea0..0960a9397 100644 --- a/src/Cat/Displayed/Instances/Identity.lagda.md +++ b/src/Cat/Displayed/Instances/Identity.lagda.md @@ -34,7 +34,7 @@ $B$, called the **identity bifibration**. IdD : Displayed B lzero lzero IdD .Ob[_] _ = ⊤ IdD .Hom[_] _ _ _ = ⊤ -IdD .Hom[_]-set _ _ _ = hlevel! +IdD .Hom[_]-set _ _ _ = hlevel 2 IdD .id' = tt IdD ._∘'_ _ _ = tt IdD .idr' _ = refl @@ -47,8 +47,8 @@ discrete as you can get! ```agda IdD-discrete-fibration : Discrete-fibration IdD -IdD-discrete-fibration .Discrete-fibration.fibre-set = hlevel! -IdD-discrete-fibration .Discrete-fibration.lifts _ _ = hlevel! +IdD-discrete-fibration .Discrete-fibration.fibre-set _ = hlevel 2 +IdD-discrete-fibration .Discrete-fibration.lifts _ _ = hlevel 0 ``` Every morphism in the identity fibration is trivially cartesian and diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md index c4c59f252..2a6953527 100644 --- a/src/Cat/Displayed/Instances/Lifting.lagda.md +++ b/src/Cat/Displayed/Instances/Lifting.lagda.md @@ -154,12 +154,7 @@ between $F'(j)$ and $G'(j)$. @@ -318,7 +310,7 @@ module _ Liftings : Displayed Cat[ J , B ] (o' ⊔ ℓ' ⊔ oj ⊔ ℓj) (ℓ' ⊔ oj ⊔ ℓj) Liftings .Displayed.Ob[_] = Lifting E Liftings .Displayed.Hom[_] α F' G' = F' =[ α ]=>l G' - Liftings .Displayed.Hom[_]-set _ _ _ = Nat-lift-is-set + Liftings .Displayed.Hom[_]-set _ _ _ = hlevel 2 Liftings .Displayed.id' = idntl Liftings .Displayed._∘'_ = _∘ntl_ Liftings .Displayed.idr' _ = Nat-lift-pathp (λ _ → idr' _) diff --git a/src/Cat/Displayed/Instances/Opposite.lagda.md b/src/Cat/Displayed/Instances/Opposite.lagda.md index 18232238b..bb9bc15d4 100644 --- a/src/Cat/Displayed/Instances/Opposite.lagda.md +++ b/src/Cat/Displayed/Instances/Opposite.lagda.md @@ -1,6 +1,6 @@ @@ -136,7 +133,7 @@ displayed over $\cB$. Slices : Displayed B (o ⊔ ℓ) ℓ Slices .Ob[_] = /-Obj {C = B} Slices .Hom[_] = Slice-hom -Slices .Hom[_]-set = Slice-is-set +Slices .Hom[_]-set _ _ _ = hlevel 2 Slices .id' = slice-hom id id-comm-sym Slices ._∘'_ {x = x} {y = y} {z = z} {f = f} {g = g} px py = slice-hom (px .to ∘ py .to) $ diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md index ce021077b..3a8d727f0 100644 --- a/src/Cat/Displayed/Instances/Subobjects.lagda.md +++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md @@ -1,6 +1,5 @@ @@ -67,10 +67,6 @@ the bundled morphisms form an hset, and another characterizing the paths between morphisms. ```agda -total-hom-is-set : ∀ (X Y : Total) → is-set (Total-hom X Y) -total-hom-is-set X Y = Iso→is-hlevel 2 eqv $ - Σ-is-hlevel 2 (hlevel 2) (λ a → Hom[ _ ]-set _ _) - total-hom-path : ∀ {X Y : Total} {f g : Total-hom X Y} → (p : f .hom ≡ g .hom) → f .preserves ≡[ p ] g .preserves → f ≡ g total-hom-path p p' i .hom = p i @@ -96,7 +92,7 @@ With all that in place, we can construct the total category! ∫ : Precategory (o ⊔ o') (ℓ ⊔ ℓ') ∫ .Precategory.Ob = Total ∫ .Precategory.Hom = Total-hom -∫ .Precategory.Hom-set = total-hom-is-set +∫ .Precategory.Hom-set _ _ = hlevel 2 ∫ .Precategory.id .hom = id ∫ .Precategory.id .preserves = id' ∫ .Precategory._∘_ f g .hom = f .hom ∘ g .hom diff --git a/src/Cat/Displayed/Univalence.lagda.md b/src/Cat/Displayed/Univalence.lagda.md index bc78aa4fa..0e327696f 100644 --- a/src/Cat/Displayed/Univalence.lagda.md +++ b/src/Cat/Displayed/Univalence.lagda.md @@ -1,6 +1,5 @@ diff --git a/src/Cat/Functor/Subcategory.lagda.md b/src/Cat/Functor/Subcategory.lagda.md index 55723d79c..9012da887 100644 --- a/src/Cat/Functor/Subcategory.lagda.md +++ b/src/Cat/Functor/Subcategory.lagda.md @@ -91,15 +91,12 @@ module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} {S : Subcat C o' ℓ'} where Subcat-hom-pathp {f = f} {g = g} p q r i .witness = is-prop→pathp (λ i → is-hom-prop (r i) (p i .snd) (q i .snd)) (f .witness) (g .witness) i - Extensional-subcat-hom - : ∀ {ℓr x y} ⦃ sa : Extensional (Hom (x .fst) (y .fst)) ℓr ⦄ - → Extensional (Subcat-hom S x y) ℓr - Extensional-subcat-hom ⦃ sa ⦄ = injection→extensional! - (Subcat-hom-pathp refl refl) sa - instance - extensionality-subcat-hom : ∀ {x y} → Extensionality (Subcat-hom S x y) - extensionality-subcat-hom = record { lemma = quote Extensional-subcat-hom } + Extensional-subcat-hom + : ∀ {ℓr x y} ⦃ sa : Extensional (Hom (x .fst) (y .fst)) ℓr ⦄ + → Extensional (Subcat-hom S x y) ℓr + Extensional-subcat-hom ⦃ sa ⦄ = injection→extensional! + (Subcat-hom-pathp refl refl) sa Funlike-Subcat-hom : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y} diff --git a/src/Cat/Functor/WideSubcategory.lagda.md b/src/Cat/Functor/WideSubcategory.lagda.md index 37fbd9949..b0dc91ee6 100644 --- a/src/Cat/Functor/WideSubcategory.lagda.md +++ b/src/Cat/Functor/WideSubcategory.lagda.md @@ -88,25 +88,19 @@ module _ {o h} {C : Precategory o h} where Wide-hom-path {sub = sub} {f = f} {g = g} p i .witness = is-prop→pathp (λ i → sub .P-prop (p i)) (f .witness) (g .witness) i - Extensional-wide-hom - : ∀ {ℓ ℓr} {sub : Wide-subcat C ℓ} {x y : C.Ob} - → ⦃ sa : Extensional (C.Hom x y) ℓr ⦄ - → Extensional (Wide-hom sub x y) ℓr - Extensional-wide-hom ⦃ sa ⦄ = injection→extensional! - Wide-hom-path sa - instance - extensionality-wide-hom - : ∀ {ℓ} {sub : Wide-subcat C ℓ} {x y : C.Ob} → Extensionality (Wide-hom sub x y) - extensionality-wide-hom = record { lemma = quote Extensional-wide-hom } - - Wide-hom-is-set - : {sub : Wide-subcat C ℓ} - → {x y : C.Ob} - → is-set (Wide-hom sub x y) - Wide-hom-is-set {sub = sub} = Iso→is-hlevel 2 eqv $ - Σ-is-hlevel 2 (C.Hom-set _ _) λ f → is-hlevel-suc 1 (sub .P-prop f) - where unquoteDecl eqv = declare-record-iso eqv (quote Wide-hom) + Extensional-wide-hom + : ∀ {ℓ ℓr} {sub : Wide-subcat C ℓ} {x y : C.Ob} + → ⦃ sa : Extensional (C.Hom x y) ℓr ⦄ + → Extensional (Wide-hom sub x y) ℓr + Extensional-wide-hom ⦃ sa ⦄ = injection→extensional! Wide-hom-path sa + + H-Level-Wide-hom + : ∀ {sub : Wide-subcat C ℓ} {x y : C.Ob} {n} + → H-Level (Wide-hom sub x y) (2 + n) + H-Level-Wide-hom {sub = sub} = basic-instance 2 $ Iso→is-hlevel 2 eqv $ + Σ-is-hlevel 2 (C.Hom-set _ _) λ f → is-hlevel-suc 1 (sub .P-prop f) + where unquoteDecl eqv = declare-record-iso eqv (quote Wide-hom) ``` --> @@ -116,7 +110,7 @@ We can then use this data to construct a category. Wide : Wide-subcat C ℓ → Precategory o (h ⊔ ℓ) Wide sub .Ob = C.Ob Wide sub .Hom = Wide-hom sub - Wide sub .Hom-set _ _ = Wide-hom-is-set + Wide sub .Hom-set _ _ = hlevel 2 Wide sub .id .hom = C.id Wide sub .id .witness = sub .P-id diff --git a/src/Cat/Gaunt.lagda.md b/src/Cat/Gaunt.lagda.md index 90c7605e0..b4adbcb4b 100644 --- a/src/Cat/Gaunt.lagda.md +++ b/src/Cat/Gaunt.lagda.md @@ -38,19 +38,7 @@ record is-gaunt {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ ℓ) where @@ -62,7 +50,7 @@ module _ {o ℓ} {C : Precategory o ℓ} (gaunt : is-gaunt C) where open Cat.Reasoning C iso-is-prop : ∀ {x y} → is-prop (x ≅ y) - iso-is-prop = hlevel 1 + iso-is-prop = hlevel 1 ⦃ R-H-level ⦄ ``` This implies that gaunt categories are [skeletal]: Since there is at diff --git a/src/Cat/Instances/Comma.lagda.md b/src/Cat/Instances/Comma.lagda.md index 16c84f604..9824ebdfd 100644 --- a/src/Cat/Instances/Comma.lagda.md +++ b/src/Cat/Instances/Comma.lagda.md @@ -66,10 +66,6 @@ module module C = Cat.Reasoning C module F = Cat.Functor.Reasoning F module G = Cat.Functor.Reasoning G - - open A.HLevel-instance - open B.HLevel-instance - open C.HLevel-instance ``` --> @@ -155,7 +151,7 @@ page: `↓Hom-path`{.Agda} and `↓Hom-set`{.Agda}. ↓Hom-set : ∀ x y → is-set (↓Hom x y) ↓Hom-set a b = hl' where abstract hl' : is-set (↓Hom a b) - hl' = Iso→is-hlevel 2 eqv (hlevel 2) + hl' = Iso→is-hlevel! 2 eqv ``` --> diff --git a/src/Cat/Instances/Elements.lagda.md b/src/Cat/Instances/Elements.lagda.md index edf5e4c2e..18b7de257 100644 --- a/src/Cat/Instances/Elements.lagda.md +++ b/src/Cat/Instances/Elements.lagda.md @@ -75,24 +75,17 @@ space of `Element-hom`{.Agda}. @@ -255,14 +251,13 @@ again mirror precisely the proofs for lists, or simple paths. ```agda abstract ++-nil : ∀ {a b} (fs : Zigzag C W a b) → fs ++ [] ≡ fs - ++-nil = Zigzag-elim-prop (λ h → h ++ [] ≡ h) (λ h → hlevel 1) + ++-nil = Zigzag-elim-prop (λ h → h ++ [] ≡ h) refl (λ f h p → ap (zig f) p) (λ f hf h p → ap (zag f hf) p) ++-assoc : ∀ {a b c d} (fs : Zigzag C W c d) (gs : Zigzag C W b c) (hs : Zigzag C W a b) → (fs ++ gs) ++ hs ≡ fs ++ (gs ++ hs) ++-assoc = Zigzag-elim-prop (λ fs → ∀ gs hs → (fs ++ gs) ++ hs ≡ fs ++ (gs ++ hs)) - (λ h → hlevel 1) (λ gs hs → refl) (λ f h p gs hs → ap (zig f) (p gs hs)) (λ f hf h p gs hs → ap (zag f hf) (p gs hs)) @@ -370,7 +365,6 @@ identity definitionally. → Zigzag-univ (f ++ g) ≡ Zigzag-univ f D.∘ Zigzag-univ g Zigzag-univ-++ = Zigzag-elim-prop (λ f → ∀ g → Zigzag-univ (f ++ g) ≡ Zigzag-univ f D.∘ Zigzag-univ g) - (λ _ → hlevel 1) (λ g → D.introl refl) (λ f h p g → ap (F.₁ f D.∘_) (p g) ∙ D.pulll refl) (λ f hf h p g → ap (F⁻¹ f hf D.∘_) (p g) ∙ D.pulll refl) @@ -402,7 +396,6 @@ localisation functor results in the identity. Localisation-univ-η : Localisation-univ Localise inverted ≡ Id Localisation-univ-η = Functor-path (λ _ → refl) $ Zigzag-elim-prop (λ h → Zigzag-univ Localise inverted h ≡ h) - (λ h → squash _ _) refl (λ f h p → ap (zig f) p) (λ f hf h p → ap (zag f hf) p) ``` @@ -476,7 +469,6 @@ induction. : ∀ {a b c d} (fs : Meander d c) (gs : Meander b c) (hs : Meander a b) → (fs r++ gs) ++ hs ≡ fs r++ (gs ++ hs) r++-assoc = Zigzag-elim-prop (λ fs → ∀ gs hs → (fs r++ gs) ++ hs ≡ fs r++ (gs ++ hs)) - (λ _ → hlevel 1) (λ _ _ → refl) (λ f fs rec gs hs → rec _ _) (λ f hf fs rec gs hs → rec _ _) @@ -485,7 +477,6 @@ induction. : ∀ {a b c d} (fs : Meander b c) (gs : Meander d c) (hs : Meander a b) → (fs r++ gs) r++ hs ≡ gs r++ (fs ++ hs) r++-assoc' = Zigzag-elim-prop (λ f → ∀ g h → (f r++ g) r++ h ≡ g r++ (f ++ h)) - (λ _ → hlevel 1) (λ _ _ → refl) (λ f fs rec gs hs → rec _ _) (λ f h fs rec gs hs → rec _ _) @@ -506,7 +497,6 @@ categorical *inverse* in the total localisation $\cC\loc{\cC}$. ```agda r++-cancel : ∀ {a b} (fs : Meander a b) → fs r++ fs ≡ [] r++-cancel = Zigzag-elim-prop (λ fs → fs r++ fs ≡ []) - (λ _ → hlevel 1) refl (λ f fs rec → ap (fs r++_) (zag-zig _ _ _) ∙ rec) (λ f tt fs rec → ap (fs r++_) (zig-zag _ _ _) ∙ rec) diff --git a/src/Cat/Instances/OFE.lagda.md b/src/Cat/Instances/OFE.lagda.md index 44e07bedb..36bfa8ac7 100644 --- a/src/Cat/Instances/OFE.lagda.md +++ b/src/Cat/Instances/OFE.lagda.md @@ -1,5 +1,7 @@ @@ -93,8 +91,8 @@ to write about. ```agda ⊎-OFE .has-is-ofe .has-is-prop zero x y _ _ = refl - ⊎-OFE .has-is-ofe .has-is-prop (suc n) (inl _) (inl _) = hlevel! - ⊎-OFE .has-is-ofe .has-is-prop (suc n) (inr _) (inr _) = hlevel! + ⊎-OFE .has-is-ofe .has-is-prop (suc n) (inl _) (inl _) = hlevel 1 + ⊎-OFE .has-is-ofe .has-is-prop (suc n) (inr _) (inr _) = hlevel 1 ⊎-OFE .has-is-ofe .≈-sym zero p = lift tt ⊎-OFE .has-is-ofe .≈-sym (suc n) {inl _} {inl _} p = lift (O.≈-sym _ (p .Lift.lower)) diff --git a/src/Cat/Instances/OFE/Product.lagda.md b/src/Cat/Instances/OFE/Product.lagda.md index b3e26bd7f..093661dbd 100644 --- a/src/Cat/Instances/OFE/Product.lagda.md +++ b/src/Cat/Instances/OFE/Product.lagda.md @@ -35,8 +35,6 @@ module _ {ℓa ℓb ℓa' ℓb'} {A : Type ℓa} {B : Type ℓb} (O : OFE-on ℓ _ = P module O = OFE-on O module P = OFE-on P - open OFE-H-Level O - open OFE-H-Level P ``` --> @@ -97,7 +95,6 @@ module P-ofe : ∀ {i} → OFE-on ℓr (F i) P-ofe {i} = P i module P {i} = OFE-on (P i) - module _ {i} where open OFE-H-Level (P i) public ``` --> @@ -153,7 +150,7 @@ about to get the actual inhabitant of $(1)$ that we're interested in. Π-OFE .has-is-ofe .limit x y wit i j = P.limit (x j) (y j) (λ n → wit' n j) i where wit' : ∀ n i → within (P i) n (x i) (y i) - wit' n i = out! {pa = hlevel 1} (wit n .Lift.lower) i + wit' n i = out! (wit n .Lift.lower) i ``` Now we can observe an interesting property of the initial object of $\Sets$: it is *[strict]*, meaning every morphism into it is in fact an *iso*morphism. -Intuitively, if you can write a function $X \to \bot$ then $X$ must itself be empty. +Intuitively, if you can write a function $X \to \bot$ then $X$ must itself be empty. [strict]: Cat.Diagram.Initial.html#strictness @@ -69,13 +69,13 @@ Sets-strict-initial .has-is-strict x f .inverses .invl = ext λ () Sets-strict-initial .has-is-strict x f .inverses .invr = ext λ x → absurd (f x .Lift.lower) ``` - -Crucially, this property is not shared by the initial object of $\Sets\op$! Unfolding definitions, it says +Crucially, this property is not shared by the initial object of $\Sets\op$! Unfolding definitions, it says that any function $\top \to X$ is an isomorphism, or equivalently, every inhabited set is contractible. But is this is certainly false: `Bool`{.Agda} is inhabited, but not contractible, since `true≠false`{.Agda}. @@ -103,8 +103,8 @@ we conclude that `Bool`{.Agda} is contractible, from which we obtain (modulo `li Bool≅⊤ = to-iso-⊤ (el! (Lift _ Bool)) λ _ → lift true Bool-is-contr : is-contr (Lift ℓ Bool) - Bool-is-contr = subst (is-contr ⊙ ∣_∣) (sym (Univalent.iso→path Sets^op-is-category Bool≅⊤)) hlevel! - + Bool-is-contr = subst (is-contr ⊙ ∣_∣) (sym (Univalent.iso→path Sets^op-is-category Bool≅⊤)) (hlevel 0) + true≡false : true ≡ false true≡false = lift-inj $ is-contr→is-prop Bool-is-contr _ _ ``` @@ -116,4 +116,3 @@ so we have a contradiction! Sets≠Sets^op : ¬ (Sets ℓ ≡ Sets ℓ ^op) Sets≠Sets^op p = ¬Sets^op-strict-initial (subst Strict-initial p Sets-strict-initial) ``` - diff --git a/src/Cat/Instances/Shape/Involution.lagda.md b/src/Cat/Instances/Shape/Involution.lagda.md index 7014f5977..6bd914ee8 100644 --- a/src/Cat/Instances/Shape/Involution.lagda.md +++ b/src/Cat/Instances/Shape/Involution.lagda.md @@ -82,5 +82,5 @@ walking involution would mean that there are two paths $\tt{tt} \equiv Bool≃Ob-path = Bool≃∙⤮∙-isos ∙e identity-system-gives-path is-cat Bool-is-prop : is-prop Bool - Bool-is-prop = Equiv→is-hlevel 1 Bool≃Ob-path hlevel! + Bool-is-prop = Equiv→is-hlevel 1 Bool≃Ob-path (hlevel 1) ``` diff --git a/src/Cat/Instances/Shape/Isomorphism.lagda.md b/src/Cat/Instances/Shape/Isomorphism.lagda.md index 43cf45f45..0ed0adc68 100644 --- a/src/Cat/Instances/Shape/Isomorphism.lagda.md +++ b/src/Cat/Instances/Shape/Isomorphism.lagda.md @@ -22,7 +22,7 @@ with a unique isomorphism between them. 0≅1 : Precategory lzero lzero 0≅1 .Precategory.Ob = Bool 0≅1 .Precategory.Hom _ _ = ⊤ -0≅1 .Precategory.Hom-set _ _ = hlevel! +0≅1 .Precategory.Hom-set _ _ = hlevel 2 0≅1 .Precategory.id = tt 0≅1 .Precategory._∘_ tt tt = tt 0≅1 .Precategory.idr tt i = tt @@ -52,7 +52,7 @@ The isomorphism category is strict, as its objects form a set. ```agda 0≅1-is-strict : is-set 0≅1.Ob -0≅1-is-strict = hlevel! +0≅1-is-strict = hlevel 2 ``` # The isomorphism category is not univalent diff --git a/src/Cat/Instances/Shape/Join.lagda.md b/src/Cat/Instances/Shape/Join.lagda.md index 8672a62f7..cb86a7a6b 100644 --- a/src/Cat/Instances/Shape/Join.lagda.md +++ b/src/Cat/Instances/Shape/Join.lagda.md @@ -43,9 +43,9 @@ module _ {o ℓ o' ℓ'} (C : Precategory o ℓ) (D : Precategory o' ℓ') where _⋆_ .Hom = ⋆Hom _⋆_ .Hom-set x y = iss x y where iss : ∀ x y → is-set (⋆Hom x y) - iss (inl x) (inl y) = hlevel! + iss (inl x) (inl y) = hlevel 2 iss (inl x) (inr y) _ _ p q i j = lift tt - iss (inr x) (inr y) = hlevel! + iss (inr x) (inr y) = hlevel 2 _⋆_ .id {inl x} = lift C.id _⋆_ .id {inr x} = lift D.id _⋆_ ._∘_ = ⋆compose diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index cb9b768ac..7456e99bf 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/src/Cat/Instances/Simplex.lagda.md @@ -38,10 +38,7 @@ record Δ-map (n m : Nat) : Type where ```agda open Δ-map -private - unquoteDecl eqv = declare-record-iso eqv (quote Δ-map) - Δ-map-is-set : ∀ x y → is-set (Δ-map x y) - Δ-map-is-set x y = Iso→is-hlevel 2 eqv $ hlevel! +unquoteDecl H-Level-Δ-map = declare-record-hlevel 2 H-Level-Δ-map (quote Δ-map) Δ-map-path : ∀ {n m : Nat} {f g : Δ-map n m} @@ -58,7 +55,7 @@ private Δ : Precategory lzero lzero Δ .Ob = Nat Δ .Hom n m = Δ-map n m -Δ .Hom-set = Δ-map-is-set +Δ .Hom-set _ _ = hlevel 2 Δ .id .map x = x Δ .id .ascending x y p = p diff --git a/src/Cat/Instances/Slice.lagda.md b/src/Cat/Instances/Slice.lagda.md index 6f4301f4f..142d448e9 100644 --- a/src/Cat/Instances/Slice.lagda.md +++ b/src/Cat/Instances/Slice.lagda.md @@ -128,24 +128,13 @@ says that the map $h$ "respects reindexing", or less obliquely → x ≡ y /-Hom-path = /-Hom-pathp refl refl - Extensional-/-Hom - : ∀ {c a b ℓ} ⦃ sa : Extensional (C.Hom (/-Obj.domain a) (/-Obj.domain b)) ℓ ⦄ - → Extensional (/-Hom {c = c} a b) ℓ - Extensional-/-Hom ⦃ sa ⦄ = injection→extensional! (/-Hom-pathp refl refl) sa - instance - extensionality-/-hom : ∀ {c a b} → Extensionality (/-Hom {c = c} a b) - extensionality-/-hom = record { lemma = quote Extensional-/-Hom } - - private unquoteDecl eqv = declare-record-iso eqv (quote /-Hom) - - abstract - /-Hom-is-set : ∀ {c a b} → is-set (/-Hom {c = c} a b) - /-Hom-is-set {a = a} {b} = hl where abstract - open C.HLevel-instance + Extensional-/-Hom + : ∀ {c a b ℓ} ⦃ sa : Extensional (C.Hom (/-Obj.domain a) (/-Obj.domain b)) ℓ ⦄ + → Extensional (/-Hom {c = c} a b) ℓ + Extensional-/-Hom ⦃ sa ⦄ = injection→extensional! (/-Hom-pathp refl refl) sa - hl : is-set (/-Hom a b) - hl = Iso→is-hlevel 2 eqv (hlevel 2) +unquoteDecl H-Level-/-Hom = declare-record-hlevel 2 H-Level-/-Hom (quote /-Hom) ``` --> @@ -163,7 +152,7 @@ Slice C c = precat where precat : Precategory _ _ precat .Ob = /-Obj {C = C} c precat .Hom = /-Hom - precat .Hom-set x y = /-Hom-is-set + precat .Hom-set x y = hlevel 2 precat .id .map = C.id precat .id .commutes = C.idr _ ``` @@ -522,7 +511,7 @@ fast: ```agda Total-space : Functor Cat[ Disc' I , Sets ℓ ] (Slice (Sets ℓ) I) - Total-space .F₀ F .domain = el (Σ _ (∣_∣ ⊙ F₀ F)) hlevel! + Total-space .F₀ F .domain = el! (Σ _ (∣_∣ ⊙ F₀ F)) Total-space .F₀ F .map = fst Total-space .F₁ nt .map (i , x) = i , nt .η _ x diff --git a/src/Cat/Instances/Slice/Presheaf.lagda.md b/src/Cat/Instances/Slice/Presheaf.lagda.md index 2fedfa1a8..cf63f9f69 100644 --- a/src/Cat/Instances/Slice/Presheaf.lagda.md +++ b/src/Cat/Instances/Slice/Presheaf.lagda.md @@ -105,7 +105,7 @@ projection `fst`{.Agda}: presheaf→slice-ob y = obj where obj : /-Obj {C = Cat[ _ , _ ]} P obj .domain .F₀ c .∣_∣ = Σ[ sect ∈ P ʻ c ] y ʻ elem c sect - obj .domain .F₀ c .is-tr = hlevel! + obj .domain .F₀ c .is-tr = hlevel 2 obj .domain .F₁ f (x , p) = P.₁ f x , y .F₁ (elem-hom f refl) p obj .map .η x = fst ``` diff --git a/src/Cat/Instances/StrictCat.lagda.md b/src/Cat/Instances/StrictCat.lagda.md index cd4f7acf1..85d7f8a62 100644 --- a/src/Cat/Instances/StrictCat.lagda.md +++ b/src/Cat/Instances/StrictCat.lagda.md @@ -41,13 +41,9 @@ private unquoteDecl eqv = declare-record-iso eqv (quote Functor) Functor-is-set : ∀ {o h} {C D : Precategory o h} → is-set (Ob D) → is-set (Functor C D) -Functor-is-set {o = o} {h} {C} {D} dobset = - Iso→is-hlevel 2 eqv (hlevel 2) - where - open Precategory.HLevel-instance D - instance - Dob : H-Level (Ob D) 2 - Dob = basic-instance 2 dobset +Functor-is-set {o = o} {h} {C} {D} dobset = Iso→is-hlevel! 2 eqv where instance + Dob : H-Level (Ob D) 2 + Dob = basic-instance 2 dobset ``` --> diff --git a/src/Cat/Instances/StrictCat/Cohesive.lagda.md b/src/Cat/Instances/StrictCat/Cohesive.lagda.md index 0c98fa780..c0789f120 100644 --- a/src/Cat/Instances/StrictCat/Cohesive.lagda.md +++ b/src/Cat/Instances/StrictCat/Cohesive.lagda.md @@ -351,7 +351,7 @@ the morphisms. ```agda f : π₀ ʻ (C ×ᶜ D) → π₀ ʻ C × π₀ ʻ D f = Quot-elim - (λ _ → hlevel!) + (λ _ → hlevel 2) (λ (a , b) → inc a , inc b) λ (x , x') (y , y') (f , g) i → glue (x , y , f) i , glue (x' , y' , g) i diff --git a/src/Cat/Instances/Twisted.lagda.md b/src/Cat/Instances/Twisted.lagda.md index 8b083750e..bb9f12f6c 100644 --- a/src/Cat/Instances/Twisted.lagda.md +++ b/src/Cat/Instances/Twisted.lagda.md @@ -78,8 +78,7 @@ module _ {o ℓ} (C : Precategory o ℓ) where Twisted : Precategory (o ⊔ ℓ) ℓ Twisted .Precategory.Ob = Σ[ (a , b) ∈ Ob × Ob ] Hom a b Twisted .Precategory.Hom (_ , f) (_ , g) = Twist f g - Twisted .Precategory.Hom-set (_ , f) (_ , g) = - Iso→is-hlevel 2 eqv (hlevel 2) + Twisted .Precategory.Hom-set (_ , f) (_ , g) = Iso→is-hlevel! 2 eqv Twisted .Precategory.id = record { before = id ; after = id ; commutes = idl _ ∙ idr _ } Twisted .Precategory._∘_ t1 t2 .Twist.before = t2 .Twist.before ∘ t1 .Twist.before @@ -119,8 +118,7 @@ Note that the twisted arrow category is equivalently the F .F-∘ f g = trivial! F-precat-iso : is-precat-iso F - F-precat-iso .has-is-ff = injective-surjective→is-equiv - (Element-hom-is-set _ _ _) + F-precat-iso .has-is-ff = injective-surjective→is-equiv! (λ p → Twist-path (ap (fst ⊙ hom) p) (ap (snd ⊙ hom) p)) λ f → inc (twist (f .hom .fst) (f .hom .snd) (f .commute) , trivial!) F-precat-iso .has-is-iso = is-iso→is-equiv (iso diff --git a/src/Cat/Internal/Base.lagda.md b/src/Cat/Internal/Base.lagda.md index 5cd3d9bf5..7f1ef47d5 100644 --- a/src/Cat/Internal/Base.lagda.md +++ b/src/Cat/Internal/Base.lagda.md @@ -180,7 +180,7 @@ private unquoteDecl eqv = declare-record-iso eqv (quote Internal-hom) Internal-hom-set : ∀ {Γ C₀ C₁} {src tgt : Hom C₁ C₀} {x y : Hom Γ C₀} → is-set (Internal-hom src tgt x y) -Internal-hom-set = Iso→is-hlevel 2 eqv hlevel! +Internal-hom-set = Iso→is-hlevel! 2 eqv instance H-Level-Internal-hom @@ -532,6 +532,8 @@ open _=>i_ diff --git a/src/Cat/Internal/Functor/Outer.lagda.md b/src/Cat/Internal/Functor/Outer.lagda.md index 966d8fcef..2290c717f 100644 --- a/src/Cat/Internal/Functor/Outer.lagda.md +++ b/src/Cat/Internal/Functor/Outer.lagda.md @@ -334,17 +334,7 @@ us to work in the internal language of $\cC$. (α .ηo-nat px σ) (β .ηo-nat px σ) i - private unquoteDecl nat-eqv = declare-record-iso nat-eqv (quote _=>o_) - - Outer-nat-is-set - : ∀ {F G : Outer-functor ℂ} → is-set (F =>o G) - Outer-nat-is-set = Iso→is-hlevel 2 nat-eqv hlevel! - -instance - H-Level-Outer-nat - : ∀ {ℂ : Internal-cat} {F G : Outer-functor ℂ} {n} - → H-Level (F =>o G) (2 + n) - H-Level-Outer-nat = basic-instance 2 Outer-nat-is-set +unquoteDecl H-Level-=>o = declare-record-hlevel 2 H-Level-=>o (quote _=>o_) ``` --> diff --git a/src/Cat/Monoidal/Diagram/Monoid.lagda.md b/src/Cat/Monoidal/Diagram/Monoid.lagda.md index 1706f40e0..bda66958f 100644 --- a/src/Cat/Monoidal/Diagram/Monoid.lagda.md +++ b/src/Cat/Monoidal/Diagram/Monoid.lagda.md @@ -1,6 +1,6 @@ diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md index 4951e056a..38f44743b 100644 --- a/src/Cat/Morphism.lagda.md +++ b/src/Cat/Morphism.lagda.md @@ -1,6 +1,6 @@ @@ -80,18 +73,6 @@ record _↠_ (a b : Ob) : Type (o ⊔ h) where open _↠_ public ``` - - The identity morphism is monic and epic. ```agda @@ -238,20 +219,6 @@ has-section→epic {f = f} f-sect g h p = h ∎ ``` - - ## Retracts A morphism $r : A \to B$ is a retract of another morphism $s : B \to A$ @@ -297,20 +264,6 @@ retract-∘ f-ret g-ret .is-retract = retract-of-∘ (f-ret .is-retract) (g-ret .is-retract) ``` - - If $f$ has a retract, then $f$ is monic. ```agda @@ -541,10 +494,6 @@ make-iso f g p q ._≅_.from = g make-iso f g p q ._≅_.inverses .Inverses.invl = p make-iso f g p q ._≅_.inverses .Inverses.invr = q -instance - H-Level-is-invertible : ∀ {f : Hom a b} {n} → H-Level (is-invertible f) (suc n) - H-Level-is-invertible = prop-instance is-invertible-is-prop - inverses→invertible : ∀ {f : Hom a b} {g : Hom b a} → Inverses f g → is-invertible f inverses→invertible x .is-invertible.inv = _ inverses→invertible x .is-invertible.inverses = x @@ -566,24 +515,6 @@ is-invertible-inverse g = iso→invertible : (i : a ≅ b) → is-invertible (i ._≅_.to) iso→invertible i = record { inv = i ._≅_.from ; inverses = i ._≅_.inverses } -≅-is-set : is-set (a ≅ b) -≅-is-set x y p q = s where - open _≅_ - open Inverses - - s : p ≡ q - s i j .to = Hom-set _ _ (x .to) (y .to) (ap to p) (ap to q) i j - s i j .from = Hom-set _ _ (x .from) (y .from) (ap from p) (ap from q) i j - s i j .inverses = - is-prop→squarep - (λ i j → Inverses-are-prop {f = Hom-set _ _ (x .to) (y .to) (ap to p) (ap to q) i j} - {g = Hom-set _ _ (x .from) (y .from) (ap from p) (ap from q) i j}) - (λ i → x .inverses) (λ i → p i .inverses) (λ i → q i .inverses) (λ i → y .inverses) i j - -instance - H-Level-≅ : ∀ {a b} {n} → H-Level (a ≅ b) (suc (suc n)) - H-Level-≅ = basic-instance 2 ≅-is-set - private ≅-pathp-internal : (p : a ≡ c) (q : b ≡ d) diff --git a/src/Cat/Morphism/Extensionality.agda b/src/Cat/Morphism/Extensionality.agda deleted file mode 100644 index 3c7ab5908..000000000 --- a/src/Cat/Morphism/Extensionality.agda +++ /dev/null @@ -1,23 +0,0 @@ -open import 1Lab.Prelude - -open import Cat.Base - -import Cat.Morphism - -module Cat.Morphism.Extensionality {o ℓ} {C : Precategory o ℓ} where - -open Cat.Morphism C - -Extensional-≅ - : ∀ {ℓr} {a b} - → ⦃ sa : Extensional (Hom a b) ℓr ⦄ - → Extensional (a ≅ b) ℓr -Extensional-≅ ⦃ sa ⦄ .Pathᵉ a b = Pathᵉ sa (a .to) (b .to) -Extensional-≅ ⦃ sa ⦄ .reflᵉ im = reflᵉ sa (im .to) -Extensional-≅ ⦃ sa ⦄ .idsᵉ = set-identity-system - (λ x y → Pathᵉ-is-hlevel 1 sa hlevel!) - (λ p → ≅-path (sa .idsᵉ .to-path p)) - -instance - extensionality-≅ : ∀ {a b} → Extensionality (a ≅ b) - extensionality-≅ = record { lemma = quote Extensional-≅ } diff --git a/src/Cat/Morphism/Factorisation.lagda.md b/src/Cat/Morphism/Factorisation.lagda.md index db68908b0..96ad84c5b 100644 --- a/src/Cat/Morphism/Factorisation.lagda.md +++ b/src/Cat/Morphism/Factorisation.lagda.md @@ -216,7 +216,7 @@ orthogonal to itself, hence an isomorphism. in-intersection≃is-iso : ∀ {a b} (f : C.Hom a b) → C.is-invertible f ≃ ((f ∈ E) × (f ∈ M)) - in-intersection≃is-iso f = prop-ext (hlevel 1) (×-is-hlevel 1 hlevel! hlevel!) + in-intersection≃is-iso f = prop-ext! (λ fi → is-iso→in-E f fi , is-iso→in-M f fi) λ { (a , b) → in-intersection→is-iso f a b } ``` diff --git a/src/Cat/Morphism/Instances.agda b/src/Cat/Morphism/Instances.agda new file mode 100644 index 000000000..940afe8aa --- /dev/null +++ b/src/Cat/Morphism/Instances.agda @@ -0,0 +1,32 @@ +open import 1Lab.Prelude hiding (_∘_ ; id ; _↪_ ; _↠_) + +open import Cat.Morphism +open import Cat.Base + +open Precategory + +module Cat.Morphism.Instances where + +instance + H-Level-is-invertible + : ∀ {o ℓ} {C : Precategory o ℓ} {a b} {f : C .Hom a b} {n} → H-Level (is-invertible C f) (suc n) + H-Level-is-invertible {C = C} = prop-instance (is-invertible-is-prop C) + +unquoteDecl H-Level-↪ = declare-record-hlevel 2 H-Level-↪ (quote _↪_) +unquoteDecl H-Level-↠ = declare-record-hlevel 2 H-Level-↠ (quote _↠_) +unquoteDecl H-Level-Inverses = declare-record-hlevel 2 H-Level-Inverses (quote Inverses) +unquoteDecl H-Level-≅ = declare-record-hlevel 2 H-Level-≅ (quote _≅_) +unquoteDecl + H-Level-has-section = declare-record-hlevel 2 H-Level-has-section (quote has-section) +unquoteDecl + H-Level-has-retract = declare-record-hlevel 2 H-Level-has-retract (quote has-retract) + +module _ {o ℓ} {C : Precategory o ℓ} where instance + Extensional-↪ : ∀ {a b ℓr} ⦃ _ : Extensional (C .Hom a b) ℓr ⦄ → Extensional (_↪_ C a b) ℓr + Extensional-↪ ⦃ sa ⦄ = injection→extensional! (↪-pathp C) sa + + Extensional-↠ : ∀ {a b ℓr} ⦃ _ : Extensional (C .Hom a b) ℓr ⦄ → Extensional (_↠_ C a b) ℓr + Extensional-↠ ⦃ sa ⦄ = injection→extensional! (↠-pathp C) sa + + Extensional-≅ : ∀ {a b ℓr} ⦃ _ : Extensional (C .Hom a b) ℓr ⦄ → Extensional (_≅_ C a b) ℓr + Extensional-≅ ⦃ sa ⦄ = injection→extensional! (≅-pathp C refl refl) sa diff --git a/src/Cat/Morphism/StrongEpi.lagda.md b/src/Cat/Morphism/StrongEpi.lagda.md index 3d79be30d..6612d33b9 100644 --- a/src/Cat/Morphism/StrongEpi.lagda.md +++ b/src/Cat/Morphism/StrongEpi.lagda.md @@ -67,7 +67,7 @@ lifts→is-strong-epi epic lift-it = epic , λ {c} {d} mm sq → abstract is-strong-epi-is-prop : ∀ {a b} (f : Hom a b) → is-prop (is-strong-epi f) - is-strong-epi-is-prop f = hlevel! + is-strong-epi-is-prop f = hlevel 1 ``` --> diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index c62a8a59e..aa1979f86 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -26,4 +26,4 @@ open import Cat.Univalent ; module Univalent ) public -open import Cat.Morphism.Extensionality public +open import Cat.Morphism.Instances public diff --git a/src/Cat/Regular/Image.lagda.md b/src/Cat/Regular/Image.lagda.md index f8a9e7a1d..e2d4362a1 100644 --- a/src/Cat/Regular/Image.lagda.md +++ b/src/Cat/Regular/Image.lagda.md @@ -62,7 +62,7 @@ Im-universal → f ≡ m .map ∘ e → Im f ≤ₘ m Im-universal f m {e = e} p = r where - the-lift = out! {pa = is-strong-epi-is-prop C _} (factor f .mediate∈E) .snd + the-lift = out! (factor f .mediate∈E) .snd record { Subobject m } (sym (factor f .factors) ∙ p) r : _ ≤ₘ _ @@ -98,7 +98,7 @@ image-pre-cover {a = a} {b} {c} f g g-covers = Sub-antisym imf≤imfg imfg≤imf (out! (factor f .forget∈M) _ _ (sym (pulll (sym (imfg≤imf .sq) ∙ idl _) ∙ sym (factor (f ∘ g) .factors) ∙ pushl (factor f .factors)))) .centre inverse : is-invertible (imfg≤imf .map) - inverse = is-strong-epi→is-extremal-epi C (out! {pa = is-strong-epi-is-prop C _} (factor f .mediate∈E)) + inverse = is-strong-epi→is-extremal-epi C (out! (factor f .mediate∈E)) (≤ₘ→mono imfg≤imf) (the-lift .fst) (sym (the-lift .snd .snd)) imf≤imfg : Im f ≤ₘ Im (f ∘ g) diff --git a/src/Cat/Restriction/Reasoning.lagda.md b/src/Cat/Restriction/Reasoning.lagda.md index 01d25c989..bc49bfa11 100644 --- a/src/Cat/Restriction/Reasoning.lagda.md +++ b/src/Cat/Restriction/Reasoning.lagda.md @@ -111,20 +111,11 @@ forms a set. ```agda is-total-is-prop : ∀ {x y} → (f : Hom x y) → is-prop (is-total f) is-total-is-prop f = Hom-set _ _ _ _ - -Total-is-set : ∀ {x y} → is-set (Total x y) ``` diff --git a/src/Cat/Univalent.lagda.md b/src/Cat/Univalent.lagda.md index b08d90ce3..a8796a3e6 100644 --- a/src/Cat/Univalent.lagda.md +++ b/src/Cat/Univalent.lagda.md @@ -2,6 +2,7 @@ ``` open import 1Lab.Prelude hiding (_∘_ ; id) +open import Cat.Morphism.Instances open import Cat.Base import Cat.Reasoning @@ -65,8 +66,8 @@ determines the h-level of the type it applies to, we have that the space of objects in any univalent category is a proposition: ```agda - Ob-is-groupoid : is-groupoid (C .Precategory.Ob) - Ob-is-groupoid = path→iso.hlevel 2 λ _ _ → ≅-is-set + Ob-is-groupoid : is-groupoid ⌞ C ⌟ + Ob-is-groupoid = path→iso.hlevel 2 λ _ _ → hlevel 2 ``` :::{.definition #transport-in-hom} diff --git a/src/Cat/Univalent/Rezk.lagda.md b/src/Cat/Univalent/Rezk.lagda.md index 00cd5ef1c..e100bd6e9 100644 --- a/src/Cat/Univalent/Rezk.lagda.md +++ b/src/Cat/Univalent/Rezk.lagda.md @@ -1,6 +1,5 @@ -
It will again turn out that any initial choice of fibre over $b$ and $b'$ gives a morphism candidate over $f : b \to b'$, and the @@ -481,11 +471,11 @@ This proof _really_ isn't commented. I'm sorry. Homs-contr' {b = b} {b'} f = do (a₀ , h) ← H-eso b (a₀' , h') ← H-eso b' - inc (contr (Homs-pt f a₀ h a₀' h') λ h' → Σ-prop-path - (λ _ → compat-prop f) (sym (Homs-prop' f _ _ _ _ h'))) + inc (contr (Homs-pt f a₀ h a₀' h') λ h' → Σ-prop-path! + (sym (Homs-prop' f _ _ _ _ h'))) Homs-contr : ∀ {b b'} (f : B.Hom b b') → is-contr (Homs f) - Homs-contr f = ∥-∥-proj! (Homs-contr' f) + Homs-contr f = ∥-∥-out! (Homs-contr' f) G₁ : ∀ {b b'} → B.Hom b b' → C.Hom (G₀ b) (G₀ b') G₁ f = Homs-contr f .centre .fst @@ -549,7 +539,7 @@ a set --- a proposition --- these choices don't matter, so we can use essential surjectivity of $H$. ```agda - G .F-∘ {x} {y} {z} f g = ∥-∥-proj! do + G .F-∘ {x} {y} {z} f g = ∥-∥-out! do (ax , hx) ← H-eso x (ay , hy) ← H-eso y (az , hz) ← H-eso z diff --git a/src/Data/Dec/Path.lagda.md b/src/Data/Dec/Path.lagda.md index 9d2c9ae01..32ab5d331 100644 --- a/src/Data/Dec/Path.lagda.md +++ b/src/Data/Dec/Path.lagda.md @@ -63,7 +63,4 @@ instance H-Level-Dec : ∀ {n} {ℓ} {A : Type ℓ} ⦃ hl : H-Level A n ⦄ → H-Level (Dec A) n H-Level-Dec {n} = hlevel-instance (Dec-is-hlevel n (hlevel n)) - - decomp-dec : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (Dec A) - decomp-dec = decomp (quote Dec-is-hlevel) (`level ∷ `search ∷ []) ``` diff --git a/src/Data/Fin/Finite.lagda.md b/src/Data/Fin/Finite.lagda.md index da6d1e199..09aedc618 100644 --- a/src/Data/Fin/Finite.lagda.md +++ b/src/Data/Fin/Finite.lagda.md @@ -107,11 +107,11 @@ open Finite using (Finite→is-set) public instance opaque H-Level-Finite : ∀ {ℓ} {A : Type ℓ} {n : Nat} → H-Level (Finite A) (suc n) H-Level-Finite = prop-instance {T = Finite _} λ where - x y i .Finite.cardinality → ∥-∥-proj! + x y i .Finite.cardinality → ∥-∥-out! ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i x y i .Finite.enumeration → is-prop→pathp - {B = λ i → ∥ _ ≃ Fin (∥-∥-proj! ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i) ∥} + {B = λ i → ∥ _ ≃ Fin (∥-∥-out! ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i) ∥} (λ _ → squash) (x .enumeration) (y .enumeration) i @@ -146,7 +146,7 @@ Finite-≃ ⦃ fin {n} e ⦄ e' = fin (∥-∥-map (e' e⁻¹ ∙e_) e) equiv→same-cardinality : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ fa : Finite A ⦄ ⦃ fb : Finite B ⦄ → ∥ A ≃ B ∥ → fa .Finite.cardinality ≡ fb .Finite.cardinality -equiv→same-cardinality ⦃ fa ⦄ ⦃ fb ⦄ e = ∥-∥-proj! do +equiv→same-cardinality ⦃ fa ⦄ ⦃ fb ⦄ e = ∥-∥-out! do e ← e ea ← fa .Finite.enumeration eb ← fb .Finite.enumeration @@ -164,7 +164,7 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ fb : Finite B ⦄ (e : ∥ A ≃ B ∥) (f : A → B) where Finite-injection→equiv : injective f → is-equiv f - Finite-injection→equiv inj = ∥-∥-proj! do + Finite-injection→equiv inj = ∥-∥-out! do e ← e eb ← fb .Finite.enumeration pure @@ -174,7 +174,7 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ fb : Finite B ⦄ $ Equiv.injective (eb e⁻¹ ∙e e e⁻¹) ∘ inj ∘ Equiv.injective eb Finite-surjection→equiv : is-surjective f → is-equiv f - Finite-surjection→equiv surj = ∥-∥-proj! do + Finite-surjection→equiv surj = ∥-∥-out! do e ← e eb ← fb .Finite.enumeration pure @@ -222,7 +222,7 @@ Finite-⊎ {A = A} {B = B} = fin $ do beq ← enumeration {T = B} pure (⊎-ap aeq beq ∙e Finite-coproduct) -Finite-Π {A = A} {P = P} ⦃ afin ⦄ ⦃ pfin ⦄ = ∥-∥-proj! do +Finite-Π {A = A} {P = P} ⦃ afin ⦄ ⦃ pfin ⦄ = ∥-∥-out! do aeq ← afin .Finite.enumeration let module aeq = Equiv aeq @@ -232,7 +232,7 @@ Finite-Π {A = A} {P = P} ⦃ afin ⦄ ⦃ pfin ⦄ = ∥-∥-proj! do t ← Finite-choice λ x → pfin {x} .Finite.enumeration pure (Π-cod≃ t ∙e Π-dom≃ aeq.inverse ∙e Finite-product bc) -Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ pfin ⦄ = ∥-∥-proj! do +Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ pfin ⦄ = ∥-∥-out! do aeq ← afin .Finite.enumeration let module aeq = Equiv aeq diff --git a/src/Data/Fin/Finite/Listed.lagda.md b/src/Data/Fin/Finite/Listed.lagda.md index 5bed9b642..5abd0db08 100644 --- a/src/Data/Fin/Finite/Listed.lagda.md +++ b/src/Data/Fin/Finite/Listed.lagda.md @@ -148,7 +148,7 @@ the listing into an enumeration. nub-listing : ⦃ _ : Discrete A ⦄ → Listing A → Enumeration A nub-listing li = record { members = nub m - ; has-member = λ a → ∥-∥-proj! do + ; has-member = λ a → ∥-∥-out! do memb ← has a pure (is-prop∙→is-contr (member-nub-is-prop m) (member→member-nub memb)) } @@ -164,7 +164,7 @@ Discrete-finitely-indexed→Finite : ⦃ _ : Discrete A ⦄ → is-finitely-indexed A → Finite A -Discrete-finitely-indexed→Finite fi = ∥-∥-proj! do +Discrete-finitely-indexed→Finite fi = ∥-∥-out! do cov ← □-tr fi let over = finite-cover→listing cov diff --git a/src/Data/Fin/Indexed.lagda.md b/src/Data/Fin/Indexed.lagda.md index cd008ec5d..1d69ec131 100644 --- a/src/Data/Fin/Indexed.lagda.md +++ b/src/Data/Fin/Indexed.lagda.md @@ -191,5 +191,5 @@ Moreover, we have that a singleton set is $K$-finite, as well. ```agda singleton-is-K-finite : is-set T → (x : T) → is-K-finite (singleton x) singleton-is-K-finite t-set x = inc (covering {cardinality = 1} (λ _ → x , inc refl) - λ (y , p) → inc (fzero , Σ-prop-path! (out! {pa = t-set _ _} p))) + λ (y , p) → inc (fzero , Σ-prop-path! (□-rec (t-set _ _) id p))) ``` diff --git a/src/Data/Id/Base.lagda.md b/src/Data/Id/Base.lagda.md index a94df27fe..03fdf7b5d 100644 --- a/src/Data/Id/Base.lagda.md +++ b/src/Data/Id/Base.lagda.md @@ -131,37 +131,29 @@ Discrete-inj' f inj {x} {y} = Dec-map (λ p → Id≃path.to (inj p)) (λ x → Id≃path.from (ap f x)) (f x ≡ᵢ? f y) instance - Dec-Σ-path + Discrete-Σ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → ⦃ _ : Discrete A ⦄ → ⦃ _ : ∀ {x} → Discrete (B x) ⦄ → Discrete (Σ A B) - Dec-Σ-path {B = B} {x = a , b} {a' , b'} = case a ≡ᵢ? a' of λ where + Discrete-Σ {B = B} {x = a , b} {a' , b'} = case a ≡ᵢ? a' of λ where (yes reflᵢ) → case b ≡? b' of λ where (yes q) → yes (ap₂ _,_ refl q) (no ¬q) → no λ p → ¬q (Σ-inj-set (Discrete→is-set auto) p) (no ¬p) → no λ p → ¬p (Id≃path.from (ap fst p)) -abstract - Id-is-hlevel - : ∀ {ℓ} {A : Type ℓ} (n : Nat) - → is-hlevel A n - → ∀ {a b : A} - → is-hlevel (a ≡ᵢ b) n - Id-is-hlevel n p = Equiv→is-hlevel n Id≃path (Path-is-hlevel n p) - - Id-is-hlevel' - : ∀ {ℓ} {A : Type ℓ} (n : Nat) - → is-hlevel A (suc n) - → ∀ {a b : A} - → is-hlevel (a ≡ᵢ b) n - Id-is-hlevel' n p = Equiv→is-hlevel n Id≃path (Path-is-hlevel' n p _ _) - -substᵢ-filler-set : ∀ {ℓ ℓ'} {A : Type ℓ} (P : A → Type ℓ') - → is-set A - → {a : A} - → (p : a ≡ᵢ a) - → ∀ x → x ≡ substᵢ P p x +abstract instance + H-Level-Id + : ∀ {ℓ n} {S : Type ℓ} ⦃ s : H-Level S (suc n) ⦄ {x y : S} + → H-Level (x ≡ᵢ y) n + H-Level-Id {n = n} = hlevel-instance (Equiv→is-hlevel n Id≃path (hlevel n)) + +substᵢ-filler-set + : ∀ {ℓ ℓ'} {A : Type ℓ} (P : A → Type ℓ') + → is-set A + → {a : A} + → (p : a ≡ᵢ a) + → ∀ x → x ≡ substᵢ P p x substᵢ-filler-set P is-set-A p x = subst (λ q → x ≡ substᵢ P q x) (is-set→is-setᵢ is-set-A _ _ reflᵢ p) refl record Recallᵢ @@ -179,7 +171,6 @@ recallᵢ → Recallᵢ f x (f x) recallᵢ f x = ⟪ reflᵢ ⟫ᵢ - symᵢ : ∀ {a} {A : Type a} {x y : A} → x ≡ᵢ y → y ≡ᵢ x symᵢ reflᵢ = reflᵢ diff --git a/src/Data/Image.lagda.md b/src/Data/Image.lagda.md index dd6bcb5aa..c19536996 100644 --- a/src/Data/Image.lagda.md +++ b/src/Data/Image.lagda.md @@ -1,6 +1,5 @@ diff --git a/src/Data/Maybe/Properties.lagda.md b/src/Data/Maybe/Properties.lagda.md index f7849c3ae..c17d0ad62 100644 --- a/src/Data/Maybe/Properties.lagda.md +++ b/src/Data/Maybe/Properties.lagda.md @@ -7,7 +7,7 @@ open import Data.Maybe.Base open import Data.List.Base using (_∷_; []) open import Data.Dec.Base open import Data.Nat.Base -open import Data.Fin +open import Data.Fin hiding (_≤_) ``` --> @@ -108,8 +108,11 @@ Maybe-is-hlevel n ahl x y = diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md index 0d22867f6..9da4870d7 100644 --- a/src/Data/Nat/Base.lagda.md +++ b/src/Data/Nat/Base.lagda.md @@ -204,6 +204,16 @@ instance s≤s' : ∀ {x y} → ⦃ x ≤ y ⦄ → suc x ≤ suc y s≤s' ⦃ x ⦄ = s≤s x + x≤x : ∀ {x} → x ≤ x + x≤x {zero} = 0≤x + x≤x {suc x} = s≤s x≤x + + x≤sucy : ∀ {x y} ⦃ p : x ≤ y ⦄ → x ≤ suc y + x≤sucy {.0} {y} ⦃ 0≤x ⦄ = 0≤x + x≤sucy {.(suc _)} {.(suc _)} ⦃ s≤s p ⦄ = s≤s (x≤sucy ⦃ p ⦄) + + {-# INCOHERENT x≤x x≤sucy #-} + Positive : Nat → Type Positive zero = ⊥ Positive (suc n) = ⊤ diff --git a/src/Data/Nat/Divisible.lagda.md b/src/Data/Nat/Divisible.lagda.md index 7e75dfd7a..5129d3f42 100644 --- a/src/Data/Nat/Divisible.lagda.md +++ b/src/Data/Nat/Divisible.lagda.md @@ -50,6 +50,7 @@ this indirection, we can prove that divisibility is a mere property: instance H-Level-∣ : ∀ {x y} {n} → H-Level (x ∣ y) (suc n) H-Level-∣ = prop-instance (∣-is-prop _ _) + {-# INCOHERENT H-Level-∣ #-} ``` The type $x | y$ is, in fact, the [[propositional truncation]] of $(* diff --git a/src/Data/Partial/Base.lagda.md b/src/Data/Partial/Base.lagda.md index 8c219aeb7..046edcba0 100644 --- a/src/Data/Partial/Base.lagda.md +++ b/src/Data/Partial/Base.lagda.md @@ -4,6 +4,7 @@ open import 1Lab.Prelude open import Data.Maybe.Base open import Data.List.Base +open import Data.Nat.Base open import Data.Dec ``` --> @@ -111,16 +112,11 @@ instance @@ -148,16 +144,10 @@ record _⊑_ {ℓ} {A : Type ℓ} (x y : ↯ A) : Type ℓ where ```agda open _⊑_ public -abstract - ⊑-is-hlevel : ∀ {x y : ↯ A} n → is-hlevel A (2 + n) → is-hlevel (x ⊑ y) (suc n) - ⊑-is-hlevel {x = x} {y = y} n hl = Iso→is-hlevel (suc n) eqv $ - Σ-is-hlevel (suc n) (Π-is-hlevel (suc n) λ _ → is-prop→is-hlevel-suc (y .def .is-tr)) λ _ → - Π-is-hlevel (suc n) λ _ → hl _ _ +abstract instance + H-Level-⊑ : ∀ {A : Type ℓ} {x y : ↯ A} {n} ⦃ _ : 1 ≤ n ⦄ ⦃ _ : H-Level A (suc n) ⦄ → H-Level (x ⊑ y) n + H-Level-⊑ {n = suc n} ⦃ s≤s p ⦄ = hlevel-instance $ Iso→is-hlevel! (suc n) eqv where unquoteDecl eqv = declare-record-iso eqv (quote _⊑_) - -instance - decomp-⊑ : ∀ {ℓ} {A : Type ℓ} {x y : ↯ A} → hlevel-decomposition (x ⊑ y) - decomp-⊑ = decomp (quote ⊑-is-hlevel) (`level-minus 1 ∷ `search ∷ []) ``` --> @@ -200,7 +190,7 @@ always a .elt _ = a part-bind : ↯ A → (A → ↯ B) → ↯ B part-bind x f .def .∣_∣ = Σ[ px ∈ x ] (f ʻ x .elt px) -part-bind x f .def .is-tr = hlevel! +part-bind x f .def .is-tr = hlevel 1 part-bind x f .elt (px , pfx) = f (x .elt px) .elt pfx ``` @@ -211,7 +201,7 @@ result whenever they are both defined. ```agda part-ap : ↯ (A → B) → ↯ A → ↯ B part-ap f x .def .∣_∣ = ⌞ f ⌟ × ⌞ x ⌟ -part-ap f x .def .is-tr = hlevel! +part-ap f x .def .is-tr = hlevel 1 part-ap f x .elt (pf , px) = f .elt pf (x .elt px) ``` diff --git a/src/Data/Partial/Properties.lagda.md b/src/Data/Partial/Properties.lagda.md index 70962ee7e..78e1f006a 100644 --- a/src/Data/Partial/Properties.lagda.md +++ b/src/Data/Partial/Properties.lagda.md @@ -31,9 +31,6 @@ $A$ is a [[set]], the information ordering is an actual [[poset]]: ⊑-refl .implies x-def = x-def ⊑-refl .refines _ = refl - ⊑-thin : {x y : ↯ A} → is-set A → is-prop (x ⊑ y) - ⊑-thin A-set = ⊑-is-hlevel 0 A-set - ⊑-trans : {x y z : ↯ A} → x ⊑ y → y ⊑ z → x ⊑ z ⊑-trans p q .implies = q .implies ∘ p .implies ⊑-trans {x = x} {y} {z} p q .refines x-def = diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md index d6fe91463..0de45bf3b 100644 --- a/src/Data/Power.lagda.md +++ b/src/Data/Power.lagda.md @@ -105,13 +105,3 @@ _∪_ : ℙ X → ℙ X → ℙ X infixr 32 _∩_ infixr 31 _∪_ ``` - -## Images - -```agda -image-of - : ∀ {a b} {A : Type a} {B : Type b} {@(tactic hlevel-tactic-worker) b-set : is-set B} - → (f : A → B) → ℙ A → ℙ B -image-of {A = A} {b-set = b-set} f s b .∣_∣ = □ (Σ[ a ∈ A ] ((a ∈ s) × (f a ≡ b))) -image-of _ _ _ .is-tr = squash -``` diff --git a/src/Data/Power/Complemented.lagda.md b/src/Data/Power/Complemented.lagda.md index 533eeadcc..2804cf03e 100644 --- a/src/Data/Power/Complemented.lagda.md +++ b/src/Data/Power/Complemented.lagda.md @@ -53,7 +53,7 @@ is-decidable {A = A} p = (a : A) → Dec (a ∈ p) is-decidable→is-complemented : (p : ℙ A) → is-decidable p → is-complemented p is-decidable→is-complemented {A = A} p dec = inv , intersection , union where inv : ℙ A - inv x = el (¬ (x ∈ p)) hlevel! + inv x = el (¬ (x ∈ p)) (hlevel 1) intersection : (p ∩ inv) ⊆ minimal intersection x (x∈p , x∉p) = x∉p x∈p @@ -102,7 +102,7 @@ subobject because $2$ has decidable equality. ```agda to : (A → Bool) → (Σ[ p ∈ ℙ A ] (is-decidable p)) - to map .fst x = el (map x ≡ true) hlevel! + to map .fst x = el (map x ≡ true) (hlevel 1) to map .snd p = Bool-elim (λ p → Dec (p ≡ true)) (yes refl) (no (λ p → true≠false (sym p))) (map p) ``` diff --git a/src/Data/Set/Coequaliser.lagda.md b/src/Data/Set/Coequaliser.lagda.md index 06c271979..7938f0f68 100644 --- a/src/Data/Set/Coequaliser.lagda.md +++ b/src/Data/Set/Coequaliser.lagda.md @@ -510,7 +510,7 @@ so the function $f^*x \to A/\ker f$ is constant, and factors through the g₀-const (_ , p) (_ , q) = quot (p ∙ sym q) g₁ : ∀ {x} → ∥ fibre f x ∥ → c.quotient - g₁ f = ∥-∥-rec-set hlevel! g₀ g₀-const f + g₁ f = ∥-∥-rec-set (hlevel 2) g₀ g₀-const f ``` Since each $\| f^*x \|$ is inhabited, all of these functions glue @@ -536,21 +536,28 @@ is a set, that means it's an equivalence. diff --git a/src/Data/Set/Material.lagda.md b/src/Data/Set/Material.lagda.md index 41bf77bf8..24b3bcce0 100644 --- a/src/Data/Set/Material.lagda.md +++ b/src/Data/Set/Material.lagda.md @@ -215,7 +215,7 @@ $i = a$! V-identity-system : ∀ {ℓ} → is-identity-system {A = V ℓ} (λ A B → A ⊆ B × B ⊆ A) λ a → (λ _ w → w) , λ _ w → w -V-identity-system = set-identity-system (λ x y → hlevel!) +V-identity-system = set-identity-system (λ x y → hlevel 1) λ { (a , b) → extensionality _ _ a b } ``` --> @@ -274,8 +274,8 @@ Presentation-is-prop {ℓ} {A} f P1 P2 = done where eqv : ∀ x → fibre g x ≃ fibre h x eqv x = prop-ext (gm x) (hm x) - (λ fib → ∥-∥-proj (hm x) (v' .fst x (u' .snd x (inc fib)))) - (λ fib → ∥-∥-proj (gm x) (u' .fst x (v' .snd x (inc fib)))) + (λ fib → ∥-∥-out (hm x) (v' .fst x (u' .snd x (inc fib)))) + (λ fib → ∥-∥-out (gm x) (u' .fst x (v' .snd x (inc fib)))) ``` This pointwise equivalence between fibres extends to an equivalence @@ -375,7 +375,7 @@ module Members {ℓ} (X : V ℓ) where memb : ∀ {x} → x ∈ X ≃ fibre elem x memb {x = x} = prop-ext (is-member _ X .is-tr) (embeds _) - (λ a → ∥-∥-proj (embeds _) (subst (x ∈_) presents a)) + (λ a → ∥-∥-out (embeds _) (subst (x ∈_) presents a)) (λ a → subst (x ∈_) (sym presents) (inc a)) module memb {x} = Equiv (memb {x}) @@ -465,7 +465,7 @@ F \simeq m_F^*(x)$. ```agda union : ∀ {x F} → x ∈ ⋃V F ≃ ∃ (V ℓ) λ u → x ∈ u × u ∈ F - union {x} {F} = prop-ext hlevel! squash + union {x} {F} = prop-ext! (∥-∥-map λ { ((i , j) , p) → Members.elem F i , Members.contains' (Members.elem F i) (sym p) @@ -618,8 +618,8 @@ $p$, a proof that $C$ holds of $x$. ```agda separation : ∀ a C (x : V ℓ) → (x ∈ subset a C) ≃ (x ∈ a × x ∈ C) - separation a C x = prop-ext squash hlevel! - (∥-∥-rec hlevel! λ { ((j , w) , p) → + separation a C x = prop-ext! + (∥-∥-rec! λ { ((j , w) , p) → Members.contains' a (sym p) , subst (λ e → ∣ C e ∣) p w }) (λ { (i∈a , Ci) → inc ( ( Members.memb.to a i∈a .fst @@ -670,8 +670,8 @@ construction of power set. deduplicate : (x ∈ a × x ∈ predicate→class p) ≃ Σ (fibre (Members.elem a) x) (λ f → f .fst ∈ p) - deduplicate = prop-ext hlevel! hp - (λ { (_ , pcx) → out! {pa = hp} pcx }) + deduplicate = prop-ext (hlevel 1) hp + (λ { (_ , pcx) → □-rec hp id pcx }) λ { (f , p) → Members.memb.from a f , inc (f , p) } ``` --> @@ -720,7 +720,7 @@ By transporting this last proof along the middle path, we conclude $x to : subset a (predicate→class belongs) ⊆ i to e e∈sub = subst (_∈ i) (Equiv.to (subset-separation belongs e) e∈sub .fst .snd) - (out! {pa = is-member _ i .is-tr} + (□-rec (is-member _ i .is-tr) id (Equiv.to (subset-separation belongs e) e∈sub .snd)) ``` @@ -735,7 +735,7 @@ m_a^*(x)$. It remains to show $m_a(k) \in i$; but this is equal to $x ( Members.memb.to a (i⊆a _ e∈i) , inc (subst (_∈ i) (sym (Members.memb.to a (i⊆a _ e∈i) .snd)) e∈i)) - done = prop-ext squash hlevel! (∥-∥-rec hlevel! p1) p2 + done = prop-ext! (∥-∥-rec! p1) p2 ``` ## Set induction diff --git a/src/Data/Set/Surjection.lagda.md b/src/Data/Set/Surjection.lagda.md index 7d5de6819..91ccc5aef 100644 --- a/src/Data/Set/Surjection.lagda.md +++ b/src/Data/Set/Surjection.lagda.md @@ -61,7 +61,7 @@ elimination principle for $\| f^*x \| \to F$, since $F$ is a set. surjective→regular-epi c d f surj .has-is-coeq = coeqs where go : ∀ {F} (e' : ∣ c ∣ → ∣ F ∣) p (x : ∣ d ∣) → ∥ fibre f x ∥ → ∣ F ∣ go e' p x = - ∥-∥-rec-set hlevel! (λ x → e' (x .fst)) + ∥-∥-rec-set (hlevel 2) (λ x → e' (x .fst)) (λ x y → p $ₚ (x .fst , y .fst , x .snd ∙ sym (y .snd))) ``` @@ -74,9 +74,9 @@ surjectivity out of the way, we get what we wanted. coeqs .universal {F} {e'} p x = go {F = F} e' p x (surj x) coeqs .factors {F} {e'} {p = p} = funext λ x → ∥-∥-elim {P = λ e → go {F} e' p (f x) e ≡ e' x} - (λ x → hlevel!) (λ e → p $ₚ (e .fst , x , e .snd)) (surj (f x)) + (λ x → hlevel 1) (λ e → p $ₚ (e .fst , x , e .snd)) (surj (f x)) coeqs .unique {F} {e'} {p} {colim} comm = funext λ a → - ∥-∥-elim {P = λ e → colim a ≡ go {F} e' p a e} (λ x → hlevel!) + ∥-∥-elim {P = λ e → colim a ≡ go {F} e' p a e} (λ x → hlevel 1) (λ x → ap colim (sym (x .snd)) ∙ comm $ₚ x .fst) (surj a) ``` @@ -135,14 +135,14 @@ $P' : \| \rm{Cofibre}(f) \|_0 \to \rm{Prop}$. ```agda P : Cofibre f → Prop _ - P tip = el (Lift _ ⊤) hlevel! - P (base x) = el ∥ fibre f x ∥ hlevel! + P tip = el! (Lift _ ⊤) + P (base x) = el! ∥ fibre f x ∥ P (cone a i) = - n-ua {X = el (Lift _ ⊤) hlevel!} {Y = el ∥ fibre f (f a) ∥ hlevel!} + n-ua {X = el! (Lift _ ⊤)} {Y = el! ∥ fibre f (f a) ∥} (prop-ext! (λ _ → inc (a , refl)) λ _ → lift tt) i P' : ∥ Cofibre f ∥₀ → Prop _ - P' = ∥-∥₀-elim (λ _ → hlevel!) P + P' = ∥-∥₀-elim (λ _ → hlevel 2) P ``` Letting $x$ be an element of the codomain, and since by assumption $f$'s diff --git a/src/Data/Set/Truncation.lagda.md b/src/Data/Set/Truncation.lagda.md index 56645120e..b6dcbaffb 100644 --- a/src/Data/Set/Truncation.lagda.md +++ b/src/Data/Set/Truncation.lagda.md @@ -1,5 +1,6 @@ diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md index 7a274c47a..5350a945b 100644 --- a/src/HoTT.lagda.md +++ b/src/HoTT.lagda.md @@ -354,12 +354,12 @@ _ = Axiom-of-choice ```agda _ = is-prop→equiv∥-∥ _ = ∥-∥-univ -_ = ∥-∥-proj +_ = ∥-∥-out ``` --> * Lemma 3.9.1: `is-prop→equiv∥-∥`{.Agda} -* Corollary 3.9.2: Implicit in e.g. `∥-∥-univ`{.Agda}, `∥-∥-proj`{.Agda} +* Corollary 3.9.2: Implicit in e.g. `∥-∥-univ`{.Agda}, `∥-∥-out`{.Agda} ### 3.11: Contractibility @@ -808,7 +808,6 @@ _ = is-invertible _ = _≅_ _ = is-invertible-is-prop _ = Cat[_,_] -_ = ≅-is-set _ = path→iso _ = is-category _ = equiv-path→identity-system @@ -829,7 +828,7 @@ _ = Sets-is-category * Definition 9.1.1: `Precategory`{.Agda} * Definition 9.1.2: `is-invertible`{.Agda}, `_≅_`{.Agda} -* Lemma 9.1.3: `is-invertible-is-prop`{.Agda}, `≅-is-set`{.Agda} +* Lemma 9.1.3: `is-invertible-is-prop`{.Agda} * Lemma 9.1.4: `path→iso`{.Agda} * Example 9.1.5: `Sets`{.Agda} * Definition 9.1.6^[We use a slightly different definition of univalence diff --git a/src/Homotopy/Connectedness.lagda.md b/src/Homotopy/Connectedness.lagda.md index 448133e8d..e5b5d06d8 100644 --- a/src/Homotopy/Connectedness.lagda.md +++ b/src/Homotopy/Connectedness.lagda.md @@ -91,7 +91,7 @@ module _ {ℓ} {X@(_ , pt) : Type∙ ℓ} where is-connected∙→is-connected c .centre = inc pt is-connected∙→is-connected c .paths = ∥-∥₀-elim (λ _ → is-hlevel-suc 2 squash (inc pt) _) λ x → - ∥-∥-rec! {pprop = squash _ _} (ap inc ∘ sym) (c x) + ∥-∥-rec! (ap inc ∘ sym) (c x) is-connected→is-connected∙ : is-connected ⌞ X ⌟ → is-connected∙ X is-connected→is-connected∙ c x = @@ -167,7 +167,7 @@ the general $n$-truncation uniformly. ```agda is-n-connected-Tr : ∀ {ℓ} {A : Type ℓ} n → is-n-connected A (suc n) → is-contr (n-Tr A (suc n)) -is-n-connected-Tr zero a-conn = ∥-∥-proj! do +is-n-connected-Tr zero a-conn = ∥-∥-out! do pt ← a-conn pure $ contr (inc pt) (λ x → n-Tr-is-hlevel 0 _ _) is-n-connected-Tr (suc zero) a-conn = @@ -184,7 +184,7 @@ is-n-connected-Tr (suc (suc n)) a-conn = a-conn is-n-connected-Tr-is-equiv : ∀ {ℓ} {A : Type ℓ} n → is-equiv (is-n-connected-Tr {A = A} n) is-n-connected-Tr-is-equiv {A = A} n = prop-ext (is-n-connected-is-prop _) (hlevel 1) _ (from n) .snd where from : ∀ n → is-contr (n-Tr A (suc n)) → is-n-connected A (suc n) - from zero c = n-Tr-elim (λ _ → ∥ A ∥) (λ _ → squash) inc (c .centre) + from zero c = n-Tr-rec! inc (c .centre) from (suc zero) = retract→is-hlevel 0 (n-Tr-rec! inc) (∥-∥₀-rec (n-Tr-is-hlevel 1) inc) (∥-∥₀-elim (λ _ → is-prop→is-set (squash _ _)) λ _ → refl) @@ -243,7 +243,7 @@ _ = is-hlevel-suc Path-is-connected : ∀ n → is-n-connected A (suc n) → is-n-connected (Path A x y) n Path-is-connected 0 = _ Path-is-connected {x = x} (suc n) conn = n-connected.from n (contr (ps _ _) $ - n-Tr-elim _ (λ _ → hlevel!) + n-Tr-elim! _ (J (λ y p → ps x y ≡ inc p) (Equiv.injective (Equiv.inverse n-Tr-path-equiv) (is-contr→is-set (is-n-connected-Tr _ conn) _ _ _ _)))) where @@ -255,7 +255,7 @@ is-connected-suc → is-n-connected A (suc n) → is-n-connected A n is-connected-suc {A = A} zero _ = _ is-connected-suc {A = A} (suc n) w = n-connected.from n $ n-Tr-elim! _ - (λ x → contr (inc x) (n-Tr-elim _ (λ _ → hlevel!) (rem₁ n w x))) + (λ x → contr (inc x) (n-Tr-elim! _ (rem₁ n w x))) (is-n-connected-Tr (suc n) w .centre) where rem₁ : ∀ n → is-n-connected A (2 + n) → ∀ x y → Path (n-Tr A (suc n)) (inc x) (inc y) @@ -311,7 +311,7 @@ is-contr-n-Tr→∥-∥ (suc n) h .snd a b = is-contr-n-Tr→∥-∥ n ∥-∥→is-contr-n-Tr : ∀ n → is-n-connected-∥-∥ A (suc n) → is-contr (n-Tr A (suc n)) -∥-∥→is-contr-n-Tr zero (a , _) = is-prop∙→is-contr hlevel! (∥-∥-rec! inc a) +∥-∥→is-contr-n-Tr zero (a , _) = is-prop∙→is-contr (hlevel 1) (∥-∥-rec! inc a) ∥-∥→is-contr-n-Tr (suc n) (a , h) = ∥-∥-rec! (λ a → is-prop∙→is-contr (n-Tr-elim! _ λ a → n-Tr-elim! _ λ b → Equiv.from n-Tr-path-equiv (∥-∥→is-contr-n-Tr n (h a b) .centre)) @@ -390,7 +390,7 @@ n-type-const→is-n-connected n-type-const→is-n-connected {A = A} n eqv = n-connected.from n $ contr (rem.from inc) $ n-Tr-elim _ (λ h → Path-is-hlevel (suc n) (n-Tr-is-hlevel n)) (rem.ε inc $ₚ_) - where module rem = Equiv (_ , eqv {n-Tr A (suc n)} hlevel!) + where module rem = Equiv (_ , eqv {n-Tr A (suc n)} (hlevel _)) ``` We can now generalise this to work with an $n$-connected map $f : A \to diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md index 67b84b0e7..aefac7f8c 100644 --- a/src/Homotopy/Space/Delooping.lagda.md +++ b/src/Homotopy/Space/Delooping.lagda.md @@ -164,7 +164,7 @@ specification. base-case : Set ℓ ∣ base-case ∣ = ⌞ G ⌟ - base-case .is-tr = hlevel! + base-case .is-tr = hlevel 2 ``` To handle the path case, we'll have to produce, given an element $x : @@ -356,7 +356,7 @@ of a loop with arbitrary base. diff --git a/src/Homotopy/Space/Suspension/Properties.lagda.md b/src/Homotopy/Space/Suspension/Properties.lagda.md index 95ea1ef03..cb56cc109 100644 --- a/src/Homotopy/Space/Suspension/Properties.lagda.md +++ b/src/Homotopy/Space/Suspension/Properties.lagda.md @@ -30,7 +30,7 @@ Susp-is-connected : ∀ {ℓ} {A : Type ℓ} n → is-n-connected A n → is-n-connected (Susp A) (suc n) Susp-is-connected 0 a-conn = inc N -Susp-is-connected 1 a-conn = ∥-∥-proj! do +Susp-is-connected 1 a-conn = ∥-∥-out! do pt ← a-conn pure $ is-connected∙→is-connected λ where N → inc refl @@ -52,7 +52,7 @@ Susp-is-connected {A = A} (suc (suc n)) a-conn = rem₁ : is-equiv λ b a → b rem₁ = is-n-connected→n-type-const {B = n-Tr.inc {n = 3 + n} N ≡ inc S} {A = A} - (suc n) hlevel! a-conn + (suc n) (hlevel (2 + n)) a-conn rem₂ : Σ (inc N ≡ inc S) (λ p → ∀ x → ap n-Tr.inc (merid x) ≡ p) rem₂ = _ , λ x → sym (rem₁ .is-eqv _ .centre .snd) $ₚ x @@ -154,9 +154,9 @@ We've defined a reflexive family of propositions: ```agda Code-is-prop : ∀ a b → is-prop (Code a b) - Code-is-prop = Susp-elim-prop hlevel! - (Susp-elim-prop hlevel! hlevel! prop) - (Susp-elim-prop hlevel! prop hlevel!) + Code-is-prop = Susp-elim-prop (λ _ → hlevel 1) + (Susp-elim-prop (λ _ → hlevel 1) (hlevel 1) prop) + (Susp-elim-prop (λ _ → hlevel 1) prop (hlevel 1)) Code-refl : ∀ a → Code a a Code-refl = Susp-elim-prop (λ a → Code-is-prop a a) _ _ diff --git a/src/Homotopy/Truncation.lagda.md b/src/Homotopy/Truncation.lagda.md index 6fdca52c1..31915867b 100644 --- a/src/Homotopy/Truncation.lagda.md +++ b/src/Homotopy/Truncation.lagda.md @@ -2,6 +2,7 @@ ```agda open import 1Lab.Prelude +open import Data.Nat.Base open import Data.List using (_∷_ ; []) open import Homotopy.Space.Suspension @@ -130,8 +131,8 @@ n-Tr-is-hlevel n-Tr-is-hlevel n = hubs-and-spokes→hlevel n λ sph → hub sph , spokes sph instance - n-tr-decomp : ∀ {ℓ} {A : Type ℓ} {n} → hlevel-decomposition (n-Tr A (suc n)) - n-tr-decomp = decomp (quote n-Tr-is-hlevel) (`level-minus 1 ∷ []) + H-Level-n-Tr : ∀ {ℓ} {A : Type ℓ} {n k} ⦃ _ : suc n ≤ k ⦄ → H-Level (n-Tr A (suc n)) k + H-Level-n-Tr {k = _} ⦃ p ⦄ = hlevel-instance $ is-hlevel-le _ _ p (n-Tr-is-hlevel _) n-Tr-elim : ∀ {ℓ ℓ'} {A : Type ℓ} {n} @@ -163,16 +164,16 @@ n-Tr-elim {A = A} {n} P ptrunc pbase = go where n-Tr-elim! : ∀ {ℓ ℓ'} {A : Type ℓ} {n} → (P : n-Tr A (suc n) → Type ℓ') - → {@(tactic hlevel-tactic-worker) hl : ∀ x → is-hlevel (P x) (suc n)} + → ⦃ _ : ∀ {x} → H-Level (P x) (suc n) ⦄ → (∀ x → P (inc x)) → ∀ x → P x -n-Tr-elim! P {hl} f = n-Tr-elim P hl f +n-Tr-elim! P f = n-Tr-elim P (λ x → hlevel _) f n-Tr-rec! : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} - → {@(tactic hlevel-tactic-worker) hl : is-hlevel B (suc n)} + → ⦃ hl : H-Level B (suc n) ⦄ → (A → B) → n-Tr A (suc n) → B -n-Tr-rec! {hl = hl} = n-Tr-elim (λ _ → _) (λ _ → hl) +n-Tr-rec! = n-Tr-elim (λ _ → _) (λ _ → hlevel _) ``` --> @@ -216,10 +217,7 @@ $(2+n)$-type. ```agda code : (x : A) (y' : n-Tr A (2 + n)) → n-Type _ (suc n) - code x = - n-Tr-elim! - (λ y' → n-Type _ (suc n)) - (λ y' → el! (n-Tr (Path A x y') (suc n))) + code x = n-Tr-rec! λ y' → el! (n-Tr (Path A x y') (suc n)) ``` The rest of the proof boils down to applications of `path @@ -230,14 +228,10 @@ induction`{.Agda id=J} and the induction principle for $\|A\|_{n+2}$. encode' x _ = J (λ y _ → ∣ code x y ∣) (inc refl) decode' : ∀ x y → ∣ code x y ∣ → inc x ≡ y - decode' x = - n-Tr-elim! _ λ x → n-Tr-rec hlevel! (ap inc) + decode' x = n-Tr-elim! _ λ x → n-Tr-rec! (ap inc) rinv : ∀ x y → is-right-inverse (decode' x y) (encode' x y) - rinv x = n-Tr-elim _ - (λ y → Π-is-hlevel (2 + n) - (λ c → Path-is-hlevel (2 + n) (is-hlevel-suc (suc n) (code x y .is-tr)))) - λ x → n-Tr-elim! _ λ p → ap n-Tr.inc (subst-path-right _ _ ∙ ∙-idl _) + rinv x = n-Tr-elim! _ λ x → n-Tr-elim! _ λ p → ap n-Tr.inc (subst-path-right _ _ ∙ ∙-idl _) linv : ∀ x y → is-left-inverse (decode' x y) (encode' x y) linv x _ = J (λ y p → decode' x y (encode' x y p) ≡ p) @@ -284,10 +278,9 @@ n-Tr-product {A = A} {B} {n} = distrib , distrib-is-equiv module n-Tr-product wh distrib-is-iso : is-iso distrib distrib-is-iso .inv (x , y) = pair x y - distrib-is-iso .rinv (x , y) = n-Tr-elim + distrib-is-iso .rinv (x , y) = n-Tr-elim! (λ x → ∀ y → distrib (pair x y) ≡ (x , y)) - (λ _ → Π-is-hlevel (suc n) λ x → Path-is-hlevel (suc n) (×-is-hlevel (suc n) hlevel! hlevel!)) - (λ x → n-Tr-elim _ (λ y → Path-is-hlevel (suc n) (×-is-hlevel (suc n) hlevel! hlevel!)) λ y → refl) + (λ x → n-Tr-elim! _ λ y → refl) x y distrib-is-iso .linv = n-Tr-elim! _ λ x → refl diff --git a/src/Logic/Propositional/Classical/Compactness.lagda.md b/src/Logic/Propositional/Classical/Compactness.lagda.md index 880e0df69..f87d56274 100644 --- a/src/Logic/Propositional/Classical/Compactness.lagda.md +++ b/src/Logic/Propositional/Classical/Compactness.lagda.md @@ -118,7 +118,7 @@ We will set the `
`{.html} aside for the curious reader. let (ϕ , ϕ∈ϕs') = enum.from 0 sub ϕ ϕ∈ϕs' <&> λ where (inl xp) → - (λ _ → true) , λ ϕ' ϕ'∈ϕs' → ∥-∥-proj! do + (λ _ → true) , λ ϕ' ϕ'∈ϕs' → ∥-∥-out! do sub ϕ' ϕ'∈ϕs' >>= λ where (inl xp') → □-tr do (x=ϕ' , _) ← xp' @@ -128,7 +128,7 @@ We will set the `
`{.html} aside for the curious reader. (_ , ¬p) ← ¬xp' absurd (¬p p) (inr ¬xp) → - (λ _ → false) , λ ϕ' ϕ'∈ϕs' → ∥-∥-proj! do + (λ _ → false) , λ ϕ' ϕ'∈ϕs' → ∥-∥-out! do sub ϕ' ϕ'∈ϕs' >>= λ where (inl xp') → □-tr do (_ , ¬p) ← ¬xp @@ -218,7 +218,7 @@ If we put this all together, then we can decide $\neg P$! ```agda ¬P∨¬¬P : Dec (¬ ∣ P ∣) - ¬P∨¬¬P = ∥-∥-proj! do + ¬P∨¬¬P = ∥-∥-out! do (ρ , ρ-sat) ← compact ([x∣P] ∪ [¬x∣¬P]) finitely-consistent pure $ Bool-elim (λ b → ρ 0 ≡ b → Dec (¬ ∣ P ∣)) diff --git a/src/Order/Base.lagda.md b/src/Order/Base.lagda.md index f7a0d362b..1afa2c097 100644 --- a/src/Order/Base.lagda.md +++ b/src/Order/Base.lagda.md @@ -202,20 +202,13 @@ nondecreasing sequences of elements in $P$. ```agda open Monotone public -private - variable - o ℓ o' ℓ' o'' ℓ'' : Level - P Q R : Poset o ℓ +private variable + o ℓ o' ℓ' o'' ℓ'' : Level + P Q R : Poset o ℓ -Monotone-is-hlevel : ∀ n → is-hlevel (Monotone P Q) (2 + n) -Monotone-is-hlevel {Q = Q} n = - Iso→is-hlevel (2 + n) eqv $ is-set→is-hlevel+2 $ hlevel! - where unquoteDecl eqv = declare-record-iso eqv (quote Monotone) +unquoteDecl H-Level-Monotone = declare-record-hlevel 2 H-Level-Monotone (quote Monotone) instance - H-Level-Monotone : ∀ {n} → H-Level (Monotone P Q) (2 + n) - H-Level-Monotone = basic-instance 2 (Monotone-is-hlevel 0) - Funlike-Monotone : Funlike (Monotone P Q) ⌞ P ⌟ λ _ → ⌞ Q ⌟ Funlike-Monotone = record { _#_ = hom } @@ -235,18 +228,13 @@ Monotone-pathp {P = P} {Q} {f} {g} q i .Monotone.pres-≤ {x} {y} α = (λ _ _ α → f .Monotone.pres-≤ α) (λ _ _ α → g .Monotone.pres-≤ α) i x y α -Extensional-Monotone - : ∀ {o ℓ o' ℓ' ℓr} {P : Poset o ℓ} {Q : Poset o' ℓ'} - → ⦃ sa : Extensional (⌞ P ⌟ → ⌞ Q ⌟) ℓr ⦄ - → Extensional (Monotone P Q) ℓr -Extensional-Monotone {Q = Q} ⦃ sa ⦄ = - injection→extensional! Monotone-pathp sa - instance - Extensionality-Monotone - : ∀ {o ℓ o' ℓ'} {P : Poset o ℓ} {Q : Poset o' ℓ'} - → Extensionality (Monotone P Q) - Extensionality-Monotone = record { lemma = quote Extensional-Monotone } + Extensional-Monotone + : ∀ {o ℓ o' ℓ' ℓr} {P : Poset o ℓ} {Q : Poset o' ℓ'} + → ⦃ sa : Extensional (⌞ P ⌟ → ⌞ Q ⌟) ℓr ⦄ + → Extensional (Monotone P Q) ℓr + Extensional-Monotone {Q = Q} ⦃ sa ⦄ = + injection→extensional! Monotone-pathp sa ``` --> @@ -265,9 +253,9 @@ _∘ₘ_ : Monotone Q R → Monotone P Q → Monotone P R (f ∘ₘ g) .pres-≤ x≤y = f .pres-≤ (g .pres-≤ x≤y) Posets : ∀ (o ℓ : Level) → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ) -Posets o ℓ .Precategory.Ob = Poset o ℓ -Posets o ℓ .Precategory.Hom = Monotone -Posets o ℓ .Precategory.Hom-set = hlevel! +Posets o ℓ .Precategory.Ob = Poset o ℓ +Posets o ℓ .Precategory.Hom = Monotone +Posets o ℓ .Precategory.Hom-set _ _ = hlevel 2 Posets o ℓ .Precategory.id = idₘ Posets o ℓ .Precategory._∘_ = _∘ₘ_ @@ -291,7 +279,7 @@ evidently extends to a faithful functor $\Pos \to \Sets$. ```agda Forget-poset : ∀ {o ℓ} → Functor (Posets o ℓ) (Sets o) ∣ Forget-poset .Functor.F₀ P ∣ = ⌞ P ⌟ -Forget-poset .Functor.F₀ P .is-tr = hlevel! +Forget-poset .Functor.F₀ P .is-tr = hlevel 2 Forget-poset .Functor.F₁ = hom @@ -321,7 +309,7 @@ We can construct the trivial posets with one and zero (object(s), ordering(s)) r 𝟙ᵖ : ∀ {o ℓ} → Poset o ℓ 𝟙ᵖ .Poset.Ob = Lift _ ⊤ 𝟙ᵖ .Poset._≤_ _ _ = Lift _ ⊤ -𝟙ᵖ .Poset.≤-thin = hlevel! +𝟙ᵖ .Poset.≤-thin = hlevel 1 𝟙ᵖ .Poset.≤-refl = lift tt 𝟙ᵖ .Poset.≤-trans = λ _ _ → lift tt 𝟙ᵖ .Poset.≤-antisym = λ _ _ → refl @@ -333,5 +321,4 @@ We can construct the trivial posets with one and zero (object(s), ordering(s)) r 𝟘ᵖ .Poset.≤-refl {()} 𝟘ᵖ .Poset.≤-trans () 𝟘ᵖ .Poset.≤-antisym () - ``` diff --git a/src/Order/DCPO.lagda.md b/src/Order/DCPO.lagda.md index 9e1f2961b..d055fb3d8 100644 --- a/src/Order/DCPO.lagda.md +++ b/src/Order/DCPO.lagda.md @@ -1,6 +1,6 @@ -```agda - is-dcpo-is-prop : is-prop (is-dcpo P) - is-dcpo-is-prop = Iso→is-hlevel 1 eqv hlevel! - where unquoteDecl eqv = declare-record-iso eqv (quote is-dcpo) -``` - # Scott-continuous functions Let $(P, \le)$ and $(Q, \lsq)$ be a pair of posets. A monotone map $f : @@ -120,7 +112,7 @@ module _ {P Q : Poset o ℓ} where is-scott-continuous-is-prop : ∀ (f : Posets.Hom P Q) → is-prop (is-scott-continuous f) - is-scott-continuous-is-prop = hlevel! + is-scott-continuous-is-prop _ = hlevel 1 ``` If $(P, \le)$ is a DCPO, then any function $f : P \to Q$ which preserves @@ -235,7 +227,7 @@ DCPOs : ∀ (o ℓ : Level) → Precategory (lsuc (o ⊔ ℓ)) (lsuc o ⊔ ℓ) DCPOs o ℓ = Subcategory (DCPOs-subcat o ℓ) DCPOs-is-category : ∀ {o ℓ} → is-category (DCPOs o ℓ) -DCPOs-is-category = subcat-is-category Posets-is-category (λ _ → is-dcpo-is-prop) +DCPOs-is-category = subcat-is-category Posets-is-category (λ _ → hlevel 1) ``` ```agda - ⊑-lub-le : ∀ i → s i ⊑ ⊑-lub set s dir + ⊑-lub-le : ∀ i → s i ⊑ ⊑-lub s dir ⊑-lub-le i .implies si = inc (i , si) ⊑-lub-le i .refines si = refl ⊑-lub-least - : ∀ x → (∀ i → s i ⊑ x) → ⊑-lub set s dir ⊑ x + : ∀ x → (∀ i → s i ⊑ x) → ⊑-lub s dir ⊑ x ⊑-lub-least x le .implies = □-rec! λ (i , si) → le i .implies si - ⊑-lub-least x le .refines = □-elim (λ _ → set _ _) λ (i , si) → + ⊑-lub-least x le .refines = □-elim! λ (i , si) → le i .refines si ``` @@ -218,7 +218,7 @@ open Lub ```agda Parts-is-dcpo : ∀ {A : Set ℓ} → is-dcpo (Parts A) Parts-is-dcpo {A = A} .directed-lubs s dir .lub = - ⊑-lub (A .is-tr) s (dir .semidirected) + ⊑-lub s (dir .semidirected) Parts-is-dcpo {A = A} .directed-lubs s dir .has-lub .fam≤lub = ⊑-lub-le Parts-is-dcpo {A = A} .directed-lubs s dir .has-lub .least = ⊑-lub-least @@ -248,12 +248,12 @@ part-map-lub : {Ix : Type ℓ} {A : Set o} {B : Set o'} {s : Ix → ↯ ∣ A ∣} → {dir : ∀ i j → ∃[ k ∈ Ix ] (s i ⊑ s k × s j ⊑ s k)} → (f : ∣ A ∣ → ∣ B ∣) - → is-lub (Parts B) (part-map f ⊙ s) (part-map f (⊑-lub (A .is-tr) s dir)) + → is-lub (Parts B) (part-map f ⊙ s) (part-map f (⊑-lub s dir)) part-map-lub f .fam≤lub i = part-map-⊑ (⊑-lub-le i) part-map-lub f .least y le .implies = □-rec! λ (i , si) → le i .implies si part-map-lub {B = B} f .least y le .refines = - □-elim (λ _ → B .is-tr _ _) λ (i , si) → le i .refines si + □-elim! λ (i , si) → le i .refines si Free-Pointed-dcpo : Functor (Sets ℓ) (Pointed-DCPOs ℓ ℓ) Free-Pointed-dcpo .F₀ A = Parts-pointed-dcpo A @@ -289,7 +289,7 @@ $$. part-counit : ↯ Ob → Ob part-counit x = ⋃-prop (x .elt ⊙ Lift.lower) def-prop where abstract def-prop : is-prop (Lift o ⌞ x ⌟) - def-prop = hlevel! + def-prop = hlevel 1 ``` We can characterise the behaviour of this definition as though it were @@ -318,7 +318,7 @@ The following three properties are fundamental: the counit part-counit-⊑ : ∀ {x y} → x ⊑ y → part-counit x ≤ part-counit y part-counit-lub : ∀ {Ix} s (sdir : is-semidirected-family (Parts set) {Ix} s) - → is-lub poset (part-counit ⊙ s) (part-counit (⊑-lub (set .is-tr) s sdir)) + → is-lub poset (part-counit ⊙ s) (part-counit (⊑-lub s sdir)) part-counit-never : ∀ x → part-counit never ≤ x ``` @@ -336,7 +336,7 @@ curious reader.
 ⋃-prop-least _ _ _ λ (lift p) → ⋃-prop-le _ _ (lift (inc (i , p))) part-counit-lub {Ix = Ix} s sdir .is-lub.least y le = ⋃-prop-least _ _ _ $ - λ (lift p) → □-elim (λ p → ≤-thin {x = ⊑-lub _ s sdir .elt p}) (λ (i , si) → + λ (lift p) → □-elim (λ p → ≤-thin {x = ⊑-lub s sdir .elt p}) (λ (i , si) → s i .elt si ≤⟨ ⋃-prop-le _ _ (lift si) ⟩ ⋃-prop _ _ ≤⟨ le i ⟩ y ≤∎) p diff --git a/src/Order/Diagram/Bottom.lagda.md b/src/Order/Diagram/Bottom.lagda.md index 8b50663fe..51ac10062 100644 --- a/src/Order/Diagram/Bottom.lagda.md +++ b/src/Order/Diagram/Bottom.lagda.md @@ -53,7 +53,7 @@ is-lub→is-bottom lub x = lub .least x λ () @@ -284,7 +269,7 @@ of the category of posets. Frame-subcat : ∀ o ℓ → Subcat (Posets o ℓ) _ _ Frame-subcat o ℓ .Subcat.is-ob = is-frame Frame-subcat o ℓ .Subcat.is-hom = is-frame-hom -Frame-subcat o ℓ .Subcat.is-hom-prop = hlevel! +Frame-subcat o ℓ .Subcat.is-hom-prop _ _ _ = hlevel 1 Frame-subcat o ℓ .Subcat.is-hom-id = id-frame-hom Frame-subcat o ℓ .Subcat.is-hom-∘ = ∘-frame-hom diff --git a/src/Order/Frame/Free.lagda.md b/src/Order/Frame/Free.lagda.md index 19cf8c02b..3dfbe54c5 100644 --- a/src/Order/Frame/Free.lagda.md +++ b/src/Order/Frame/Free.lagda.md @@ -1,6 +1,6 @@ @@ -201,7 +182,7 @@ of the category of posets. Lattices-subcat : ∀ o ℓ → Subcat (Posets o ℓ) _ _ Lattices-subcat o ℓ .Subcat.is-ob = is-lattice Lattices-subcat o ℓ .Subcat.is-hom = is-lattice-hom -Lattices-subcat o ℓ .Subcat.is-hom-prop = hlevel! +Lattices-subcat o ℓ .Subcat.is-hom-prop _ _ _ = hlevel 1 Lattices-subcat o ℓ .Subcat.is-hom-id = id-lattice-hom Lattices-subcat o ℓ .Subcat.is-hom-∘ = ∘-lattice-hom diff --git a/src/Order/Semilattice/Join.lagda.md b/src/Order/Semilattice/Join.lagda.md index a3ca671a6..a7197ecb2 100644 --- a/src/Order/Semilattice/Join.lagda.md +++ b/src/Order/Semilattice/Join.lagda.md @@ -144,19 +144,7 @@ record open is-join-slat-hom -abstract - is-join-slat-hom-is-prop - : ∀ {P : Poset o ℓ} {Q : Poset o' ℓ'} {f : Monotone P Q} {P-slat Q-slat} - → is-prop (is-join-slat-hom f P-slat Q-slat) - is-join-slat-hom-is-prop = - Iso→is-hlevel 1 eqv hlevel! - where unquoteDecl eqv = declare-record-iso eqv (quote is-join-slat-hom) - -instance - H-Level-is-join-slat-hom - : ∀ {f : Monotone P Q} {P-slat Q-slat n} - → H-Level (is-join-slat-hom f P-slat Q-slat) (suc n) - H-Level-is-join-slat-hom = prop-instance is-join-slat-hom-is-prop +unquoteDecl H-Level-is-join-slat-hom = declare-record-hlevel 1 H-Level-is-join-slat-hom (quote is-join-slat-hom) open Poset ``` @@ -195,7 +183,7 @@ id-join-slat-hom {P = P} _ .bot-≤ = P .≤-refl Join-slats-subcat : ∀ o ℓ → Subcat (Posets o ℓ) (o ⊔ ℓ) (o ⊔ ℓ) Join-slats-subcat o ℓ .Subcat.is-ob = is-join-semilattice Join-slats-subcat o ℓ .Subcat.is-hom = is-join-slat-hom -Join-slats-subcat o ℓ .Subcat.is-hom-prop = hlevel! +Join-slats-subcat o ℓ .Subcat.is-hom-prop _ _ _ = hlevel 1 Join-slats-subcat o ℓ .Subcat.is-hom-id = id-join-slat-hom Join-slats-subcat o ℓ .Subcat.is-hom-∘ = ∘-join-slat-hom diff --git a/src/Order/Semilattice/Meet.lagda.md b/src/Order/Semilattice/Meet.lagda.md index 1914211a1..a624a2597 100644 --- a/src/Order/Semilattice/Meet.lagda.md +++ b/src/Order/Semilattice/Meet.lagda.md @@ -150,20 +150,7 @@ record open is-meet-slat-hom -abstract - is-meet-slat-hom-is-prop - : ∀ {P : Poset o ℓ} {Q : Poset o' ℓ'} {f : Monotone P Q} - {P-slat Q-slat} - → is-prop (is-meet-slat-hom f P-slat Q-slat) - is-meet-slat-hom-is-prop = - Iso→is-hlevel 1 eqv hlevel! - where unquoteDecl eqv = declare-record-iso eqv (quote is-meet-slat-hom) - -instance - H-Level-is-meet-slat-hom - : ∀ {f : Monotone P Q} {P-slat Q-slat n} - → H-Level (is-meet-slat-hom f P-slat Q-slat) (suc n) - H-Level-is-meet-slat-hom = prop-instance is-meet-slat-hom-is-prop +unquoteDecl H-Level-is-meet-slat-hom = declare-record-hlevel 1 H-Level-is-meet-slat-hom (quote is-meet-slat-hom) ``` --> @@ -191,7 +178,7 @@ id-meet-slat-hom {P = P} _ .top-≤ = Poset.≤-refl P Meet-slats-subcat : ∀ o ℓ → Subcat (Posets o ℓ) (o ⊔ ℓ) (o ⊔ ℓ) Meet-slats-subcat o ℓ .Subcat.is-ob = is-meet-semilattice Meet-slats-subcat o ℓ .Subcat.is-hom = is-meet-slat-hom -Meet-slats-subcat o ℓ .Subcat.is-hom-prop = hlevel! +Meet-slats-subcat o ℓ .Subcat.is-hom-prop _ _ _ = hlevel 1 Meet-slats-subcat o ℓ .Subcat.is-hom-id = id-meet-slat-hom Meet-slats-subcat o ℓ .Subcat.is-hom-∘ = ∘-meet-slat-hom diff --git a/src/Order/Univalent.lagda.md b/src/Order/Univalent.lagda.md index c64062a71..125de99b8 100644 --- a/src/Order/Univalent.lagda.md +++ b/src/Order/Univalent.lagda.md @@ -111,10 +111,10 @@ The definition above corresponds to the top face in the square diff --git a/support/nix/dep/Agda/github.json b/support/nix/dep/Agda/github.json index 5538094ab..bbc61dfc7 100644 --- a/support/nix/dep/Agda/github.json +++ b/support/nix/dep/Agda/github.json @@ -3,6 +3,6 @@ "repo": "agda", "branch": "master", "private": false, - "rev": "aa5d8bbe723ea095d2af92ccaa2cfd2fbd89570a", - "sha256": "1czn8l2zn213nipzbmksakjsqxza07npcz5r5rlk41k61hvxc10n" + "rev": "403ee4263e0f14222956e398d2610ae1a4f05467", + "sha256": "09rbhysb06xbpw4hak69skxhdpcdxwj451rlgbk76dksa6rkk8wm" } diff --git a/support/shake/app/HTML/Backend.hs b/support/shake/app/HTML/Backend.hs index e0cb55746..67525f545 100644 --- a/support/shake/app/HTML/Backend.hs +++ b/support/shake/app/HTML/Backend.hs @@ -305,7 +305,7 @@ usedInstances = I.Def q _ -> do def <- getConstInfo q case Agda.Compiler.Backend.defInstance def of - Just c -> Set.insert q <$> getClass c + Just c -> Set.insert q <$> getClass (instanceClass c) Nothing -> pure mempty _ -> pure mempty