From cd46ec7838ceb26380c61ad09de1008a93924f90 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 27 Mar 2024 08:39:05 -0300 Subject: [PATCH 1/7] chore: bump agda --- support/nix/dep/Agda/github.json | 4 ++-- support/shake/app/HTML/Backend.hs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) 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 From b8547b4f501bad6165bb3f053847525cb6b28cac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 27 Mar 2024 11:46:30 -0300 Subject: [PATCH 2/7] chore: get rid of Extensionality w/w --- src/1Lab/Extensionality.agda | 349 ++++++------------ src/Algebra/Group/Ab/Tensor.lagda.md | 22 +- src/Algebra/Group/Subgroup.lagda.md | 19 +- src/Algebra/Ring/Module.lagda.md | 24 +- src/Algebra/Ring/Module/Action.lagda.md | 12 +- src/Algebra/Ring/Module/Free.lagda.md | 35 +- src/Cat/Base.lagda.md | 58 +-- src/Cat/Diagram/Monad.lagda.md | 25 +- src/Cat/Displayed/Univalence/Thin.lagda.md | 21 +- src/Cat/Functor/Base.lagda.md | 6 +- src/Cat/Functor/Subcategory.lagda.md | 13 +- src/Cat/Functor/WideSubcategory.lagda.md | 32 +- src/Cat/Instances/Elements.lagda.md | 38 +- src/Cat/Instances/Elements/Covariant.lagda.md | 27 +- src/Cat/Instances/Slice.lagda.md | 27 +- src/Cat/Monoidal/Instances/Day.lagda.md | 46 +-- src/Cat/Morphism.lagda.md | 12 +- src/Cat/Morphism/Extensionality.agda | 23 -- src/Cat/Prelude.agda | 2 - src/Cat/Univalent/Rezk.lagda.md | 2 + src/Data/Set/Coequaliser.lagda.md | 37 +- src/Order/Base.lagda.md | 18 +- src/Order/DCPO.lagda.md | 2 +- src/Order/DCPO/Free.lagda.md | 4 +- 24 files changed, 326 insertions(+), 528 deletions(-) delete mode 100644 src/Cat/Morphism/Extensionality.agda diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda index 3f35b13e0..446ae1cf9 100644 --- a/src/1Lab/Extensionality.agda +++ b/src/1Lab/Extensionality.agda @@ -18,217 +18,84 @@ open import Data.Nat.Base module 1Lab.Extensionality where -record Extensional {ℓ} (A : Type ℓ) (ℓ-rel : Level) : Typeω where +record Extensional {ℓ} (A : Type ℓ) (ℓ-rel : Level) : Type (ℓ ⊔ lsuc ℓ-rel) where no-eta-equality field Pathᵉ : A → A → Type ℓ-rel reflᵉ : ∀ x → Pathᵉ x x idsᵉ : is-identity-system Pathᵉ reflᵉ -record Extensionality {ℓ} (A : Type ℓ) : Type where - field lemma : Name - -{- -The 'Extensional' and 'Extensionality' classes both function to equip a -type with a preferred choice of identity system. The idea is that -'Extensional' actually carries the data, and 'Extensionality' is a -pointer to the 'Extensional' instance. - -We use tactic arguments to implement default instances: since Agda will -happily call tactic arguments inside get-instances, if we had Extensional -instances with Extensional superclasses, this would lead to a -super-exponential amount of work being done: *every Extensional -instance*, including the "instance context", would have its full -instantiation computed before being added to the list of possible -instances. - -Instead the macro looks for 'Extensionality' instances, which *have no -'Extensionality' class constraints*, and unfolds those to get the -"actual" 'Extensional' instance. --} - open Extensional using (Pathᵉ ; reflᵉ ; idsᵉ) public --- Default instance, uses regular paths for the relation. -Extensional-default : ∀ {ℓ} {A : Type ℓ} → Extensional A ℓ -Extensional-default .Pathᵉ = _≡_ -Extensional-default .reflᵉ _ = refl -Extensional-default .idsᵉ = Path-identity-system - --- Find a value of 'Extensional' by looking at instances of 'Extensionality'. -find-extensionality : Term → TC Term -find-extensionality tm = do - -- We have to block on the full type being available to prevent a - -- situation where the default instance (or an incorrect instance!) is - -- picked because the type is meta-headed. - debugPrint "tactic.extensionality.top" 10 "entering extensionality tactic" - debugPrint "tactic.extensionality" 10 (" find-extensionality type:\n " ∷ termErr tm ∷ []) - tm ← reduce =<< wait-for-type tm - let search = it Extensionality ##ₙ tm - - resetting $ do - (mv , _) ← new-meta' search - get-instances mv >>= λ where - (x ∷ _) → do - it ← unquoteTC {A = Name} =<< normalise (it Extensionality.lemma ##ₙ x) - debugPrint "tactic.extensionality" 10 (" ⇒ found lemma " ∷ nameErr it ∷ []) - pure (def it []) - [] → do - debugPrint "tactic.extensionality" 10 " ⇒ using default" - pure (it Extensional-default) - --- Entry point for getting hold of an 'Extensional' instance: -extensional : ∀ {ℓ} (A : Type ℓ) → Term → TC ⊤ -extensional A goal = do - `A ← quoteTC A - check-type goal $ it Extensional ##ₙ `A ##ₙ unknown - unify goal =<< find-extensionality `A - -{- -Unlike extensional, which is parametrised by a type, extensionalᶠ -can be parametrised by a function (of arbitrary arity) into types, -even though its type doesn't properly reflect this. It will discharge -goals like - - ∀ x → Extensional (P x) ℓ - -by getting rid of every Π in the type and looking in an extended -context. It's also possible to use ⦃ _ : ∀ {x} → Extensional (P x) ℓ ⦄, -since Agda supports commuting those by itself. However, using -extensionalᶠ blocks more aggressively, which is required for touchy -instances like Extensional-natural-transformation. --} -extensionalᶠ - : ∀ {ℓ} {A : Type ℓ} → A → Term → TC ⊤ -extensionalᶠ {A = A} fun goal = ⦇ wrap (quoteTC A) (quoteTC fun) ⦈ >>= id where - work : Term → Term → TC Term - work (pi dom@(arg ai _) (abs nm cod)) tm = do - prf ← extend-context nm dom $ - work cod (raise 1 tm <#> arg ai (var 0 [])) - pure (lam (ai .ArgInfo.arg-vis) (abs nm prf)) - work _ tm = find-extensionality tm - - wrap : Term → Term → TC ⊤ - wrap t fn = do - t ← wait-for-type t - debugPrint "tactic.extensionality" 10 ("extensionalᶠ goal:\n " ∷ termErr fn ∷ "\nof type\n " ∷ termErr t ∷ []) - prf ← work t fn - unify goal prf - instance - extensional-extensionality - : ∀ {ℓ ℓs} {A : Type ℓ} {@(tactic extensional A) sa : Extensional A ℓs} - → Extensional A ℓs - extensional-extensionality {sa = sa} = sa - -{- -Canonical example of extending the Extensionality tactic: - -* The actual 'Extensional' value can have ⦃ Extensional A ℓ ⦄ in its - "instance context". These are filled in by the bridge instance above. - -* The 'Extensionality' loop-breaker only mentions the things that are - actually required to compute the "head" type. --} -Extensional-Lift - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} - → ⦃ sa : Extensional A ℓr ⦄ - → Extensional (Lift ℓ' A) ℓr -Extensional-Lift ⦃ sa ⦄ .Pathᵉ (lift x) (lift y) = sa .Pathᵉ x y -Extensional-Lift ⦃ sa ⦄ .reflᵉ (lift x) = sa .reflᵉ x -Extensional-Lift ⦃ sa ⦄ .idsᵉ .to-path p = ap lift (sa .idsᵉ .to-path p) -Extensional-Lift ⦃ sa ⦄ .idsᵉ .to-path-over p = sa .idsᵉ .to-path-over p - -instance - extensionality-lift : ∀ {ℓ ℓ'} {A : Type ℓ} → Extensionality (Lift ℓ' A) - extensionality-lift = record { lemma = quote Extensional-Lift } - -Extensional-Π - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} - → ⦃ sb : ∀ {x} → Extensional (B x) ℓr ⦄ - → Extensional ((x : A) → B x) (ℓ ⊔ ℓr) -Extensional-Π ⦃ sb ⦄ .Pathᵉ f g = ∀ x → Pathᵉ sb (f x) (g x) -Extensional-Π ⦃ sb ⦄ .reflᵉ f x = reflᵉ sb (f x) -Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path h = funext λ i → sb .idsᵉ .to-path (h i) -Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path-over h = funextP λ i → sb .idsᵉ .to-path-over (h i) - -Extensional-Π' - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} - → ⦃ sb : ∀ {x} → Extensional (B x) ℓr ⦄ - → Extensional ({x : A} → B x) (ℓ ⊔ ℓr) -Extensional-Π' ⦃ sb ⦄ .Pathᵉ f g = ∀ {x} → Pathᵉ sb (f {x}) (g {x}) -Extensional-Π' ⦃ sb ⦄ .reflᵉ f = reflᵉ sb f -Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path h i {x} = sb .idsᵉ .to-path (h {x}) i -Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path-over h i {x} = sb .idsᵉ .to-path-over (h {x}) i - -Extensional-→ - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'} - → ⦃ sb : Extensional B ℓr ⦄ - → Extensional (A → B) (ℓ ⊔ ℓr) -Extensional-→ ⦃ sb ⦄ = Extensional-Π ⦃ λ {_} → sb ⦄ - -Extensional-uncurry - : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : A → Type ℓ'} {C : Type ℓ''} - → ⦃ sb : Extensional ((x : A) → B x → C) ℓr ⦄ - → Extensional (Σ A B → C) ℓr -Extensional-uncurry ⦃ sb ⦄ .Pathᵉ f g = sb .Pathᵉ (curry f) (curry g) -Extensional-uncurry ⦃ sb ⦄ .reflᵉ f = sb .reflᵉ (curry f) -Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path h i (a , b) = sb .idsᵉ .to-path h i a b -Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path-over h = sb .idsᵉ .to-path-over h - -Extensional-× - : ∀ {ℓ ℓ' ℓr ℓs} {A : Type ℓ} {B : Type ℓ'} - → ⦃ sa : Extensional A ℓr ⦄ - → ⦃ sb : Extensional B ℓs ⦄ - → Extensional (A × B) (ℓr ⊔ ℓs) -Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .Pathᵉ (x , y) (x' , y') = Pathᵉ sa x x' × Pathᵉ sb y y' -Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .reflᵉ (x , y) = reflᵉ sa x , reflᵉ sb y -Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .idsᵉ .to-path (p , q) = ap₂ _,_ - (sa .idsᵉ .to-path p) - (sb .idsᵉ .to-path q) -Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .idsᵉ .to-path-over (p , q) = Σ-pathp - (sa .idsᵉ .to-path-over p) - (sb .idsᵉ .to-path-over q) - -Extensional-lift-map - : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : Type ℓ''} - → ⦃ sa : Extensional (A → B) ℓr ⦄ - → Extensional (Lift ℓ' A → B) ℓr -Extensional-lift-map ⦃ sa = sa ⦄ .Pathᵉ f g = sa .Pathᵉ (f ∘ lift) (g ∘ lift) -Extensional-lift-map ⦃ sa = sa ⦄ .reflᵉ x = sa .reflᵉ (x ∘ lift) -Extensional-lift-map ⦃ sa = sa ⦄ .idsᵉ .to-path h i (lift x) = sa .idsᵉ .to-path h i x -Extensional-lift-map ⦃ sa = sa ⦄ .idsᵉ .to-path-over h = sa .idsᵉ .to-path-over h - -instance - extensionality-fun - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} - → Extensionality (A → B) - extensionality-fun = record { lemma = quote Extensional-→ } - - extensionality-uncurry - : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : Type ℓ''} - → Extensionality (Σ A B → C) - extensionality-uncurry = record { lemma = quote Extensional-uncurry } - - extensionality-lift-map - : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} - → Extensionality (Lift ℓ'' A → B) - extensionality-lift-map = record { lemma = quote Extensional-lift-map } - - extensionality-Π - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} - → Extensionality ((x : A) → B x) - extensionality-Π = record { lemma = quote Extensional-Π } - - extensionality-Π' - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} - → Extensionality ({x : A} → B x) - extensionality-Π' = record { lemma = quote Extensional-Π' } - - extensionality-× - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} - → Extensionality (A × B) - extensionality-× = record { lemma = quote Extensional-× } + -- Default instance, uses regular paths for the relation. + Extensional-default : ∀ {ℓ} {A : Type ℓ} → Extensional A ℓ + Extensional-default .Pathᵉ = _≡_ + Extensional-default .reflᵉ _ = refl + Extensional-default .idsᵉ = Path-identity-system + + {-# INCOHERENT Extensional-default #-} + + Extensional-Lift + : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} + → ⦃ sa : Extensional A ℓr ⦄ + → Extensional (Lift ℓ' A) ℓr + Extensional-Lift ⦃ sa ⦄ .Pathᵉ (lift x) (lift y) = sa .Pathᵉ x y + Extensional-Lift ⦃ sa ⦄ .reflᵉ (lift x) = sa .reflᵉ x + Extensional-Lift ⦃ sa ⦄ .idsᵉ .to-path p = ap lift (sa .idsᵉ .to-path p) + Extensional-Lift ⦃ sa ⦄ .idsᵉ .to-path-over p = sa .idsᵉ .to-path-over p + + Extensional-Π + : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} + → ⦃ sb : ∀ {x} → Extensional (B x) ℓr ⦄ + → Extensional ((x : A) → B x) (ℓ ⊔ ℓr) + Extensional-Π ⦃ sb ⦄ .Pathᵉ f g = ∀ x → Pathᵉ sb (f x) (g x) + Extensional-Π ⦃ sb ⦄ .reflᵉ f x = reflᵉ sb (f x) + Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path h = funext λ i → sb .idsᵉ .to-path (h i) + Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path-over h = funextP λ i → sb .idsᵉ .to-path-over (h i) + + {-# OVERLAPPABLE Extensional-Π #-} + + Extensional-Π' + : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} + → ⦃ sb : ∀ {x} → Extensional (B x) ℓr ⦄ + → Extensional ({x : A} → B x) (ℓ ⊔ ℓr) + Extensional-Π' ⦃ sb ⦄ .Pathᵉ f g = ∀ {x} → Pathᵉ (sb {x}) f g + Extensional-Π' ⦃ sb ⦄ .reflᵉ f = reflᵉ sb f + Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path h i = sb .idsᵉ .to-path h i + Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path-over h i = sb .idsᵉ .to-path-over h i + + Extensional-uncurry + : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : A → Type ℓ'} {C : Type ℓ''} + → ⦃ sb : Extensional ((x : A) → B x → C) ℓr ⦄ + → Extensional (Σ A B → C) ℓr + Extensional-uncurry ⦃ sb ⦄ .Pathᵉ f g = sb .Pathᵉ (curry f) (curry g) + Extensional-uncurry ⦃ sb ⦄ .reflᵉ f = sb .reflᵉ (curry f) + Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path h i (a , b) = sb .idsᵉ .to-path h i a b + Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path-over h = sb .idsᵉ .to-path-over h + + Extensional-× + : ∀ {ℓ ℓ' ℓr ℓs} {A : Type ℓ} {B : Type ℓ'} + → ⦃ sa : Extensional A ℓr ⦄ + → ⦃ sb : Extensional B ℓs ⦄ + → Extensional (A × B) (ℓr ⊔ ℓs) + Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .Pathᵉ (x , y) (x' , y') = Pathᵉ sa x x' × Pathᵉ sb y y' + Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .reflᵉ (x , y) = reflᵉ sa x , reflᵉ sb y + Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .idsᵉ .to-path (p , q) = ap₂ _,_ + (sa .idsᵉ .to-path p) + (sb .idsᵉ .to-path q) + Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .idsᵉ .to-path-over (p , q) = Σ-pathp + (sa .idsᵉ .to-path-over p) + (sb .idsᵉ .to-path-over q) + + Extensional-lift-map + : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : Lift ℓ' A → Type ℓ''} + → ⦃ sa : Extensional ((x : A) → B (lift x)) ℓr ⦄ + → Extensional ((x : Lift ℓ' A) → B x) ℓr + Extensional-lift-map ⦃ sa = sa ⦄ .Pathᵉ f g = sa .Pathᵉ (f ∘ lift) (g ∘ lift) + Extensional-lift-map ⦃ sa = sa ⦄ .reflᵉ x = sa .reflᵉ (x ∘ lift) + Extensional-lift-map ⦃ sa = sa ⦄ .idsᵉ .to-path h i (lift x) = sa .idsᵉ .to-path h i x + Extensional-lift-map ⦃ sa = sa ⦄ .idsᵉ .to-path-over h = sa .idsᵉ .to-path-over h {- Actual user-facing entry point for the tactic: using the 'extensional' @@ -236,7 +103,7 @@ tactic (through the blanket instance) we can find an identity system for the type A, and turn a proof in the computed relation to an identity. -} ext - : ∀ {ℓ ℓr} {A : Type ℓ} ⦃ r : Extensional A ℓr ⦄ {x y : A} + : ∀ {ℓ ℓr} {A : Type ℓ} {x y : A} ⦃ r : Extensional A ℓr ⦄ → Pathᵉ r x y → x ≡ y ext ⦃ r ⦄ p = r .idsᵉ .to-path p @@ -270,7 +137,7 @@ private -- slightly better error message than what Agda would yell. try : TC ⊤ try = do - `r ← wait-for-type =<< quoteωTC r + `r ← wait-for-type =<< quoteTC r ty ← quoteTC (Pathᵉ r x y) `x ← quoteTC x `refl ← check-type (it reflᵉ ##ₙ `r ##ₙ `x) ty <|> error @@ -373,30 +240,52 @@ injection→extensional! {sb = b-set} = injection→extensional b-set → Extensional (Σ A B) ℓr Σ-prop-extensional bprop = embedding→extensional (fst , Subset-proj-embedding bprop) -Extensional-Σ-trunc - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} - → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → ∥ B x ∥) ℓr -Extensional-Σ-trunc ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea - -Extensional-Σ-□ - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} - → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → □ (B x)) ℓr -Extensional-Σ-□ ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea - -Extensional-equiv - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'} - → ⦃ ea : Extensional (A → B) ℓr ⦄ → Extensional (A ≃ B) ℓr -Extensional-equiv ⦃ ea ⦄ = Σ-prop-extensional (λ x → is-equiv-is-prop _) ea - instance - extensionality-Σ-trunc - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → Extensionality (Σ A λ x → ∥ B x ∥) - extensionality-Σ-trunc = record { lemma = quote Extensional-Σ-trunc } - - extensionality-Σ-□ - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → Extensionality (Σ A λ x → □ (B x)) - extensionality-Σ-□ = record { lemma = quote Extensional-Σ-□ } - - extensionality-equiv - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Extensionality (A ≃ B) - extensionality-equiv = record { lemma = quote Extensional-equiv } + Extensional-Σ-trunc + : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} + → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → ∥ B x ∥) ℓr + Extensional-Σ-trunc ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea + + Extensional-Σ-□ + : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} + → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → □ (B x)) ℓr + Extensional-Σ-□ ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea + + Extensional-equiv + : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'} + → ⦃ ea : Extensional (A → B) ℓr ⦄ → Extensional (A ≃ B) ℓr + Extensional-equiv ⦃ ea ⦄ = Σ-prop-extensional (λ x → is-equiv-is-prop _) ea + + Extensional-tr-map + : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'} + → {@(tactic hlevel-tactic-worker) bset : is-set B} + → ⦃ _ : Extensional (A → B) ℓr ⦄ + → Extensional (∥ A ∥ → B) ℓr + Extensional-tr-map {bset = bset} ⦃ ea ⦄ = + injection→extensional (Π-is-hlevel 2 λ _ → bset) {f = λ f → f ∘ inc} + (λ p → funext $ ∥-∥-elim (λ _ → bset _ _) (happly p)) ea + +private module test where + variable + ℓ ℓ' ℓ'' : Level + A B C : Type ℓ + P Q R : A → Type ℓ + + _ : {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g + _ = ext + + _ : {f g : A × B → C} → ((a : A) (b : B) → f (a , b) ≡ g (a , b)) → f ≡ g + _ = ext + + _ : {f g : Σ A P → B} → ((a : A) (b : P a) → f (a , b) ≡ g (a , b)) → f ≡ g + _ = ext + + open Lift + + _ : {f g : Σ (Lift ℓ' A) (λ x → Lift ℓ' (P (x .lower))) → Lift ℓ'' B} + → ((a : A) (b : P a) → f (lift a , lift b) .lower ≡ g (lift a , lift b) .lower) + → f ≡ g + _ = ext + + _ : {f g : A → B ≃ C} → ((a : A) (b : B) → f a .fst b ≡ g a .fst b) → f ≡ g + _ = ext diff --git a/src/Algebra/Group/Ab/Tensor.lagda.md b/src/Algebra/Group/Ab/Tensor.lagda.md index 61491c787..c6828cc26 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! {B = ⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟} + {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/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md index fbe90b768..3b61f33d3 100644 --- a/src/Algebra/Group/Subgroup.lagda.md +++ b/src/Algebra/Group/Subgroup.lagda.md @@ -310,10 +310,8 @@ rest of the construction, most of it is applying induction will compute. ```agda - coeq : is-coequaliser _ _ A→im - coeq .coequal = Forget-is-faithful (funext path) where - path : (x : ⌞ Kerf.ker ⌟) → A→im # A.unit ≡ A→im # (x .fst) - path (x* , p) = Tpath (f.pres-id ∙ sym p) + coeq : is-coequaliser (Groups.Zero.zero→ ∅ᴳ) Kerf.kernel A→im + coeq .coequal = ext λ x p → f.pres-id ∙ sym p coeq .universal {F = F} {e' = e'} p = gh where module F = Group-on (F .snd) @@ -328,17 +326,8 @@ will compute. coeq .factors = Forget-is-faithful refl - coeq .unique {F} {p = p} {colim = colim} prf = Forget-is-faithful (funext path) - where - module F = Group-on (F .snd) - path : ∀ (x : image (apply f)) → colim # x ≡ elim p (x .snd) - path (x , t) = - ∥-∥-elim - {P = λ q → colim # (x , q) ≡ elim p q} - (λ _ → F.has-is-set _ _) - (λ { (f , fp) → ap (apply colim) (Σ-prop-path! (sym fp)) - ∙ (happly (ap hom prf) f) }) - t + coeq .unique {F} {p = p} {colim = colim} prf = ext λ x y p → + ap# colim (Σ-prop-path! (sym p)) ∙ happly (ap hom prf) y ``` ## Representing kernels diff --git a/src/Algebra/Ring/Module.lagda.md b/src/Algebra/Ring/Module.lagda.md index e9cbdfc79..40b332445 100644 --- a/src/Algebra/Ring/Module.lagda.md +++ b/src/Algebra/Ring/Module.lagda.md @@ -412,6 +412,7 @@ open Mod ; Module-on→Abelian-group-on ; H-Level-is-linear-map ; H-Level-is-module + ; H-Level-Linear-map ) public @@ -428,18 +429,16 @@ module _ {ℓ} {R : Ring ℓ} where ; Module-on→Abelian-group-on ; H-Level-is-linear-map ; H-Level-is-module + ; H-Level-Linear-map ) public - Extensional-linear-map - : ∀ {ℓr} {M : Module R ℓm} {N : Module R ℓn} - → ⦃ ext : Extensional (⌞ M ⌟ → ⌞ N ⌟) ℓr ⦄ - → Extensional (Linear-map M N) ℓr - Extensional-linear-map ⦃ ext ⦄ = injection→extensional! (λ p → Linear-map-path (happly p)) ext - instance - extensionality-linear-map : {M : Module R ℓm} {N : Module R ℓn} → Extensionality (Linear-map M N) - extensionality-linear-map = record { lemma = quote Extensional-linear-map } + Extensional-linear-map + : ∀ {ℓr} {M : Module R ℓm} {N : Module R ℓn} + → ⦃ ext : Extensional (⌞ M ⌟ → ⌞ N ⌟) ℓr ⦄ + → Extensional (Linear-map M N) ℓr + Extensional-linear-map ⦃ ext ⦄ = injection→extensional! (λ p → Linear-map-path (happly p)) ext module R-Mod {ℓ ℓm} {R : Ring ℓ} = Cat.Reasoning (R-Mod R ℓm) @@ -456,5 +455,14 @@ linear-map→hom → R-Mod.Hom M N linear-map→hom h .hom = h .map linear-map→hom h .preserves = h .lin + +extensional-mod-hom + : ∀ {ℓ ℓrel} {R : Ring ℓ} {M : Module R ℓm} {N : Module R ℓm} + → ⦃ ext : Extensional (Linear-map M N) ℓrel ⦄ + → Extensional (R-Mod R _ .Precategory.Hom M N) ℓrel +extensional-mod-hom ⦃ ei ⦄ = injection→extensional! {f = hom→linear-map} (λ p → ext λ e → ap map p $ₚ e) ei + +instance Extensional-mod-hom = extensional-mod-hom +{-# OVERLAPS Extensional-mod-hom #-} ``` --> diff --git a/src/Algebra/Ring/Module/Action.lagda.md b/src/Algebra/Ring/Module/Action.lagda.md index e3501525b..9ebcf229c 100644 --- a/src/Algebra/Ring/Module/Action.lagda.md +++ b/src/Algebra/Ring/Module/Action.lagda.md @@ -101,13 +101,15 @@ 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 → Iso.injective eqv (Σ-prop-path! refl)) + where private unquoteDecl eqv = declare-record-iso eqv (quote Ring-action) ``` 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/Base.lagda.md b/src/Cat/Base.lagda.md index 6ad40d081..11de232c0 100644 --- a/src/Cat/Base.lagda.md +++ b/src/Cat/Base.lagda.md @@ -580,49 +580,19 @@ 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 + (λ _ → Equiv→is-hlevel 1 (identity-system-gives-path (sa .idsᵉ)) (D .Hom-set _ _ _ _))) + _ _ ``` --> diff --git a/src/Cat/Diagram/Monad.lagda.md b/src/Cat/Diagram/Monad.lagda.md index b73239b19..8b9552c6a 100644 --- a/src/Cat/Diagram/Monad.lagda.md +++ b/src/Cat/Diagram/Monad.lagda.md @@ -204,7 +204,7 @@ open Algebra-hom public open _=>_ using (η) -module _ {o ℓ} {C : Precategory o ℓ} {M : Monad C} where +module _ {o ℓ} {C : Precategory o ℓ} {M : Monad C} where instance private module C = Cat.Reasoning C Extensional-Algebra-Hom @@ -214,22 +214,18 @@ module _ {o ℓ} {C : Precategory o ℓ} {M : Monad C} where Extensional-Algebra-Hom ⦃ sa ⦄ = injection→extensional! (Algebra-hom-path C) sa - instance - extensionality-algebra-hom - : ∀ {a b} {A : Algebra-on C M a} {B : Algebra-on C M b} - → Extensionality (Algebra-hom C M (a , A) (b , B)) - extensionality-algebra-hom = record { lemma = quote Extensional-Algebra-Hom } + Funlike-Algebra-hom + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {X Y} + → ⦃ i : Funlike (C.Hom (X .fst) (Y .fst)) A B ⦄ + → Funlike (Algebra-hom C M X Y) A B + Funlike-Algebra-hom ⦃ i ⦄ .Funlike._#_ f x = f .morphism # x - instance - Funlike-Algebra-hom - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {X Y} - → ⦃ i : Funlike (C.Hom (X .fst) (Y .fst)) A B ⦄ - → Funlike (Algebra-hom C M X Y) A B - Funlike-Algebra-hom ⦃ i ⦄ .Funlike._#_ f x = f .morphism # x + H-Level-Algebra-hom : ∀ {A B n} → H-Level (Algebra-hom C M A B) (2 + n) + H-Level-Algebra-hom = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2) + where unquoteDecl eqv = declare-record-iso eqv (quote Algebra-hom) module _ {o ℓ} (C : Precategory o ℓ) where private module C = Cat.Reasoning C - private unquoteDecl eqv = declare-record-iso eqv (quote Algebra-hom) ``` --> @@ -281,8 +277,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/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md index fa5c6c5c8..3b8f0588f 100644 --- a/src/Cat/Displayed/Univalence/Thin.lagda.md +++ b/src/Cat/Displayed/Univalence/Thin.lagda.md @@ -128,32 +128,23 @@ module _ {ℓ o' ℓ'} {S : Type ℓ → Type o'} {spec : Thin-structure ℓ' S} module So = Precategory (Structured-objects spec) module Som = Cat.Morphism (Structured-objects spec) - Extensional-Hom - : ∀ {a b ℓr} ⦃ sa : Extensional (⌞ a ⌟ → ⌞ b ⌟) ℓr ⦄ - → Extensional (So.Hom a b) ℓr - Extensional-Hom ⦃ sa ⦄ = injection→extensional! - (Structured-hom-path spec) sa - instance - extensionality-hom : ∀ {a b} → Extensionality (So.Hom a b) - extensionality-hom = record { lemma = quote Extensional-Hom } + Extensional-Hom + : ∀ {a b ℓr} ⦃ sa : Extensional (⌞ a ⌟ → ⌞ b ⌟) ℓr ⦄ + → Extensional (So.Hom a b) ℓr + Extensional-Hom ⦃ sa ⦄ = injection→extensional! + (Structured-hom-path spec) sa Funlike-Hom : ∀ {x y} → Funlike (So.Hom x y) ⌞ x ⌟ λ _ → ⌞ y ⌟ Funlike-Hom = record { _#_ = Total-hom.hom } - Homomorphism-path - : ∀ {x y : So.Ob} {f g : So.Hom x y} - → (∀ x → f # x ≡ g # x) - → f ≡ g - Homomorphism-path h = Structured-hom-path spec (funext h) - Homomorphism-monic : ∀ {x y : So.Ob} (f : So.Hom x y) → (∀ {x y} (p : f # x ≡ f # y) → x ≡ y) → Som.is-monic f - Homomorphism-monic f wit g h p = Homomorphism-path λ x → wit (ap hom p $ₚ x) + Homomorphism-monic f wit g h p = ext λ x → wit (ap hom p $ₚ x) record is-equational {ℓ o' ℓ'} {S : Type ℓ → Type o'} (spec : Thin-structure ℓ' S) : Type (lsuc ℓ ⊔ o' ⊔ ℓ') where field diff --git a/src/Cat/Functor/Base.lagda.md b/src/Cat/Functor/Base.lagda.md index 7102f2938..9516f59ea 100644 --- a/src/Cat/Functor/Base.lagda.md +++ b/src/Cat/Functor/Base.lagda.md @@ -77,9 +77,9 @@ Cat[ C , D ] .Pc.Hom-set F G = Nat-is-set Cat[ C , D ] .Pc.id = idnt Cat[ C , D ] .Pc._∘_ = _∘nt_ -Cat[ C , D ] .Pc.idr f = ext λ x → Pc.idr D _ -Cat[ C , D ] .Pc.idl f = ext λ x → Pc.idl D _ -Cat[ C , D ] .Pc.assoc f g h = ext λ x → Pc.assoc D _ _ _ +Cat[ C , D ] .Pc.idr f = ext λ x → D .Pc.idr _ +Cat[ C , D ] .Pc.idl f = ext λ x → D .Pc.idl _ +Cat[ C , D ] .Pc.assoc f g h = ext λ x → D .Pc.assoc _ _ _ ``` We'll also need the following foundational tool, characterising paths 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/Instances/Elements.lagda.md b/src/Cat/Instances/Elements.lagda.md index edf5e4c2e..f5f96067a 100644 --- a/src/Cat/Instances/Elements.lagda.md +++ b/src/Cat/Instances/Elements.lagda.md @@ -75,24 +75,24 @@ space of `Element-hom`{.Agda}. @@ -163,7 +156,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 _ ``` diff --git a/src/Cat/Monoidal/Instances/Day.lagda.md b/src/Cat/Monoidal/Instances/Day.lagda.md index 00cab72b9..ec47750d4 100644 --- a/src/Cat/Monoidal/Instances/Day.lagda.md +++ b/src/Cat/Monoidal/Instances/Day.lagda.md @@ -304,33 +304,30 @@ $f(\day{h,x,y})$, in a way compatible with the relation above. -- computation rule for `factor W (day ...)` without exposing the -- computational behaviour of any other of the symbols here. - Extensional-day-map - : ∀ {i ℓ' ℓr} {C : Type ℓ'} {@(tactic hlevel-tactic-worker) c-set : is-set C} - → ⦃ sf : ∀ {a b} → Extensional ((h : Hom i (a ⊗ b)) (x : X ʻ a) (y : Y ʻ b) → C) ℓr ⦄ - → Extensional (⌞ Day.nadir i ⌟ → C) (ℓ ⊔ ℓr) - Extensional-day-map {i} {C = C} {c-set} ⦃ sf ⦄ = done where - instance - _ : H-Level C 2 - _ = basic-instance 2 c-set + instance + Extensional-day-map + : ∀ {i ℓ' ℓr} {C : Type ℓ'} {@(tactic hlevel-tactic-worker) c-set : is-set C} + → ⦃ sf : ∀ {a b} → Extensional ((h : Hom i (a ⊗ b)) (x : X ʻ a) (y : Y ʻ b) → C) ℓr ⦄ + → Extensional (⌞ Day.nadir i ⌟ → C) (ℓ ⊔ ℓr) + Extensional-day-map {i} {C = C} {c-set} ⦃ sf ⦄ = done where + instance + _ : H-Level C 2 + _ = basic-instance 2 c-set - T : Type _ - T = {a b : Ob} (h : Hom i (a ⊗ b)) (x : X ʻ a) (y : Y ʻ b) → C + T : Type _ + T = {a b : Ob} (h : Hom i (a ⊗ b)) (x : X ʻ a) (y : Y ʻ b) → C - unday : (⌞ Day.nadir i ⌟ → C) → T - unday f h x y = f (day h x y) + unday : (⌞ Day.nadir i ⌟ → C) → T + unday f h x y = f (day h x y) - opaque - unfolding Day-coend day + opaque + unfolding Day-coend day - to-p : ∀ {f g} → Path T (unday f) (unday g) → f ≡ g - to-p p = ext λ (a , b) h x y i → p i {a} {b} h x y + to-p : ∀ {f g} → Path T (unday f) (unday g) → f ≡ g + to-p p = ext λ (a , b) h x y i → p i {a} {b} h x y - done : Extensional (⌞ Day.nadir i ⌟ → C) _ - done = injection→extensional (hlevel 2) to-p (Extensional-Π' ⦃ Extensional-Π' ⦃ sf ⦄ ⦄) - - private instance - _ : ∀ {i ℓ'} {C : Type ℓ'} → Extensionality (⌞ Day.nadir i ⌟ → C) - _ = record { lemma = quote Extensional-day-map } + done : Extensional (⌞ Day.nadir i ⌟ → C) _ + done = injection→extensional (hlevel 2) to-p auto day-swap : ∀ {i a b a' b'} {f : Hom a' a} {g : Hom b' b} {h : Hom i (a' ⊗ b')} @@ -375,11 +372,6 @@ module _ {X Y} where renaming (factor to Day-rec) public -instance - extensionality-day-map - : ∀ {X Y i ℓ'} {C : Type ℓ'} → Extensionality (⌞ Day.nadir X Y i ⌟ → C) - extensionality-day-map = record { lemma = quote Extensional-day-map } - open Day using (_⊗ᴰ_ ; Day-diagram) ``` --> diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md index 4951e056a..b2c6e8263 100644 --- a/src/Cat/Morphism.lagda.md +++ b/src/Cat/Morphism.lagda.md @@ -1,6 +1,6 @@ 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/Prelude.agda b/src/Cat/Prelude.agda index c62a8a59e..c5681c9f9 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -25,5 +25,3 @@ open import Cat.Univalent ; Hom-transport ; Hom-pathp-refll ; Hom-pathp-reflr ; module Univalent ) public - -open import Cat.Morphism.Extensionality public diff --git a/src/Cat/Univalent/Rezk.lagda.md b/src/Cat/Univalent/Rezk.lagda.md index 00cd5ef1c..88d7b8dff 100644 --- a/src/Cat/Univalent/Rezk.lagda.md +++ b/src/Cat/Univalent/Rezk.lagda.md @@ -156,6 +156,8 @@ functor is fully faithful, that's equivalent to what we want. ```agda private module Rezk↪PSh = Ffr Rezk↪PSh id-equiv + open Cr Rezk-completion using (Extensional-≅) + abstract Rezk-completion-is-category : is-category Rezk-completion Rezk-completion-is-category = diff --git a/src/Data/Set/Coequaliser.lagda.md b/src/Data/Set/Coequaliser.lagda.md index 06c271979..46d85522a 100644 --- a/src/Data/Set/Coequaliser.lagda.md +++ b/src/Data/Set/Coequaliser.lagda.md @@ -536,21 +536,28 @@ is a set, that means it's an equivalence. diff --git a/src/Order/Base.lagda.md b/src/Order/Base.lagda.md index f7a0d362b..a6cb30f39 100644 --- a/src/Order/Base.lagda.md +++ b/src/Order/Base.lagda.md @@ -235,18 +235,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 ``` --> @@ -333,5 +328,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..5e7e1c984 100644 --- a/src/Order/DCPO.lagda.md +++ b/src/Order/DCPO.lagda.md @@ -1,6 +1,6 @@ diff --git a/src/1Lab/HIT/Truncation.lagda.md b/src/1Lab/HIT/Truncation.lagda.md index f287ecb9b..a7e74cddf 100644 --- a/src/1Lab/HIT/Truncation.lagda.md +++ b/src/1Lab/HIT/Truncation.lagda.md @@ -103,14 +103,13 @@ whenever it is a family of propositions, by providing a case for ∥-∥-rec₂ pprop = ∥-∥-elim₂ (λ _ _ → pprop) ∥-∥-rec! - : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} - → {@(tactic hlevel-tactic-worker) pprop : is-prop P} + : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} ⦃ _ : H-Level P 1 ⦄ → (A → P) → (x : ∥ A ∥) → P -∥-∥-rec! {pprop = pprop} = ∥-∥-elim (λ _ → pprop) +∥-∥-rec! = ∥-∥-elim (λ _ → hlevel 1) -∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A -∥-∥-proj! {ap = ap} = ∥-∥-proj ap +∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} ⦃ _ : H-Level A 1 ⦄ → ∥ A ∥ → A +∥-∥-proj! = ∥-∥-proj (hlevel 1) ``` --> 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..ef39e524e 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 @@ -20,85 +22,6 @@ 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. --} - --- | 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@. - -- | How to decompose an application of a record selector into something -- which might have an h-level. record hlevel-projection (proj : Name) : Type where @@ -138,668 +61,189 @@ 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 ---------------- +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 + + 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 + (tm ∷ []) → unquoteTC {A = hlevel-projection head} =<< normalise tm + [] → typeError [ "H-Level: Do not know how to invert projection\n " , termErr (def head args) ] + _ → typeError [ "H-Level: Ambiguous inversions for projection\n " , nameErr head ] + + it ← projection .get-argument args + lvl ← projection .get-level =<< infer-type it + + let + soln = def (quote is-hlevel-le) + [ argN lvl + , argN want + , argN (def (quote auto) []) + , argN (def (projection .has-level) [ argN it ]) + ] + + unify goal soln +open hlevel-projection + +instance + 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 [] -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 +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 - T = def (quote X) as + 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)) -with - get-level (get-argument T) = n - w : is-hlevel T n + 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) -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? + {-# INCOHERENT H-Level-projection #-} + {-# OVERLAPPING h-level-is-prop #-} -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 +open Data.Nat.Base using (0≤x ; s≤s' ; x≤x ; x≤sucy) public - is-hlevel-suc n w : is-hlevel T (suc n) +hlevel' : ∀ {ℓ} {T : Type ℓ} (n : Nat) → ⦃ H-Level T n ⦄ → is-hlevel T n +hlevel' n ⦃ x ⦄ = H-Level.has-hlevel x -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 +private module _ {ℓ} {A : n-Type ℓ 2} {B : ∣ A ∣ → n-Type ℓ 3} where + some-def = ∣ A ∣ + + _ : is-hlevel (∣ A ∣ → ∣ A ∣) 2 + _ = hlevel' {T = _ → _} 2 + + _ : is-hlevel (Σ some-def λ x → ∣ B x ∣) 3 + _ = hlevel 3 + + _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 5 + _ = λ a → hlevel 5 + + _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 3 + _ = λ a → hlevel 3 + + _ : is-hlevel ∣ A ∣ 2 + _ = hlevel 2 + + _ : ∀ n → is-hlevel (n-Type ℓ n) (suc n) + _ = λ n → hlevel (suc n) + + _ : ∀ n (x : n-Type ℓ n) → is-hlevel ∣ x ∣ (2 + n) + _ = λ n x → hlevel (2 + n) + + _ : ∀ k {ℓ} {A : n-Type ℓ k} → is-hlevel ∣ A ∣ (4 + k) + _ = λ k → hlevel (4 + k) + + _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x : A) → is-prop A) + _ = hlevel 1 + + _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x y : A) → is-prop A) + _ = hlevel 1 + + _ : ∀ {ℓ} {A : Type ℓ} → is-groupoid (is-hlevel A 5) + _ = hlevel 3 + +private variable + ℓ ℓ' : Level + A B C : Type ℓ -- 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 - +el! : ∀ {ℓ} (A : Type ℓ) {n} ⦃ hl : H-Level A n ⦄ → n-Type ℓ n +∣ el! A ∣ = A +el! A {n} .is-tr = hlevel n 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} + : ⦃ aprop : H-Level A 1 ⦄ ⦃ bprop : H-Level B 1 ⦄ → (f : A → B) → (B → A) → is-equiv f -biimp-is-equiv! {aprop = aprop} {bprop = bprop} = biimp-is-equiv aprop bprop +biimp-is-equiv! = biimp-is-equiv (hlevel 1) (hlevel 1) prop-ext! : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} - {@(tactic hlevel-tactic-worker) aprop : is-hlevel A 1} - {@(tactic hlevel-tactic-worker) bprop : is-hlevel B 1} + → ⦃ aprop : H-Level A 1 ⦄ ⦃ bprop : H-Level B 1 ⦄ → (A → B) → (B → A) → A ≃ B -prop-ext! {aprop = aprop} {bprop = bprop} = prop-ext aprop bprop +prop-ext! = prop-ext (hlevel 1) (hlevel 1) Σ-prop-path! : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} - → {@(tactic hlevel-tactic-worker) bxprop : ∀ x → is-hlevel (B x) 1} + → ⦃ bxprop : ∀ {x} → H-Level (B x) 1 ⦄ → {x y : Σ A B} → x .fst ≡ y .fst → x ≡ y -Σ-prop-path! {bxprop = bxprop} = Σ-prop-path bxprop +Σ-prop-path! = Σ-prop-path (λ x → hlevel 1) prop! - : ∀ {ℓ} {A : I → Type ℓ} {@(tactic hlevel-tactic-worker) aip : is-hlevel (A i0) 1} + : ∀ {ℓ} {A : I → Type ℓ} ⦃ aip : H-Level (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 +prop! {A = A} {x} {y} = + is-prop→pathp (λ i → coe0→i (λ j → is-prop (A j)) i (hlevel 1)) x y injective→is-embedding! - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} - {@(tactic hlevel-tactic-worker) bset : is-set B} + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ bset : H-Level B 2 ⦄ → ∀ {f : A → B} → injective f → is-embedding f -injective→is-embedding! {bset = bset} {f} inj = injective→is-embedding bset f inj - -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)) ∷ []) - - {- - 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: - -} - - 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 ∷ []) - - 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 ∷ []) - - -- -- Non-dependent Π and Σ for readability first: - - -- decomp-fun = decomp (quote fun-is-hlevel) (`level ∷ `search ∷ []) - - -- decomp-prod : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → hlevel-decomposition (A × B) - -- decomp-prod = decomp (quote ×-is-hlevel) (`level ∷ `search ∷ `search ∷ []) - - -- Dependent type formers: - - 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 ∷ []) - - 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 ∷ []) - - decomp-pi : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (∀ a → B a) - decomp-pi = decomp (quote Π-is-hlevel) (`level ∷ `search-under 1 ∷ []) - - decomp-impl-pi : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (∀ {a} → B a) - decomp-impl-pi = decomp (quote Π-is-hlevel') (`level ∷ `search-under 1 ∷ []) - - decomp-sigma : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (Σ A B) - decomp-sigma = decomp (quote Σ-is-hlevel) (`level ∷ `search ∷ `search-under 1 ∷ []) - - -- 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 ∷ []) - - decomp-path : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ b) - decomp-path = decomp (quote Path-is-hlevel) (`level ∷ `search ∷ []) - - decomp-id : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ᵢ b) - decomp-id = decomp (quote Id-is-hlevel) (`level ∷ `search ∷ []) - - decomp-id' : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ᵢ b) - decomp-id' = decomp (quote Id-is-hlevel') (`level ∷ `search ∷ []) - - decomp-univalence : ∀ {ℓ} {A B : Type ℓ} → hlevel-decomposition (A ≡ B) - decomp-univalence = decomp (quote ≡-is-hlevel) (`level ∷ `search ∷ `search ∷ [] ) - - -- 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 ∷ []) - - 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 [] +injective→is-embedding! {f = f} inj = injective→is-embedding (hlevel 2) f inj private - module _ {ℓ} {A : n-Type ℓ 2} {B : ∣ A ∣ → n-Type ℓ 3} where - -- some-def = ∣ A ∣ - -- _ : is-hlevel (∣ A ∣ → ∣ A ∣ → ∣ A ∣ → ∣ A ∣) 2 - -- _ = hlevel! - - -- _ : is-hlevel (Σ some-def λ x → ∣ B x ∣) 3 - -- _ = hlevel! - - _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 5 - _ = hlevel! + 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 _)) - _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 3 - _ = 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) - _ : is-hlevel ∣ A ∣ 2 - _ = hlevel! +declare-record-hlevel : (n : Nat) → Name → Name → TC ⊤ +declare-record-hlevel lvl inst rec = do + (rec-tele , _) ← pi-view <$> get-type rec - _ : ∀ n → is-hlevel (n-Type ℓ n) (suc n) - _ = hlevel! + eqv ← helper-function-name rec "isom" + declare-record-iso eqv rec - _ : ∀ n (x : n-Type ℓ n) → is-hlevel ∣ x ∣ (2 + n) - _ = hlevel! + let + args = reverse $ map-up (λ n (_ , arg i _) → arg i (var₀ n)) 2 (reverse rec-tele) - _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x : A) → is-prop A) - _ = hlevel! + head-ty = it H-Level ##ₙ def rec args ##ₙ var₀ 1 - _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x y : A) → is-prop A) - _ = hlevel! + 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 - _ : ∀ {ℓ} {A : Type ℓ} → is-groupoid (is-hlevel A 5) - _ = hlevel! + 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..b7e01644d 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,6 +138,17 @@ 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 +□-rec! + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + → ⦃ _ : H-Level B 1 ⦄ + → (A → B) → □ A → B +□-rec! = □-rec (hlevel 1) + +out! : ∀ {ℓ} {A : Type ℓ} + → ⦃ _ : H-Level A 1 ⦄ + → □ A → A +out! = □-rec! λ x → x + □-rec-set : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (f : A → B) @@ -160,7 +162,7 @@ elΩ T .is-tr = squash 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! ⦃ basic-instance 1 aprop ⦄) inc □-ap : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} @@ -190,7 +192,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 +227,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 c6828cc26..7babff2d2 100644 --- a/src/Algebra/Group/Ab/Tensor.lagda.md +++ b/src/Algebra/Group/Ab/Tensor.lagda.md @@ -317,7 +317,7 @@ 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! {B = ⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟} + injection→extensional! {B = ⌞ A ⌟ → ⌞ B ⌟ → ∣ C .fst ∣} ⦃ auto ⦄ {f = λ f x y → f .hom (x , y)} (λ {x} p → Hom≃Bilinear.injective _ _ _ (ext (subst (ef .Pathᵉ _) p (ef .reflᵉ _)))) auto 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/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 3b61f33d3..cd018fcbe 100644 --- a/src/Algebra/Group/Subgroup.lagda.md +++ b/src/Algebra/Group/Subgroup.lagda.md @@ -1,6 +1,5 @@ @@ -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,22 +527,11 @@ 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 + Nat-is-set = hlevel 2 ``` - - Another fundamental lemma is that equality of natural transformations depends only on equality of the family of morphisms, since being natural is a proposition: 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. 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..97b75bd32 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 ``` --> 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/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..c27b6681c 100644 --- a/src/Cat/Displayed/Instances/Subobjects.lagda.md +++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md @@ -1,6 +1,5 @@ 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 f5f96067a..18b7de257 100644 --- a/src/Cat/Instances/Elements.lagda.md +++ b/src/Cat/Instances/Elements.lagda.md @@ -75,6 +75,7 @@ space of `Element-hom`{.Agda}. @@ -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 1971cd957..142d448e9 100644 --- a/src/Cat/Instances/Slice.lagda.md +++ b/src/Cat/Instances/Slice.lagda.md @@ -128,17 +128,13 @@ says that the map $h$ "respects reindexing", or less obliquely → x ≡ y /-Hom-path = /-Hom-pathp refl refl - private unquoteDecl eqv = declare-record-iso eqv (quote /-Hom) - 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 - abstract - H-Level-/-Hom : ∀ {c a b n} → H-Level (/-Hom {c = c} a b) (2 + n) - H-Level-/-Hom = basic-instance 2 (Iso→is-hlevel 2 eqv (hlevel 2)) +unquoteDecl H-Level-/-Hom = declare-record-hlevel 2 H-Level-/-Hom (quote /-Hom) ``` --> @@ -515,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 @@ @@ -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) @@ -666,16 +597,6 @@ abstract (f .epic) (g .epic) i - -instance - Extensional-↪ : ∀ {a b ℓr} ⦃ _ : Extensional (Hom a b) ℓr ⦄ → Extensional (a ↪ b) ℓr - Extensional-↪ ⦃ sa ⦄ = injection→extensional! ↪-pathp sa - - Extensional-↠ : ∀ {a b ℓr} ⦃ _ : Extensional (Hom a b) ℓr ⦄ → Extensional (a ↠ b) ℓr - Extensional-↠ ⦃ sa ⦄ = injection→extensional! ↠-pathp sa - - Extensional-≅ : ∀ {a b ℓr} ⦃ _ : Extensional (Hom a b) ℓr ⦄ → Extensional (a ≅ b) ℓr - Extensional-≅ ⦃ sa ⦄ = injection→extensional! (≅-pathp refl refl) sa ``` --> 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 c5681c9f9..aa1979f86 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -25,3 +25,5 @@ open import Cat.Univalent ; Hom-transport ; Hom-pathp-refll ; Hom-pathp-reflr ; module Univalent ) 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/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 88d7b8dff..e100bd6e9 100644 --- a/src/Cat/Univalent/Rezk.lagda.md +++ b/src/Cat/Univalent/Rezk.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 46d85522a..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 @@ -539,14 +539,14 @@ is a set, that means it's an equivalence. instance Extensional-coeq-map : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {f g : A → B} - → ⦃ sf : Extensional (B → C) ℓr ⦄ {@(tactic hlevel-tactic-worker) c-set : is-set C} + → ⦃ sf : Extensional (B → C) ℓr ⦄ ⦃ _ : H-Level C 2 ⦄ → Extensional (Coeq f g → C) ℓr Extensional-coeq-map ⦃ sf ⦄ .Pathᵉ f g = sf .Pathᵉ (f ∘ inc) (g ∘ inc) Extensional-coeq-map ⦃ sf ⦄ .reflᵉ f = sf .reflᵉ (f ∘ inc) - Extensional-coeq-map ⦃ sf ⦄ {c-set} .idsᵉ .to-path h = funext $ - Coeq-elim-prop (λ x → c-set _ _) (happly (sf .idsᵉ .to-path h)) - Extensional-coeq-map ⦃ sf ⦄ {c-set} .idsᵉ .to-path-over p = - is-prop→pathp (λ i → Pathᵉ-is-hlevel 1 sf (fun-is-hlevel 2 c-set)) _ _ + Extensional-coeq-map ⦃ sf ⦄ .idsᵉ .to-path h = funext $ + Coeq-elim-prop (λ x → hlevel 1) (happly (sf .idsᵉ .to-path h)) + Extensional-coeq-map ⦃ sf ⦄ .idsᵉ .to-path-over p = + is-prop→pathp (λ i → Pathᵉ-is-hlevel 1 sf (hlevel 2)) _ _ private module test where variable C : Type ℓ diff --git a/src/Data/Set/Material.lagda.md b/src/Data/Set/Material.lagda.md index 41bf77bf8..9ca5b228f 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 } ``` --> @@ -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 @@ @@ -152,16 +153,16 @@ also at the same h-level as `A` and `B`. Thus, we have: Equiv→is-hlevel (1 + n) Code≃Path (Code-is-hlevel ahl bhl) instance - hlevel-decomp-⊎ : hlevel-decomposition (A ⊎ B) - hlevel-decomp-⊎ = decomp (quote ⊎-is-hlevel) - (`level-minus 2 ∷ `search ∷ `search ∷ []) + H-Level-⊎ : ∀ {n} ⦃ _ : 2 ≤ n ⦄ ⦃ _ : H-Level A n ⦄ ⦃ _ : H-Level B n ⦄ → H-Level (A ⊎ B) n + H-Level-⊎ {n = suc (suc n)} ⦃ s≤s (s≤s p) ⦄ = hlevel-instance $ + ⊎-is-hlevel _ (hlevel (2 + n)) (hlevel (2 + n)) ``` diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md index 7a274c47a..25cd25c2e 100644 --- a/src/HoTT.lagda.md +++ b/src/HoTT.lagda.md @@ -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..ada8c7cc2 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 = @@ -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..6c1242483 100644 --- a/src/Homotopy/Space/Suspension/Properties.lagda.md +++ b/src/Homotopy/Space/Suspension/Properties.lagda.md @@ -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/Order/Base.lagda.md b/src/Order/Base.lagda.md index a6cb30f39..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 } @@ -260,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._∘_ = _∘ₘ_ @@ -286,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 @@ -316,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 diff --git a/src/Order/DCPO.lagda.md b/src/Order/DCPO.lagda.md index 5e7e1c984..d055fb3d8 100644 --- a/src/Order/DCPO.lagda.md +++ b/src/Order/DCPO.lagda.md @@ -82,18 +82,10 @@ Since least upper bounds are unique when they exist, being a DCPO is a -```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 (λ _ → hlevel 1) λ (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,7 +248,7 @@ 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 @@ -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 From 52a970afe7d81b90412576821fff3e7b2adc7085 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 27 Mar 2024 17:06:48 -0300 Subject: [PATCH 4/7] chore: sort imports --- src/1Lab/Extensionality.agda | 4 +--- src/Algebra/Group/Ab/Tensor.lagda.md | 2 +- src/Cat/Base.lagda.md | 4 ++-- src/Data/Sum/Properties.lagda.md | 2 +- 4 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda index 3650b9547..a82b174ce 100644 --- a/src/1Lab/Extensionality.agda +++ b/src/1Lab/Extensionality.agda @@ -138,10 +138,8 @@ private try : TC ⊤ try = do `r ← wait-for-type =<< quoteTC r - ty ← quoteTC (Pathᵉ r x y) `x ← quoteTC x - `refl ← check-type (it reflᵉ ##ₙ `r ##ₙ `x) ty <|> error - unify goal `refl + unify goal (it reflᵉ ##ₙ `r ##ₙ `x) <|> error error = do `x ← quoteTC x diff --git a/src/Algebra/Group/Ab/Tensor.lagda.md b/src/Algebra/Group/Ab/Tensor.lagda.md index 7babff2d2..37efe3cf2 100644 --- a/src/Algebra/Group/Ab/Tensor.lagda.md +++ b/src/Algebra/Group/Ab/Tensor.lagda.md @@ -317,7 +317,7 @@ 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! {B = ⌞ A ⌟ → ⌞ B ⌟ → ∣ C .fst ∣} ⦃ auto ⦄ + injection→extensional! {f = λ f x y → f .hom (x , y)} (λ {x} p → Hom≃Bilinear.injective _ _ _ (ext (subst (ef .Pathᵉ _) p (ef .reflᵉ _)))) auto diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md index 37c05ec27..ba7d4fae4 100644 --- a/src/Cat/Base.lagda.md +++ b/src/Cat/Base.lagda.md @@ -1,13 +1,13 @@ From 7d63fa519b52aad163adead27b3a066d4a6ec79d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 27 Mar 2024 17:22:46 -0300 Subject: [PATCH 5/7] chore: bump cache key Absolutely should not change anything but I want to see how much the build time improved on GitHub, since the CI executors are... *slightly* underpowered, compared to my desktop. --- .github/workflows/build.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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: | From 99681522bbd0a2e0a3fd02e6679a55f056187860 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Mon, 1 Apr 2024 15:22:15 -0300 Subject: [PATCH 6/7] chore: commits for new tactic impls --- src/1Lab/Extensionality.agda | 170 ++++++++++++++---- src/1Lab/Function/Surjection.lagda.md | 2 +- src/1Lab/HIT/Truncation.lagda.md | 38 ++-- src/1Lab/Reflection/HLevel.agda | 125 +++++++++++-- src/1Lab/Resizing.lagda.md | 15 +- src/Algebra/Group/Homotopy/BAut.lagda.md | 2 +- src/Algebra/Ring/Module/Action.lagda.md | 6 +- src/Cat/Base.lagda.md | 5 +- src/Cat/Displayed/Cartesian/Street.lagda.md | 9 +- src/Cat/Displayed/Doctrine/Frame.lagda.md | 32 ++-- src/Cat/Displayed/Instances/Lifting.lagda.md | 22 +-- .../Displayed/Instances/Subobjects.lagda.md | 28 +-- .../Displayed/Instances/TotalProduct.lagda.md | 4 +- src/Cat/Displayed/Total.lagda.md | 8 +- src/Cat/Functor/Equivalence.lagda.md | 2 +- src/Cat/Functor/Equivalence/Path.lagda.md | 7 +- src/Cat/Functor/Morphism.lagda.md | 4 +- src/Cat/Instances/Localisation.lagda.md | 20 +-- src/Cat/Instances/OFE/Complete.lagda.md | 2 +- src/Cat/Restriction/Reasoning.lagda.md | 11 +- src/Cat/Univalent/Rezk/Universal.lagda.md | 38 ++-- src/Data/Fin/Finite.lagda.md | 14 +- src/Data/Fin/Finite/Listed.lagda.md | 4 +- src/Data/Set/Material.lagda.md | 6 +- src/HoTT.lagda.md | 4 +- src/Homotopy/Connectedness.lagda.md | 2 +- .../Space/Suspension/Properties.lagda.md | 2 +- .../Classical/Compactness.lagda.md | 6 +- src/Order/DCPO/Free.lagda.md | 10 +- src/Order/Diagram/Glb.lagda.md | 4 +- src/Order/Diagram/Lub.lagda.md | 4 +- 31 files changed, 377 insertions(+), 229 deletions(-) diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda index a82b174ce..8fe41b69e 100644 --- a/src/1Lab/Extensionality.agda +++ b/src/1Lab/Extensionality.agda @@ -18,7 +18,82 @@ open import Data.Nat.Base module 1Lab.Extensionality where -record Extensional {ℓ} (A : Type ℓ) (ℓ-rel : Level) : Type (ℓ ⊔ lsuc ℓ-rel) where +{- +Automation for extensionality +============================= + +The 'Extensional' typeclass equips a type with a “preferred” choice of +identity system. What “preferred” of course depends on the type under +consideration, but the vast majority of instances simply exist to note +that the projection of some record field is an embedding. + +'Extensional' is quite a well-behaved typeclass. For starters, it is a +proposition: any pair of identity systems is connected by an equivalence +which preserves refl, and being an identity system is a proposition. + +Of course, identity systems are not *definitionally* unique. However, +unlike classes which equip a type with *structure* (e.g., our very own +Meta.Append, or From-list, etc), a change in which Extensional instance +is selected can not change the *meaning* of a program: it can only +change whether or not the program actually elaborates. + +Extensionality instances +------------------------ + +Every type has a default 'Extensional' instance, with the underlying +identity system being that of paths. Using instance overlap pragmas, we +can instruct Agda to only select the default instance in case it has +nothing else to try. + +All other instances serve as "reduction rules". For example, extensional +equality for functions will, by default, be pointwise extensional +equality in the codomain; extensionality for pairs can also be +pointwise. + +However, it's important that the "reduction rules" are maximally lazy. +This is because the 'Extensional' class is not actually definitionally +confluent. For example, we might expect that, since we have + + Extensionality-Π : ⦃ Extensional B ⦄ → Extensional (A → B) + +then the instance for equivalences should be + + Extensionality-≃ : ⦃ Extensional B ⦄ → Extensional (A ≃ B) + +but this is not actually the case: for specific instantiations of A and +B, it might be the case that a rule more specific than Extensional-Π can +fire (e.g. A is a quotient). The instance should instead be + + Extensionality-≃ : ⦃ Extensional (A → B) ⦄ → Extensional (A ≃ B) + +which *only* applies the fact that is-equiv is a proposition, and does +not apply function extensionality. + +Entry points +------------ + +While it would be possible to define a global relation _∼_ which +computes to the relation underlying a type's Extensional instance, this +would be pretty useless: the extensional instance would be frozen when +*the relation itself* is used, not when its values are used (or +introduced). + +Our overarching philosophy is that Extensional computes "the domain of a +smart constructor for equality"; therefore, we only expose a few entry +points: + +- ext: turn extensional equality into equality +- unext: the opposite +- reext!: a macro which abbreviates "ext (unext p)" +- trivial!: a macro which abbreviates "ext (_ .reflᵉ _)" +-} + +private variable + ℓ ℓ' ℓ'' ℓr : Level + A B C : Type ℓ + P Q R : A → Type ℓ + +record Extensional (A : Type ℓ) ℓ-rel : Type (ℓ ⊔ lsuc ℓ-rel) where no-eta-equality field Pathᵉ : A → A → Type ℓ-rel @@ -28,51 +103,53 @@ record Extensional {ℓ} (A : Type ℓ) (ℓ-rel : Level) : Type (ℓ ⊔ lsuc open Extensional using (Pathᵉ ; reflᵉ ; idsᵉ) public instance - -- Default instance, uses regular paths for the relation. - Extensional-default : ∀ {ℓ} {A : Type ℓ} → Extensional A ℓ + Extensional-default : Extensional A (level-of A) Extensional-default .Pathᵉ = _≡_ Extensional-default .reflᵉ _ = refl Extensional-default .idsᵉ = Path-identity-system + -- We can't mark this instance as OVERLAPPABLE because it's not + -- strictly less specific than most other instances (it fixes the + -- level of the relation to be that of the type). {-# INCOHERENT Extensional-default #-} - Extensional-Lift - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} - → ⦃ sa : Extensional A ℓr ⦄ - → Extensional (Lift ℓ' A) ℓr + -- Some vanilla "reduction rules": these all simply apply a + -- pre-existing extensionality lemma. E.g., equality for values in a + -- lifted type is equality of the underlying values, or equality of + -- functions is pointwise. + + Extensional-Lift : ⦃ Extensional A ℓr ⦄ → Extensional (Lift ℓ' A) ℓr Extensional-Lift ⦃ sa ⦄ .Pathᵉ (lift x) (lift y) = sa .Pathᵉ x y Extensional-Lift ⦃ sa ⦄ .reflᵉ (lift x) = sa .reflᵉ x Extensional-Lift ⦃ sa ⦄ .idsᵉ .to-path p = ap lift (sa .idsᵉ .to-path p) Extensional-Lift ⦃ sa ⦄ .idsᵉ .to-path-over p = sa .idsᵉ .to-path-over p Extensional-Π - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} - → ⦃ sb : ∀ {x} → Extensional (B x) ℓr ⦄ - → Extensional ((x : A) → B x) (ℓ ⊔ ℓr) + : ⦃ ∀ {x} → Extensional (P x) ℓr ⦄ + → Extensional ((x : A) → P x) (level-of A ⊔ ℓr) Extensional-Π ⦃ sb ⦄ .Pathᵉ f g = ∀ x → Pathᵉ sb (f x) (g x) Extensional-Π ⦃ sb ⦄ .reflᵉ f x = reflᵉ sb (f x) Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path h = funext λ i → sb .idsᵉ .to-path (h i) Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path-over h = funextP λ i → sb .idsᵉ .to-path-over (h i) + -- This instance is *very often* specialised. {-# OVERLAPPABLE Extensional-Π #-} Extensional-Π' - : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} - → ⦃ sb : ∀ {x} → Extensional (B x) ℓr ⦄ - → Extensional ({x : A} → B x) (ℓ ⊔ ℓr) + : ⦃ ∀ {x} → Extensional (P x) ℓr ⦄ + → Extensional ({x : A} → P x) (level-of A ⊔ ℓr) Extensional-Π' ⦃ sb ⦄ .Pathᵉ f g = ∀ {x} → Pathᵉ (sb {x}) f g Extensional-Π' ⦃ sb ⦄ .reflᵉ f = reflᵉ sb f Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path h i = sb .idsᵉ .to-path h i Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path-over h i = sb .idsᵉ .to-path-over h i - Extensional-uncurry - : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : A → Type ℓ'} {C : Type ℓ''} - → ⦃ sb : Extensional ((x : A) → B x → C) ℓr ⦄ - → Extensional (Σ A B → C) ℓr - Extensional-uncurry ⦃ sb ⦄ .Pathᵉ f g = sb .Pathᵉ (curry f) (curry g) - Extensional-uncurry ⦃ sb ⦄ .reflᵉ f = sb .reflᵉ (curry f) - Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path h i (a , b) = sb .idsᵉ .to-path h i a b - Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path-over h = sb .idsᵉ .to-path-over h + Extensional-Π'' + : ⦃ ∀ ⦃ x ⦄ → Extensional (P x) ℓr ⦄ + → Extensional (⦃ x : A ⦄ → P x) (level-of A ⊔ ℓr) + Extensional-Π'' ⦃ sb ⦄ .Pathᵉ f g = ∀ ⦃ x ⦄ → Pathᵉ (sb ⦃ x ⦄) f g + Extensional-Π'' ⦃ sb ⦄ .reflᵉ f = reflᵉ sb f + Extensional-Π'' ⦃ sb ⦄ .idsᵉ .to-path h i = sb .idsᵉ .to-path h i + Extensional-Π'' ⦃ sb ⦄ .idsᵉ .to-path-over h i = sb .idsᵉ .to-path-over h i Extensional-× : ∀ {ℓ ℓ' ℓr ℓs} {A : Type ℓ} {B : Type ℓ'} @@ -88,6 +165,26 @@ instance (sa .idsᵉ .to-path-over p) (sb .idsᵉ .to-path-over q) + -- Some non-confluent "reduction rules" for extensionality are those + -- for functions from a type with a mapping-out property; here, we can + -- immediately define instances for functions from Σ-types (equality + -- is equality after currying) and for functions from lifts (equality + -- is equality after lifting). + -- + -- These overlap the Extensional-Π instance. To have them selected for + -- e.g. equivalences ((Σ A B) ≃ C), the instance for equivalences + -- *needs* to ask for Extensional (Σ A B → C) instead of Extensional + -- C. + + Extensional-uncurry + : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''} + → ⦃ sb : Extensional ((x : A) (y : B x) → C x y) ℓr ⦄ + → Extensional ((p : Σ A B) → C (p .fst) (p .snd)) ℓr + Extensional-uncurry ⦃ sb ⦄ .Pathᵉ f g = sb .Pathᵉ (curry f) (curry g) + Extensional-uncurry ⦃ sb ⦄ .reflᵉ f = sb .reflᵉ (curry f) + Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path h i (a , b) = sb .idsᵉ .to-path h i a b + Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path-over h = sb .idsᵉ .to-path-over h + Extensional-lift-map : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : Lift ℓ' A → Type ℓ''} → ⦃ sa : Extensional ((x : A) → B (lift x)) ℓr ⦄ @@ -97,11 +194,6 @@ instance Extensional-lift-map ⦃ sa = sa ⦄ .idsᵉ .to-path h i (lift x) = sa .idsᵉ .to-path h i x Extensional-lift-map ⦃ sa = sa ⦄ .idsᵉ .to-path-over h = sa .idsᵉ .to-path-over h -{- -Actual user-facing entry point for the tactic: using the 'extensional' -tactic (through the blanket instance) we can find an identity system for -the type A, and turn a proof in the computed relation to an identity. --} ext : ∀ {ℓ ℓr} {A : Type ℓ} {x y : A} ⦃ r : Extensional A ℓr ⦄ → Pathᵉ r x y → x ≡ y @@ -123,11 +215,8 @@ tactic argument to accomplish this. private trivial-worker - : ∀ {ℓ ℓr} {A : Type ℓ} - → (r : Extensional A ℓr) - → (x y : A) - → Term - → TC ⊤ + : ∀ {ℓ ℓr} {A : Type ℓ} (r : Extensional A ℓr) + → (x y : A) → Term → TC ⊤ trivial-worker r x y goal = try where error : ∀ {ℓ} {A : Type ℓ} → TC A @@ -149,7 +238,7 @@ private , termErr `x , "\nand\n " , termErr `y - , "\nare not extensionally equal by refl." + , "\nare not extensionally equal by refl.\n" ] {- @@ -194,6 +283,11 @@ Pathᵉ-is-hlevel Pathᵉ-is-hlevel n sa hl = Equiv→is-hlevel _ (identity-system-gives-path (sa .idsᵉ)) (Path-is-hlevel' _ hl _ _) +-- Constructors for Extensional instances in terms of embeddings. The +-- extra coherence is required to make sure that we still have an +-- identity system by the end. +-- If the type you're reducing to is a set, use injection→extensional! instead. + embedding→extensional : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'} → (f : A ↪ B) @@ -219,8 +313,11 @@ injection→extensional → (∀ {x y} → f x ≡ f y → x ≡ y) → Extensional B ℓr → Extensional A ℓr -injection→extensional b-set {f} inj ext = - embedding→extensional (f , injective→is-embedding b-set f inj) ext +injection→extensional b-set {f} inj ext .Pathᵉ x y = ext .Pathᵉ (f x) (f y) +injection→extensional b-set {f} inj ext .reflᵉ x = ext .reflᵉ (f x) +injection→extensional b-set {f} inj ext .idsᵉ .to-path x = inj (ext .idsᵉ .to-path x) +injection→extensional b-set {f} inj ext .idsᵉ .to-path-over p = + is-prop→pathp (λ i → Pathᵉ-is-hlevel 1 ext b-set) _ _ injection→extensional! : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'} @@ -264,11 +361,6 @@ instance (λ p → funext $ ∥-∥-elim (λ _ → hlevel 1) (happly p)) ea private module test where - variable - ℓ ℓ' ℓ'' : Level - A B C : Type ℓ - P Q R : A → Type ℓ - _ : {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g _ = ext diff --git a/src/1Lab/Function/Surjection.lagda.md b/src/1Lab/Function/Surjection.lagda.md index f46c29274..14fcac8c8 100644 --- a/src/1Lab/Function/Surjection.lagda.md +++ b/src/1Lab/Function/Surjection.lagda.md @@ -118,7 +118,7 @@ embedding-surjective→is-equiv → is-embedding f → is-surjective f → is-equiv f -embedding-surjective→is-equiv f-emb f-surj .is-eqv x = ∥-∥-proj! do +embedding-surjective→is-equiv f-emb f-surj .is-eqv x = ∥-∥-out! do pt ← f-surj x pure $ is-prop∙→is-contr (f-emb x) pt ``` diff --git a/src/1Lab/HIT/Truncation.lagda.md b/src/1Lab/HIT/Truncation.lagda.md index a7e74cddf..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,14 +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 ℓ'} ⦃ _ : H-Level P 1 ⦄ - → (A → P) - → (x : ∥ A ∥) → P + → (A → P) → (x : ∥ A ∥) → P ∥-∥-rec! = ∥-∥-elim (λ _ → hlevel 1) -∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} ⦃ _ : H-Level A 1 ⦄ → ∥ A ∥ → A -∥-∥-proj! = ∥-∥-proj (hlevel 1) +∥-∥-out! : ∀ {ℓ} {A : Type ℓ} ⦃ _ : H-Level A 1 ⦄ → ∥ A ∥ → A +∥-∥-out! = ∥-∥-out (hlevel 1) ``` --> @@ -175,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 @@ -287,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, @@ -465,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/Reflection/HLevel.agda b/src/1Lab/Reflection/HLevel.agda index ef39e524e..5b3daef2e 100644 --- a/src/1Lab/Reflection/HLevel.agda +++ b/src/1Lab/Reflection/HLevel.agda @@ -22,6 +22,58 @@ open import Prim.Data.Nat module 1Lab.Reflection.HLevel where +{- +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. + + 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. record hlevel-projection (proj : Name) : Type where @@ -35,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 ----------------- @@ -73,7 +126,7 @@ is-hlevel-le (suc (suc n)) (suc (suc k)) (s≤s le) p x y = hlevel-proj : ∀ {ℓ} → Type ℓ → Nat → Term → TC ⊤ hlevel-proj A want goal = do - want ← quoteTC want + 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 ] @@ -82,9 +135,22 @@ hlevel-proj A want goal = do 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" + ] + (tm ∷ []) → unquoteTC {A = hlevel-projection head} =<< normalise tm - [] → typeError [ "H-Level: Do not know how to invert projection\n " , termErr (def head args) ] - _ → typeError [ "H-Level: Ambiguous inversions for projection\n " , nameErr head ] + + 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 @@ -98,6 +164,7 @@ hlevel-proj A want goal = do ] unify goal soln + open hlevel-projection instance @@ -129,14 +196,11 @@ instance open Data.Nat.Base using (0≤x ; s≤s' ; x≤x ; x≤sucy) public -hlevel' : ∀ {ℓ} {T : Type ℓ} (n : Nat) → ⦃ H-Level T n ⦄ → is-hlevel T n -hlevel' n ⦃ x ⦄ = H-Level.has-hlevel x - private module _ {ℓ} {A : n-Type ℓ 2} {B : ∣ A ∣ → n-Type ℓ 3} where some-def = ∣ A ∣ _ : is-hlevel (∣ A ∣ → ∣ A ∣) 2 - _ = hlevel' {T = _ → _} 2 + _ = hlevel {T = _ → _} 2 _ : is-hlevel (Σ some-def λ x → ∣ B x ∣) 3 _ = hlevel 3 @@ -172,12 +236,14 @@ private variable ℓ ℓ' : Level A B C : Type ℓ --- 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: +{- +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. +-} + el! : ∀ {ℓ} (A : Type ℓ) {n} ⦃ hl : H-Level A n ⦄ → n-Type ℓ n -∣ el! A ∣ = A +el! A .∣_∣ = A el! A {n} .is-tr = hlevel n biimp-is-equiv! @@ -201,20 +267,44 @@ prop-ext! = prop-ext (hlevel 1) (hlevel 1) → x ≡ y Σ-prop-path! = Σ-prop-path (λ x → hlevel 1) +Σ-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) + prop! - : ∀ {ℓ} {A : I → Type ℓ} ⦃ aip : H-Level (A i0) 1 ⦄ - → {x : A i0} {y : A i1} + : ∀ {ℓ} {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 injective→is-embedding! - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ bset : H-Level B 2 ⦄ - → ∀ {f : A → B} + : ∀ {ℓ ℓ'} {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 +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) + +{- +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. +-} + private record-hlevel-instance : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n : Nat) ⦃ _ : H-Level A n ⦄ @@ -224,9 +314,6 @@ private record-hlevel-instance n im ⦃ p ⦄ = hlevel-instance $ Iso→is-hlevel _ im (is-hlevel-le _ _ p (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) - declare-record-hlevel : (n : Nat) → Name → Name → TC ⊤ declare-record-hlevel lvl inst rec = do (rec-tele , _) ← pi-view <$> get-type rec diff --git a/src/1Lab/Resizing.lagda.md b/src/1Lab/Resizing.lagda.md index b7e01644d..87e0c68f0 100644 --- a/src/1Lab/Resizing.lagda.md +++ b/src/1Lab/Resizing.lagda.md @@ -138,12 +138,21 @@ 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 @@ -151,18 +160,18 @@ 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! ⦃ basic-instance 1 aprop ⦄) inc +□-idempotent aprop = prop-ext squash aprop (□-out aprop) inc □-ap : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} 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/Ring/Module/Action.lagda.md b/src/Algebra/Ring/Module/Action.lagda.md index 9ebcf229c..952e7f871 100644 --- a/src/Algebra/Ring/Module/Action.lagda.md +++ b/src/Algebra/Ring/Module/Action.lagda.md @@ -108,8 +108,6 @@ and ring morphisms $R \to [G,G]$ into the [endomorphism ring] of $G$. 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 → Iso.injective eqv (Σ-prop-path! refl)) - where private unquoteDecl eqv = declare-record-iso eqv (quote Ring-action) + Action≃Hom G = Iso→Equiv $ Action→Hom G + , iso (Hom→Action G) (λ x → trivial!) (λ x → refl) ``` diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md index ba7d4fae4..6ab3b3d0a 100644 --- a/src/Cat/Base.lagda.md +++ b/src/Cat/Base.lagda.md @@ -591,9 +591,6 @@ instance 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 - (λ _ → Equiv→is-hlevel 1 (identity-system-gives-path (sa .idsᵉ)) (D .Hom-set _ _ _ _))) - _ _ + is-prop→pathp (λ i → Π-is-hlevel 1 λ _ → Pathᵉ-is-hlevel 1 sa (hlevel 2)) _ _ ``` --> diff --git a/src/Cat/Displayed/Cartesian/Street.lagda.md b/src/Cat/Displayed/Cartesian/Street.lagda.md index 97b75bd32..52a045c8b 100644 --- a/src/Cat/Displayed/Cartesian/Street.lagda.md +++ b/src/Cat/Displayed/Cartesian/Street.lagda.md @@ -94,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/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/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md index c27b6681c..3a8d727f0 100644 --- a/src/Cat/Displayed/Instances/Subobjects.lagda.md +++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md @@ -100,7 +100,7 @@ commutative squares can be pasted together. Subobjects : Displayed B (o ⊔ ℓ) ℓ Subobjects .Ob[_] y = Subobject y Subobjects .Hom[_] = ≤-over -Subobjects .Hom[_]-set f a b = is-prop→is-set ≤-over-is-prop +Subobjects .Hom[_]-set f a b = hlevel 2 Subobjects .id' .map = id Subobjects .id' .sq = id-comm-sym @@ -111,9 +111,9 @@ Subobjects ._∘'_ α β .sq = pullr (β .sq) ∙ extendl (α .sq) @@ -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/Functor/Equivalence.lagda.md b/src/Cat/Functor/Equivalence.lagda.md index 1f459170b..a225032f9 100644 --- a/src/Cat/Functor/Equivalence.lagda.md +++ b/src/Cat/Functor/Equivalence.lagda.md @@ -693,7 +693,7 @@ of $\cC$ that holds for all hom-sets must also hold for all hom-sets of $\cD$. → (∀ c c' → P (Lift ℓd (C.Hom c c'))) → ∀ d d' → P (Lift ℓc (D.Hom d d')) ff+eso→preserves-hom-props F ff eso P prop P-hom d d' = - ∥-∥-proj (prop (Lift ℓc (D.Hom d d'))) $ do + ∥-∥-out (prop (Lift ℓc (D.Hom d d'))) $ do (c , c' , eqv) ← ff+eso→hom-equiv F ff eso d d' pure (transport (ap P (ua (Lift-ap eqv))) (P-hom c c')) ``` diff --git a/src/Cat/Functor/Equivalence/Path.lagda.md b/src/Cat/Functor/Equivalence/Path.lagda.md index 40e26d933..a99a8f2c0 100644 --- a/src/Cat/Functor/Equivalence/Path.lagda.md +++ b/src/Cat/Functor/Equivalence/Path.lagda.md @@ -189,10 +189,9 @@ Precategory-identity-system (λ C D → Σ (Functor C D) is-precat-iso) (λ a → Id , iso id-equiv id-equiv) Precategory-identity-system .to-path (F , i) = Precategory-path F i -Precategory-identity-system .to-path-over {C} {D} (F , i) = - Σ-prop-pathp (λ _ _ → hlevel 1) $ - Functor-pathp (λ p → path→ua-pathp _ (λ j → F.₀ (p j))) - (λ {x} {y} → homs x y) +Precategory-identity-system .to-path-over {C} {D} (F , i) = Σ-prop-pathp! $ + Functor-pathp (λ p → path→ua-pathp _ (λ j → F.₀ (p j))) + (λ {x} {y} → homs x y) where module C = Cat.Reasoning C module D = Cat.Reasoning D diff --git a/src/Cat/Functor/Morphism.lagda.md b/src/Cat/Functor/Morphism.lagda.md index 98b3aae3f..e1f6d381c 100644 --- a/src/Cat/Functor/Morphism.lagda.md +++ b/src/Cat/Functor/Morphism.lagda.md @@ -101,7 +101,7 @@ $F(g') = g \circ i$. ```agda module _ (ff : is-fully-faithful F) (eso : is-eso F) where ff+eso→preserves-mono : 𝒞.is-monic a → 𝒟.is-monic (F₁ a) - ff+eso→preserves-mono {a = a} a-monic {x} f g p = ∥-∥-proj! do + ff+eso→preserves-mono {a = a} a-monic {x} f g p = ∥-∥-out! do (x* , i) ← eso x (f* , q) ← fully-faithful→full {F = F} ff (f 𝒟.∘ 𝒟.to i) (g* , r) ← fully-faithful→full {F = F} ff (g 𝒟.∘ 𝒟.to i) @@ -143,7 +143,7 @@ formally dual to the case above, we will not dwell on it. ```agda ff+eso→preserves-epi : 𝒞.is-epic a → 𝒟.is-epic (F₁ a) - ff+eso→preserves-epi {a = a} a-epic {x} f g p = ∥-∥-proj! do + ff+eso→preserves-epi {a = a} a-epic {x} f g p = ∥-∥-out! do (x* , i) ← eso x (f* , q) ← fully-faithful→full {F = F} ff (𝒟.from i 𝒟.∘ f) (g* , r) ← fully-faithful→full {F = F} ff (𝒟.from i 𝒟.∘ g) diff --git a/src/Cat/Instances/Localisation.lagda.md b/src/Cat/Instances/Localisation.lagda.md index ae069e0b3..8c0964fa2 100644 --- a/src/Cat/Instances/Localisation.lagda.md +++ b/src/Cat/Instances/Localisation.lagda.md @@ -210,19 +210,15 @@ module _ {o ℓ w} {C : Precategory o ℓ} {W : Wide-subcat C w} where abstract Zigzag-elim-prop : ∀ {ℓ'} (P : ∀ {a b} → Zigzag C W a b → Type ℓ') - → (∀ {a b} (h : Zigzag C W a b) → is-prop (P h)) + → ⦃ ∀ {a b} {h : Zigzag C W a b} → H-Level (P h) 1 ⦄ → (hnil : ∀ {a} → P {a} []) → (hzig : ∀ {a b c} (f : Hom b c) (h : Zigzag C W a b) → P h → P (zig f h)) → (hzag : ∀ {a b c} (f : Hom c b) (hf : f ∈ W) (h : Zigzag C W a b) → P h → P (zag f hf h)) → ∀ {a b} (h : Zigzag C W a b) → P h - Zigzag-elim-prop P pprop hnil hzig hzag = - Zigzag-elim P - (λ h → is-prop→is-set (pprop h)) + Zigzag-elim-prop P hnil hzig hzag = + Zigzag-elim P (λ h → is-prop→is-set (hlevel 1)) hnil hzig hzag - (λ ph → is-prop→pathp (λ i → pprop _) _ _) - (λ ph → is-prop→pathp (λ i → pprop _) _ _) - (λ ph → is-prop→pathp (λ i → pprop _) _ _) - (λ ph → is-prop→pathp (λ i → pprop _) _ _) + (λ _ → prop!) (λ _ → prop!) (λ _ → prop!) (λ _ → prop!) ``` --> @@ -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/Complete.lagda.md b/src/Cat/Instances/OFE/Complete.lagda.md index 2aefdf998..9f6a3952f 100644 --- a/src/Cat/Instances/OFE/Complete.lagda.md +++ b/src/Cat/Instances/OFE/Complete.lagda.md @@ -194,7 +194,7 @@ exactly what we want. ```agda banach : ∥ A ∥ → (f : P →ᶜᵒⁿ P) → Σ A λ x → f .map x ≡ x - banach inhab f = ∥-∥-proj fp-unique fp' where + banach inhab f = ∥-∥-out fp-unique fp' where fp-unique : is-prop (Σ A λ x → f .map x ≡ x) fp-unique (a , p) (b , q) = Σ-prop-path (λ x → from-ofe-on P .fst .is-tr _ _) 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/Rezk/Universal.lagda.md b/src/Cat/Univalent/Rezk/Universal.lagda.md index 203725c33..789084ec7 100644 --- a/src/Cat/Univalent/Rezk/Universal.lagda.md +++ b/src/Cat/Univalent/Rezk/Universal.lagda.md @@ -85,7 +85,7 @@ eso→pre-faithful → is-eso H → (γ δ : F => G) → (∀ b → γ .η (H .F₀ b) ≡ δ .η (H .F₀ b)) → γ ≡ δ eso→pre-faithful {A = A} {B = B} {C = C} H {F} {G} h-eso γ δ p = ext λ b → - ∥-∥-proj (C.Hom-set _ _ _ _) do + ∥-∥-out (C.Hom-set _ _ _ _) do (b' , m) ← h-eso b ∥_∥.inc $ γ .η b ≡⟨ C.intror (F-map-iso F m .invl) ⟩ @@ -190,7 +190,7 @@ this file in Agda and poke around the proof. ```agda lemma : (a : A.Ob) (f : H.₀ a B.≅ b) → γ.η a ≡ G.₁ (f .from) C.∘ g C.∘ F.₁ (f .to) - lemma a f = ∥-∥-proj (C.Hom-set _ _ _ _) do + lemma a f = ∥-∥-out (C.Hom-set _ _ _ _) do (k , p) ← H-full (h.from B.∘ B.to f) (k⁻¹ , q) ← H-full (B.from f B.∘ h.to) ∥_∥.inc $ @@ -213,7 +213,7 @@ over $b$ is a proposition. ```agda T-prop : ∀ b → is-prop (T b) - T-prop b (g , coh) (g' , coh') = Σ-prop-path (λ x → hlevel 1) $ ∥-∥-proj (hlevel 1) do + T-prop b (g , coh) (g' , coh') = Σ-prop-path! $ ∥-∥-out! do (a₀ , h) ← H-eso b pure $ C.iso→epic (F-map-iso F h) _ _ (C.iso→monic (F-map-iso G (h B.Iso⁻¹)) _ _ @@ -233,7 +233,7 @@ $(a,h)$ pair. ∥_∥.inc (Mk.g b a₀ h , Mk.lemma b a₀ h) mkT : ∀ b → T b - mkT b = ∥-∥-proj (T-prop b) (mkT' b (H-eso b)) + mkT b = ∥-∥-out (T-prop b) (mkT' b (H-eso b)) ``` Another calculation shows that, since $H$ is full, given any pair of @@ -257,7 +257,7 @@ the transformation we're defining, too. module h = B._≅_ h naturality : _ - naturality = ∥-∥-proj (C.Hom-set _ _ _ _) do + naturality = ∥-∥-out (C.Hom-set _ _ _ _) do (k , p) ← H-full (h'.from B.∘ f B.∘ h.to) pure $ C.pullr (C.pullr (F.weave (sym (B.pushl p ∙ ap₂ B._∘_ refl (B.cancelr h.invl))))) @@ -278,8 +278,8 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful. δ : F => G δ .η b = mkT b .fst δ .is-natural b b' f = ∥-∥-elim₂ - {P = λ α β → ∥-∥-proj (T-prop b') (mkT' b' α) .fst C.∘ F.₁ f - ≡ G.₁ f C.∘ ∥-∥-proj (T-prop b) (mkT' b β) .fst} + {P = λ α β → ∥-∥-out (T-prop b') (mkT' b' α) .fst C.∘ F.₁ f + ≡ G.₁ f C.∘ ∥-∥-out (T-prop b) (mkT' b β) .fst} (λ _ _ → C.Hom-set _ _ _ _) (λ (a' , h') (a , h) → naturality f a a' h h') (H-eso b') (H-eso b) @@ -287,7 +287,7 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful. full {x = x} {y = y} γ = pure (δ _ _ γ , ext p) where p : ∀ b → δ _ _ γ .η (H.₀ b) ≡ γ .η b p b = subst - (λ e → ∥-∥-proj (T-prop _ _ γ (H.₀ b)) (mkT' _ _ γ (H.₀ b) e) .fst + (λ e → ∥-∥-out (T-prop _ _ γ (H.₀ b)) (mkT' _ _ γ (H.₀ b) e) .fst ≡ γ .η b) (squash (inc (b , B.id-iso)) (H-eso (H.₀ b))) (C.eliml (y .F-id) ∙ C.elimr (x .F-id)) @@ -357,8 +357,7 @@ candidate over it. Obs-is-prop : ∀ {b} (f : Essential-fibre H b) (c : Obs b) → obj' f ≡ c Obs-is-prop (a₀ , h₀) (c' , k' , β) = Σ-pathp (Univalent.iso→path c-cat c≅c') $ - Σ-prop-pathp - (λ i x → Π-is-hlevel³ 1 λ _ _ _ → Π-is-hlevel 1 λ _ → C.Hom-set _ _ _ _) $ + Σ-prop-pathp! $ funextP λ a → funextP λ h → C.≅-pathp _ _ $ Univalent.Hom-pathp-reflr-iso c-cat {q = c≅c'} ( C.pullr (F.eliml (H.from-id (h₀ .invr))) @@ -374,7 +373,7 @@ candidate over it. -
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/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/Set/Material.lagda.md b/src/Data/Set/Material.lagda.md index 9ca5b228f..24b3bcce0 100644 --- a/src/Data/Set/Material.lagda.md +++ b/src/Data/Set/Material.lagda.md @@ -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}) diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md index 25cd25c2e..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 diff --git a/src/Homotopy/Connectedness.lagda.md b/src/Homotopy/Connectedness.lagda.md index ada8c7cc2..e5b5d06d8 100644 --- a/src/Homotopy/Connectedness.lagda.md +++ b/src/Homotopy/Connectedness.lagda.md @@ -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 = diff --git a/src/Homotopy/Space/Suspension/Properties.lagda.md b/src/Homotopy/Space/Suspension/Properties.lagda.md index 6c1242483..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 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/DCPO/Free.lagda.md b/src/Order/DCPO/Free.lagda.md index 6ed69f13c..55f5cc87f 100644 --- a/src/Order/DCPO/Free.lagda.md +++ b/src/Order/DCPO/Free.lagda.md @@ -156,9 +156,9 @@ long as we show that the function $s_{-}$ is _constant_. ```agda ⊑-lub {Ix = Ix} s dir .elt = - □-rec-set (λ (ix , def) → s ix .elt def) (λ p q i → + □-rec-set (hlevel 2) (λ (ix , def) → s ix .elt def) (λ p q i → is-const p q i .elt $ - is-prop→pathp (λ i → is-const p q i .def .is-tr) (p .snd) (q .snd) i) (hlevel 2) + is-prop→pathp (λ i → is-const p q i .def .is-tr) (p .snd) (q .snd) i) where abstract ``` @@ -171,7 +171,7 @@ satisfying $s_i \lsq s_k$ and $s_j \lsq s_k$. We then compute: is-const : ∀ (p q : Σ[ i ∈ Ix ] ⌞ s i ⌟) → s (p .fst) ≡ s (q .fst) - is-const (i , si) (j , sj) = ∥-∥-proj! $ do + is-const (i , si) (j , sj) = ∥-∥-out! do (k , p , q) ← dir i j pure $ part-ext (λ _ → sj) (λ _ → si) λ si sj → s i .elt _ ≡˘⟨ p .refines si ⟩ @@ -202,7 +202,7 @@ module : ∀ 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 (λ _ → hlevel 1) λ (i , si) → + ⊑-lub-least x le .refines = □-elim! λ (i , si) → le i .refines si ``` @@ -253,7 +253,7 @@ 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 diff --git a/src/Order/Diagram/Glb.lagda.md b/src/Order/Diagram/Glb.lagda.md index d7e11e846..3d1deddd5 100644 --- a/src/Order/Diagram/Glb.lagda.md +++ b/src/Order/Diagram/Glb.lagda.md @@ -126,7 +126,7 @@ module _ {o ℓ} {P : Poset o ℓ} where where cover-preserves-is-glb : ∀ {glb} → is-glb P F glb → is-glb P (F ⊙ f) glb cover-preserves-is-glb g .glb≤fam i = g .glb≤fam (f i) - cover-preserves-is-glb g .greatest lb' le = g .greatest lb' λ i → ∥-∥-proj! do + cover-preserves-is-glb g .greatest lb' le = g .greatest lb' λ i → ∥-∥-out! do (i' , p) ← surj i pure (≤-trans (le i') (≤-refl' (ap F p))) @@ -135,7 +135,7 @@ module _ {o ℓ} {P : Poset o ℓ} where cover-preserves-glb g .Glb.has-glb = cover-preserves-is-glb (g .Glb.has-glb) cover-reflects-is-glb : ∀ {glb} → is-glb P (F ⊙ f) glb → is-glb P F glb - cover-reflects-is-glb g .glb≤fam i = ∥-∥-proj! do + cover-reflects-is-glb g .glb≤fam i = ∥-∥-out! do (y , p) ← surj i pure (≤-trans (g .glb≤fam y) (≤-refl' (ap F p))) cover-reflects-is-glb g .greatest lb' le = g .greatest lb' λ i → le (f i) diff --git a/src/Order/Diagram/Lub.lagda.md b/src/Order/Diagram/Lub.lagda.md index 28eb7f1d1..3b347cfbd 100644 --- a/src/Order/Diagram/Lub.lagda.md +++ b/src/Order/Diagram/Lub.lagda.md @@ -124,7 +124,7 @@ module _ {o ℓ} {P : Poset o ℓ} where where cover-preserves-is-lub : ∀ {lub} → is-lub P F lub → is-lub P (F ⊙ f) lub cover-preserves-is-lub l .fam≤lub x = l .fam≤lub (f x) - cover-preserves-is-lub l .least ub' le = l .least ub' λ i → ∥-∥-proj! do + cover-preserves-is-lub l .least ub' le = l .least ub' λ i → ∥-∥-out! do (i' , p) ← surj i pure (≤-trans (≤-refl' (ap F (sym p))) (le i')) @@ -133,7 +133,7 @@ module _ {o ℓ} {P : Poset o ℓ} where cover-preserves-lub l .Lub.has-lub = cover-preserves-is-lub (l .Lub.has-lub) cover-reflects-is-lub : ∀ {lub} → is-lub P (F ⊙ f) lub → is-lub P F lub - cover-reflects-is-lub l .fam≤lub x = ∥-∥-proj! do + cover-reflects-is-lub l .fam≤lub x = ∥-∥-out! do (y , p) ← surj x pure (≤-trans (≤-refl' (ap F (sym p))) (l .fam≤lub y)) cover-reflects-is-lub l .least ub' le = l .least ub' λ i → le (f i) From 6e18b20c33a20486573eabd2f4599ecbc6843de5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Mon, 1 Apr 2024 16:05:37 -0300 Subject: [PATCH 7/7] fixup: ext changed --- src/Cat/Monoidal/Instances/Day.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cat/Monoidal/Instances/Day.lagda.md b/src/Cat/Monoidal/Instances/Day.lagda.md index 6556e90d9..62979682f 100644 --- a/src/Cat/Monoidal/Instances/Day.lagda.md +++ b/src/Cat/Monoidal/Instances/Day.lagda.md @@ -319,7 +319,7 @@ $f(\day{h,x,y})$, in a way compatible with the relation above. unfolding Day-coend day to-p : ∀ {f g} → Path T (unday f) (unday g) → f ≡ g - to-p p = ext λ (a , b) h x y i → p i {a} {b} h x y + to-p p = ext λ a b h x y i → p i {a} {b} h x y done : Extensional (⌞ Day.nadir i ⌟ → C) _ done = injection→extensional (hlevel 2) to-p auto