diff --git a/1lab.agda-lib b/1lab.agda-lib index 844055a81..17525e768 100644 --- a/1lab.agda-lib +++ b/1lab.agda-lib @@ -12,4 +12,5 @@ flags: --guardedness --two-level -W noUnsupportedIndexedMatch + -W noRewriteVariablesBoundInSingleton --experimental-lazy-instances diff --git a/src/Algebra/Group/Concrete.lagda.md b/src/Algebra/Group/Concrete.lagda.md index 8b0024c52..f3da49630 100644 --- a/src/Algebra/Group/Concrete.lagda.md +++ b/src/Algebra/Group/Concrete.lagda.md @@ -258,9 +258,9 @@ The following construction is adapted from [@Symmetry, §6.5]: record C (x : ⌞ G ⌟) : Type ℓ where constructor mk field - y : ⌞ H ⌟ - p : pt G ≡ x → pt H ≡ y - f-p : (ω : pt G ≡ pt G) (α : pt G ≡ x) → p (ω ∙ α) ≡ f · ω ∙ p α + y : ⌞ H ⌟ + p : pt G ≡ x → pt H ≡ y + f-p : ∀ ω α → p (ω ∙ α) ≡ f · ω ∙ p α ``` Our family sends a point $x : \B{G}$ to a point $y : \B{H}$ with a function $p$ that @@ -326,7 +326,7 @@ Since $g$ is pointed by $p(\refl)$, this lets us conclude that we have found a right inverse to $\Pi_1$: ```agda - f≡apg : (ω : pt G ≡ pt G) → Square (p refl) (f · ω) (ap (g .fst) ω) (p refl) + f≡apg : ∀ ω → Square (p refl) (f · ω) (ap (g .fst) ω) (p refl) f≡apg ω = commutes→square $ p refl ∙ ap (g .fst) ω ≡˘⟨ p-g refl ω ⟩ p (refl ∙ ω) ≡˘⟨ ap p ∙-id-comm ⟩ diff --git a/src/Algebra/Group/Free/Product.lagda.md b/src/Algebra/Group/Free/Product.lagda.md index 6768e23ef..f8eebe205 100644 --- a/src/Algebra/Group/Free/Product.lagda.md +++ b/src/Algebra/Group/Free/Product.lagda.md @@ -71,7 +71,7 @@ be [[group homomorphisms]] and to make the pushout square commute... inr : ⌞ B ⌟ → Amalgamated inr-hom : ∀ b b' → inr (b B.⋆ b') ≡ inr b ◆ inr b' - glue : (c : ⌞ C ⌟) → inl (f · c) ≡ inr (g · c) + glue : ∀ c → inl (f · c) ≡ inr (g · c) ``` ...finally, we truncate the resulting type to a set. diff --git a/src/Algebra/Group/Free/Words.lagda.md b/src/Algebra/Group/Free/Words.lagda.md index 8d6abef98..f902e56c4 100644 --- a/src/Algebra/Group/Free/Words.lagda.md +++ b/src/Algebra/Group/Free/Words.lagda.md @@ -600,7 +600,7 @@ Finally, we can put this together for an arbitrary reduced word, using the lemmas above for each case. ```agda - uniq : ∀ xs (α : Reduced xs) → g · (xs , α) ≡ go xs + uniq : ∀ xs α → g · (xs , α) ≡ go xs uniq xs nil = g.pres-id uniq xs (one a) = g · (a ∷ [] , one a) ≡⟨ g-cons _ _ (one a) ⟩ diff --git a/src/Algebra/Group/Homotopy.lagda.md b/src/Algebra/Group/Homotopy.lagda.md index 7f791efe4..d5ba0d3af 100644 --- a/src/Algebra/Group/Homotopy.lagda.md +++ b/src/Algebra/Group/Homotopy.lagda.md @@ -81,12 +81,12 @@ opaque πₙ-def A n = n-Tr-set ∙e n-Tr-Ωⁿ A 1 (suc n) .fst , n-Tr-Ωⁿ A 1 (suc n) .snd πₙ-def-inc - : ∀ {ℓ} (A : Type∙ ℓ) n → (l : ⌞ Ωⁿ (1 + n) A ⌟) + : ∀ {ℓ} (A : Type∙ ℓ) n l → πₙ-def A n · inc l ≡ Ωⁿ-map (1 + n) inc∙ · l πₙ-def-inc A n l = n-Tr-Ωⁿ-inc A 1 (suc n) ·ₚ l πₙ-def-∙ - : ∀ {ℓ} (A : Type∙ ℓ) n → (p q : ⌞ Ωⁿ (1 + n) A ⌟) + : ∀ {ℓ} (A : Type∙ ℓ) n p q → πₙ-def A n · inc (p ∙ q) ≡ πₙ-def A n · inc p ∙ πₙ-def A n · inc q πₙ-def-∙ A = n-Tr-Ωⁿ-∙ A 1 ``` diff --git a/src/Algebra/Group/Instances/Cyclic.lagda.md b/src/Algebra/Group/Instances/Cyclic.lagda.md index 116cf9583..77196b116 100644 --- a/src/Algebra/Group/Instances/Cyclic.lagda.md +++ b/src/Algebra/Group/Instances/Cyclic.lagda.md @@ -77,17 +77,16 @@ $n$ when $n \geq 1$, and is the infinite cyclic group when $n = 0$. ```agda infix 30 _·ℤ -_·ℤ : ∀ (n : Nat) → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-is-prop n i) +_·ℤ : ∀ n → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-is-prop n i) (n ·ℤ) .has-rep .has-unit = ∣ℤ-zero (n ·ℤ) .has-rep .has-⋆ = ∣ℤ-+ (n ·ℤ) .has-rep .has-inv = ∣ℤ-negℤ -(n ·ℤ) .has-conjugate {x} {y} = subst (n ∣ℤ_) x≡y+x-y - where - x≡y+x-y : x ≡ y +ℤ (x -ℤ y) - x≡y+x-y = - x ≡⟨ ℤ.insertl {y} (ℤ.inverser {x = y}) ⟩ - y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩ - y +ℤ (x -ℤ y) ∎ +(n ·ℤ) .has-conjugate {x} {y} = subst (n ∣ℤ_) x≡y+x-y where + x≡y+x-y : x ≡ y +ℤ (x -ℤ y) + x≡y+x-y = + x ≡⟨ ℤ.insertl {y} (ℤ.inverser {x = y}) ⟩ + y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩ + y +ℤ (x -ℤ y) ∎ infix 25 ℤ/_ ℤ/_ : Nat → Group lzero diff --git a/src/Algebra/Group/Instances/Integers.lagda.md b/src/Algebra/Group/Instances/Integers.lagda.md index 7ad05e0d1..10879933e 100644 --- a/src/Algebra/Group/Instances/Integers.lagda.md +++ b/src/Algebra/Group/Instances/Integers.lagda.md @@ -193,15 +193,15 @@ one generator. ```agda instance Extensional-ℤ-Hom - : ∀ {ℓ ℓr} {G : Group ℓ} ⦃ _ : Extensional ⌞ G ⌟ ℓr ⦄ + : ∀ {ℓ ℓr G} ⦃ _ : Extensional ⌞ G ⌟ ℓr ⦄ → Extensional (Groups.Hom (Lift-group ℓ ℤ) G) ℓr Extensional-ℤ-Hom ⦃ e ⦄ = injection→extensional! {f = λ h → h · 1} (pow-unique₂ _ _ _) e Extensional-Ab-ℤ-Hom - : ∀ {ℓ ℓr} {G : ⌞ Ab ℓ ⌟} ⦃ _ : Extensional ⌞ G ⌟ ℓr ⦄ + : ∀ {ℓ ℓr G} ⦃ _ : Extensional ⌞ G ⌟ ℓr ⦄ → Extensional (Ab.Hom (Lift-ab ℓ ℤ-ab) G) ℓr Extensional-Ab-ℤ-Hom {ℓ = ℓ} {G = G} ⦃ ef ⦄ = injection→extensional! {f = λ h → h · 1} inj ef where - inj : {x y : Ab.Hom (Lift-ab ℓ ℤ-ab) G} → x · 1 ≡ y · 1 → x ≡ y + inj : ∀ {x y} → x · 1 ≡ y · 1 → x ≡ y inj {x} {y} p = Structured-hom-path _ (ap fst (pow-unique₂ G' x' y' p)) where G' : Group ℓ G' .fst = G .fst diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md index f6ad0f2d6..7ed961305 100644 --- a/src/Algebra/Group/Subgroup.lagda.md +++ b/src/Algebra/Group/Subgroup.lagda.md @@ -62,7 +62,8 @@ group homomorphism. ```agda rep-subgroup→group-on - : (H : ℙ ⌞ G ⌟) → represents-subgroup G H → Group-on (Σ[ x ∈ G ] x ∈ H) + : {G : Group ℓ} (H : ℙ ⌞ G ⌟) + → represents-subgroup G H → Group-on (Σ[ x ∈ G ] x ∈ H) rep-subgroup→group-on {G = G} H sg = to-group-on sg' where open Group-on (G .snd) open represents-subgroup sg diff --git a/src/Algebra/Ring/Cat/Initial.lagda.md b/src/Algebra/Ring/Cat/Initial.lagda.md index b8f960ca2..4fda2cf47 100644 --- a/src/Algebra/Ring/Cat/Initial.lagda.md +++ b/src/Algebra/Ring/Cat/Initial.lagda.md @@ -224,7 +224,7 @@ evaluates to on $n$. So we're done! f-pos zero = sym f.pres-0 f-pos (suc x) = e-suc x ∙ sym (f.pres-+ (lift 1) (lift (pos x)) ∙ ap₂ R._+_ f.pres-id (sym (f-pos x))) - lemma : (i : Int) → z→r · lift i ≡ f · lift i + lemma : ∀ i → z→r · lift i ≡ f · lift i lemma (pos x) = f-pos x lemma (negsuc x) = sym (f.pres-neg {lift (possuc x)} ∙ ap R.-_ (sym (f-pos (suc x)))) ``` diff --git a/src/Algebra/Ring/Solver.agda b/src/Algebra/Ring/Solver.agda index 031f67c82..a29aa20ad 100644 --- a/src/Algebra/Ring/Solver.agda +++ b/src/Algebra/Ring/Solver.agda @@ -52,7 +52,10 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where embed-coe : Int → R embed-coe x = ℤ↪R-rh .fst (lift x) - embed-lemma : {h' : Int → R} → is-ring-hom (Liftℤ {ℓ} .snd) (R' .snd) (h' ⊙ lower) → ∀ x → embed-coe x ≡ h' x + embed-lemma + : {h' : Int → R} + → is-ring-hom (Liftℤ {ℓ} .snd) (R' .snd) (h' ⊙ lower) + → ∀ x → embed-coe x ≡ h' x embed-lemma p x = Int-is-initial R' .paths (∫hom _ p) ·ₚ lift x data Poly : Nat → Type ℓ diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md index a44c570e0..5af1aaf32 100644 --- a/src/Cat/Base.lagda.md +++ b/src/Cat/Base.lagda.md @@ -581,7 +581,7 @@ instance 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 ⦄ + → ⦃ sa : ∀ {x} → 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) diff --git a/src/Cat/CartesianClosed/Free.lagda.md b/src/Cat/CartesianClosed/Free.lagda.md index 30b51924d..980af7306 100644 --- a/src/Cat/CartesianClosed/Free.lagda.md +++ b/src/Cat/CartesianClosed/Free.lagda.md @@ -236,7 +236,7 @@ interpretation $f$ of the base types in $\cD$. ```agda (cco : Cartesian-closed-over D cart Free-closed) - (f : (x : Node) → D ʻ (` x)) + (f : ∀ x → D ʻ (` x)) where ``` @@ -252,7 +252,7 @@ This lets us construct a section of the objects of $\cD$, i.e. a method that turns any type $\tau$ into an object $S(\tau) \liesover \tau$. ```agda - Ty-elim : (x : Ty) → D ʻ x + Ty-elim : ∀ x → D ʻ x Ty-elim `⊤ = top' Ty-elim (` x) = f x Ty-elim (τ `× σ) = Ty-elim τ ⊗₀' Ty-elim σ @@ -268,10 +268,10 @@ basic term $e$. ```agda base-method : Type _ - base-method = ∀ {x y} (e : Edge x y) → Hom[ ` e ] (Ty-elim x) (f y) + base-method = ∀ {x y} e → Hom[ ` e ] (Ty-elim x) (f y) private module _ (h : base-method) where - go : ∀ {x y} (m : Mor x y) → Hom[ m ] (Ty-elim x) (Ty-elim y) + go : ∀ {x y} m → Hom[ m ] (Ty-elim x) (Ty-elim y) ``` By a long and uninteresting case bash, we can extend @@ -1270,8 +1270,8 @@ These are required to make the following triangles commute. ::: ```agda - com₀ : {Γ : Cx} (n : Ne Γ τ) → ⟦ reflect n ⟧ₚ ≡ ⟦ n ⟧ₛ - com₁ : {Γ : Cx} (x : P .dom ʻ Γ) → ⟦ x ⟧ₚ ≡ ⟦ reify x ⟧ₙ + com₀ : ∀ {Γ} (n : Ne Γ τ) → ⟦ reflect n ⟧ₚ ≡ ⟦ n ⟧ₛ + com₁ : ∀ {Γ} (x : P .dom ʻ Γ) → ⟦ x ⟧ₚ ≡ ⟦ reify x ⟧ₙ ``` diff --git a/src/Cat/Displayed/Diagram/Total/Terminal.lagda.md b/src/Cat/Displayed/Diagram/Total/Terminal.lagda.md index 05bdc8e80..aea6be208 100644 --- a/src/Cat/Displayed/Diagram/Total/Terminal.lagda.md +++ b/src/Cat/Displayed/Diagram/Total/Terminal.lagda.md @@ -36,8 +36,8 @@ displayed over $!$. record is-terminal-over {top} (term : is-terminal B top) (top' : E ʻ top) : Type (o ⊔ o' ⊔ ℓ') where open Terminal {C = B} record{ has⊤ = term } hiding (top) field - !' : {y : ⌞ B ⌟} {y' : E ʻ y} → E.Hom[ ! ] y' top' - !-unique' : {y : ⌞ B ⌟} {y' : E ʻ y} (h : E.Hom[ ! ] y' top') → !' ≡ h + !' : ∀ {y} {y' : E ʻ y} → E.Hom[ ! ] y' top' + !-unique' : ∀ {y} {y' : E ʻ y} (h : E.Hom[ ! ] y' top') → !' ≡ h opaque !ₚ : ∀ {y} {m : B.Hom y top} {y' : E ʻ y} → E.Hom[ m ] y' top' diff --git a/src/Cat/Displayed/Doctrine/Logic.lagda.md b/src/Cat/Displayed/Doctrine/Logic.lagda.md index b9f28743b..4238782c4 100644 --- a/src/Cat/Displayed/Doctrine/Logic.lagda.md +++ b/src/Cat/Displayed/Doctrine/Logic.lagda.md @@ -413,7 +413,7 @@ private variable Φ Ψ φ ψ θ φ' ψ' : Formula Γ t t₁ s s₁ : Tm Γ τ -wk : ∀ {Γ} (φ : Formula Γ) {τ : Ty} → Formula (Γ ʻ τ) +wk : ∀ {Γ} (φ : Formula Γ) {τ} → Formula (Γ ʻ τ) wk φ = sub-prop (drop stop) φ ``` --> diff --git a/src/Cat/Displayed/Instances/Scone.lagda.md b/src/Cat/Displayed/Instances/Scone.lagda.md index a0a51180c..411cbce9e 100644 --- a/src/Cat/Displayed/Instances/Scone.lagda.md +++ b/src/Cat/Displayed/Instances/Scone.lagda.md @@ -100,11 +100,11 @@ private module Scones = Displayed Scones --> ```agda -scone : ∀ {X} → (U : Set ℓ) → (∣ U ∣ → Hom top X) → Scones ʻ X +scone : ∀ {X} U → (∣ U ∣ → Hom top X) → Scones ʻ X scone U s = cut {dom = U} s scone-hom - : ∀ {X Y} {f : Hom X Y} {U V : Set ℓ} + : ∀ {X Y} {f : Hom X Y} {U V} → {su : ∣ U ∣ → Hom top X} {sv : ∣ V ∣ → Hom top Y} → (uv : ∣ U ∣ → ∣ V ∣) → (∀ u → sv (uv u) ≡ f ∘ (su u)) diff --git a/src/Cat/Displayed/Section.lagda.md b/src/Cat/Displayed/Section.lagda.md index ed27204ba..8d3cb18ed 100644 --- a/src/Cat/Displayed/Section.lagda.md +++ b/src/Cat/Displayed/Section.lagda.md @@ -39,11 +39,13 @@ arguments. ```agda record Section : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where field - S₀ : (x : ⌞ B ⌟) → E ʻ x - S₁ : {x y : ⌞ B ⌟} (f : B.Hom x y) → E.Hom[ f ] (S₀ x) (S₀ y) + S₀ : ∀ x → E ʻ x + S₁ : ∀ {x y} (f : B.Hom x y) → E.Hom[ f ] (S₀ x) (S₀ y) - S-id : {x : ⌞ B ⌟} → S₁ {x} {x} B.id ≡ E.id' - S-∘ : {x y z : ⌞ B ⌟} (f : B.Hom y z) (g : B.Hom x y) → S₁ (f B.∘ g) ≡ S₁ f E.∘' S₁ g + S-id : ∀ {x} → S₁ {x} {x} B.id ≡ E.id' + S-∘ + : ∀ {x y z} (f : B.Hom y z) (g : B.Hom x y) + → S₁ (f B.∘ g) ≡ S₁ f E.∘' S₁ g ```
@@ -100,8 +102,8 @@ to work with sections instead. module Q = Section Q field - map : (x : ⌞ B ⌟) → E.Hom[ B.id ] (P · x) (Q · x) - com : (x y : ⌞ B ⌟) (f : B.Hom x y) + map : ∀ x → E.Hom[ B.id ] (P · x) (Q · x) + com : ∀ x y (f : B.Hom x y) → map y E.∘' P.S₁ f E.≡[ B.id-comm-sym ] Q.S₁ f E.∘' map x ``` @@ -116,7 +118,7 @@ to work with sections instead. H-Level-Natₛ = basic-instance 2 (Iso→is-hlevel 2 eqv (hlevel 2)) Extensional-Natₛ - : ∀ {P Q ℓr} ⦃ _ : Extensional ((x : ⌞ B ⌟) → E.Hom[ B.id ] (P · x) (Q · x)) ℓr ⦄ + : ∀ {P Q ℓr} ⦃ _ : Extensional (∀ x → E.Hom[ B.id ] (P · x) (Q · x)) ℓr ⦄ → Extensional (P =>s Q) ℓr Extensional-Natₛ = injection→extensional! (λ p → Iso.injective eqv (p ,ₚ prop!)) auto diff --git a/src/Cat/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md index 7cd265847..dc0c67976 100644 --- a/src/Cat/Displayed/Univalence/Thin.lagda.md +++ b/src/Cat/Displayed/Univalence/Thin.lagda.md @@ -133,7 +133,7 @@ module _ {ℓ o' ℓ'} {S : Type ℓ → Type o'} {spec : Thin-structure ℓ' S} (Structured-hom-path spec) sa Homomorphism-monic - : ∀ {x y : So.Ob} (f : So.Hom x y) + : ∀ {x y} (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 = ext λ x → wit (ap fst p $ₚ x) diff --git a/src/Cat/Functor/Base.lagda.md b/src/Cat/Functor/Base.lagda.md index 7e397ed50..46aee45c8 100644 --- a/src/Cat/Functor/Base.lagda.md +++ b/src/Cat/Functor/Base.lagda.md @@ -221,13 +221,12 @@ already coherent enough to ensure that these actions agree: ```agda F-map-path - : (ccat : is-category C) (dcat : is-category D) - → ∀ {x y} (i : x C.≅ y) + : ∀ (ccat : is-category C) (dcat : is-category D) {x y} (i : x C.≅ y) → ap· F (Univalent.iso→path ccat i) ≡ Univalent.iso→path dcat (F-map-iso i) F-map-path ccat dcat {x} = Univalent.J-iso ccat P pr where P : (b : C.Ob) → C.Isomorphism x b → Type _ - P b im = ap· F (Univalent.iso→path ccat im) - ≡ Univalent.iso→path dcat (F-map-iso im) + P b im = + ap· F (Univalent.iso→path ccat im) ≡ Univalent.iso→path dcat (F-map-iso im) pr : P x C.id-iso pr = diff --git a/src/Cat/Functor/Hom/Yoneda.lagda.md b/src/Cat/Functor/Hom/Yoneda.lagda.md index 8555a0d65..9ecc425f3 100644 --- a/src/Cat/Functor/Hom/Yoneda.lagda.md +++ b/src/Cat/Functor/Hom/Yoneda.lagda.md @@ -99,15 +99,10 @@ $$ $$. ```agda - yo-natr - : ∀ {U V} {x : A ʻ U} {h : Hom V U} {y} - → A ⟪ h ⟫ x ≡ y - → yo A x ∘nt よ₁ C h ≡ yo A y + yo-natr : ∀ {U V x y} {h : Hom V U} → A ⟪ h ⟫ x ≡ y → yo A x ∘nt よ₁ C h ≡ yo A y yo-natr p = ext λ i f → A.expand refl ∙ A.ap p - yo-naturalr - : ∀ {U V} {x : A ʻ U} {h : Hom V U} - → yo A x ∘nt よ₁ C h ≡ yo A (A ⟪ h ⟫ x) + yo-naturalr : ∀ {U V x} {h : Hom V U} → yo A x ∘nt よ₁ C h ≡ yo A (A ⟪ h ⟫ x) yo-naturalr = yo-natr refl ``` @@ -119,20 +114,16 @@ $$, as natural transformations $\cC(-,U) \To B$, for any $x : A(U)$. ```agda - yo-natl - : ∀ {B : Functor (C ^op) (Sets ℓ)} {U} {x : A ʻ U} {y : B ʻ U} {h : A => B} - → h .η U x ≡ y → h ∘nt yo A x ≡ yo B y + yo-natl : ∀ {B U x y h} → h .η U x ≡ y → h ∘nt yo A x ≡ yo B y yo-natl {B = B} {h = h} p = ext λ i f → h .is-natural _ _ _ · _ ∙ PSh.ap B p - yo-naturall - : ∀ {B : Functor (C ^op) (Sets ℓ)} {U} {x : A ʻ U} {h : A => B} - → h ∘nt yo A x ≡ yo B (h .η U x) + yo-naturall : ∀ {B U x h} → h ∘nt yo A x ≡ yo B (h .η U x) yo-naturall = yo-natl refl ``` ```agda - record Section {U} {T : Sieve C U} (p : Patch T) : Type (o ⊔ ℓ ⊔ ℓs) where + record Section {U T} (p : Patch T) : Type (o ⊔ ℓ ⊔ ℓs) where no-eta-equality field {whole} : A ʻ U @@ -253,7 +253,7 @@ module _ {o ℓ ℓs} {C : Precategory o ℓ} {A : Functor (C ^op) (Sets ℓs)} Extensional-Patch ⦃ e ⦄ .idsᵉ .to-path-over p = is-prop→pathp (λ i → Pathᵉ-is-hlevel 1 e (hlevel 2)) _ _ Extensional-Section - : ∀ {U ℓr} {S : Sieve C U} {p : Patch A S} ⦃ _ : Extensional (A ʻ U) ℓr ⦄ + : ∀ {U ℓr S} {p : Patch A S} ⦃ _ : Extensional (A ʻ U) ℓr ⦄ → Extensional (Section A p) ℓr Extensional-Section ⦃ e ⦄ .Pathᵉ x y = e .Pathᵉ (x .whole) (y .whole) Extensional-Section ⦃ e ⦄ .reflᵉ x = e .reflᵉ (x .whole) @@ -299,12 +299,12 @@ A(U)$ can be made into a bunch of *local* pieces by restricting functorially. ```agda - section→patch : ∀ {U} {T : Sieve C U} → A ʻ U → Patch A T + section→patch : ∀ {U T} → A ʻ U → Patch A T section→patch x .part f _ = A ⟪ f ⟫ x section→patch x .patch f hf g hgf = A.collapse refl section→section - : ∀ {U} {T : Sieve C U} (u : A ʻ U) + : ∀ {U T} (u : A ʻ U) → Section A {T = T} (section→patch u) section→section u .whole = u section→section u .glues f hf = refl diff --git a/src/Cat/Site/Closure.lagda.md b/src/Cat/Site/Closure.lagda.md index 64eb4d43d..cc90526d4 100644 --- a/src/Cat/Site/Closure.lagda.md +++ b/src/Cat/Site/Closure.lagda.md @@ -361,7 +361,7 @@ Showing that a $\widehat{J}$-sheaf is also a $J$-sheaf is immediate. module sat {o ℓ ℓs ℓc} {C : Precategory o ℓ} {J : Coverage C ℓc} {A : Functor (C ^op) (Sets ℓs)} (shf : is-sheaf J A) where private module shf = is-sheaf (is-sheaf-saturation.to shf) - whole : ∀ {U} {S : Sieve C U} (w : J ∋ S) (p : Patch A S) → A ʻ U + whole : ∀ {U S} (w : J ∋ S) (p : Patch A S) → A ʻ U whole w = shf.whole (_ , w) abstract diff --git a/src/Cat/Site/Instances/Atomic.lagda.md b/src/Cat/Site/Instances/Atomic.lagda.md index 22c9eb3f7..a721ffbd5 100644 --- a/src/Cat/Site/Instances/Atomic.lagda.md +++ b/src/Cat/Site/Instances/Atomic.lagda.md @@ -168,7 +168,7 @@ the atomic topology: $A$ is a sheaf if every $y : A(V)$ supported by $f ```agda is-atomic-sheaf : ∀ {ℓ'} (A : Functor (C ^op) (Sets ℓ')) → Type _ is-atomic-sheaf A = - ∀ {U V : ⌞ C ⌟} (y : A ʻ V) (f : Hom V U) + ∀ {U V} (y : A ʻ V) (f : Hom V U) → is-support A f y → is-contr (Σ[ x ∈ A ʻ U ] (y ≡ A ⟪ f ⟫ x)) ``` diff --git a/src/Cat/Site/Sheafification.lagda.md b/src/Cat/Site/Sheafification.lagda.md index e2bcd5eac..15e4e63e4 100644 --- a/src/Cat/Site/Sheafification.lagda.md +++ b/src/Cat/Site/Sheafification.lagda.md @@ -101,7 +101,7 @@ functorial, and that `inc`{.Agda} is a natural transformation: map-id : ∀ x → map {U = U} id x ≡ x map-∘ : ∀ x → map (g ∘ f) x ≡ map f (map g x) - inc-natural : (x : A ʻ U) → inc (A ⟪ f ⟫ x) ≡ map f (inc x) + inc-natural : ∀ x → inc (A ⟪ f ⟫ x) ≡ map f (inc x) ``` To ensure that $A^+$ is a sheaf, we have two constructors: one states @@ -111,7 +111,7 @@ a section of the given patch. ```agda sep - : ∀ {x y : Sheafify₀ U} (c : J ʻ U) + : ∀ {x y} (c : J ʻ U) → (l : ∀ {V} (f : Hom V U) (hf : f ∈ c) → map f x ≡ map f y) → x ≡ y @@ -176,7 +176,7 @@ have a family of [[propositions]] $P$, with sections over `inc`{.Agda}: Sheafify-elim-prop : ∀ {ℓp} (P : ∀ {U} → Sheafify₀ U → Type ℓp) → (pprop : ∀ {U} (x : Sheafify₀ U) → is-prop (P x)) - → (pinc : ∀ {U : ⌞ C ⌟} (x : A ʻ U) → P (inc x)) + → (pinc : ∀ {U} (x : A ʻ U) → P (inc x)) ``` Instead of asking for $P$ over `glue`{.Agda}, we will ask instead that @@ -187,7 +187,7 @@ restriction $A^+(f)(x)$, as long as $f \in s$. ```agda → (plocal - : ∀ {U : ⌞ C ⌟} (c : J ʻ U) (x : Sheafify₀ U) + : ∀ {U} (c : J ʻ U) (x : Sheafify₀ U) → (∀ {V} (f : Hom V U) (hf : f ∈ c) → P (map f x)) → P x) → ∀ {U} (x : Sheafify₀ U) → P x ``` @@ -219,7 +219,7 @@ Taking $h = fg$ gives $P(A^+(fg)(x))$, which is equal to our goal by functoriality. ```agda - p'map : ∀ {U V : ⌞ C ⌟} (f : Hom U V) (x : Sheafify₀ V) → P' x → P' (map f x) + p'map : ∀ {U V} (f : Hom U V) (x : Sheafify₀ V) → P' x → P' (map f x) p'map f x p g = subst P (map-∘ _) (p (f ∘ g)) ``` @@ -227,7 +227,7 @@ Similarly, we can show $P'(x)$ for the inclusion of an $x : A(U)$ at every restriction, by naturality of `inc`{.Agda}. ```agda - p'inc : ∀ {U : ⌞ C ⌟} (x : A ʻ U) → P' (inc x) + p'inc : ∀ {U} (x : A ʻ U) → P' (inc x) p'inc x {V} f = subst P (inc-natural x) (pinc (A ⟪ f ⟫ x)) ``` @@ -238,7 +238,7 @@ $P'(p(f))$ for any $f \in s$. We want to show $P(A^+(f)(\operatorname{glue} p))$ ```agda p'glue - : ∀ {U : ⌞ C ⌟} (c : J ʻ U) (p : pre.Parts C map (J .cover c)) + : ∀ {U} (c : J ʻ U) (p : pre.Parts C map (J .cover c)) → (g : pre.is-patch C map (J .cover c) p) → (∀ {V} (f : Hom V U) (hf : f ∈ c) → P' (p f hf)) → P' (glue c p g) @@ -381,7 +381,7 @@ in $B(U)$ is $J$-local. ```agda unique : (G : Functor (C ^op) (Sets ℓ)) (shf : is-sheaf J G) (eta : A => G) (eps : Sheafify A => G) - → (∀ U (x : A ʻ U) → eps .η U (inc x) ≡ eta .η U x) + → (∀ U x → eps .η U (inc x) ≡ eta .η U x) → univ G shf eta ≡ eps unique {A = A} G shf eta eps comm = ext λ i → Sheafify-elim-prop A (λ {v} x → univ G shf eta .η v x ≡ eps .η v x) diff --git a/src/Data/Id/Base.lagda.md b/src/Data/Id/Base.lagda.md index 9aba35d78..9414100a7 100644 --- a/src/Data/Id/Base.lagda.md +++ b/src/Data/Id/Base.lagda.md @@ -134,37 +134,38 @@ is-set→is-setᵢ A-set x y p q = Id≃path.injective (A-set _ _ _ _) diff --git a/src/Data/Nat/Prime.lagda.md b/src/Data/Nat/Prime.lagda.md index 965f394e1..338824ed0 100644 --- a/src/Data/Nat/Prime.lagda.md +++ b/src/Data/Nat/Prime.lagda.md @@ -110,6 +110,8 @@ abstract instance H-Level-is-composite : ∀ {n k} → H-Level (is-composite n) (suc k) H-Level-is-composite = prop-instance λ a@record{p = p ; q = q} b@record{p = p' ; q = q'} → let + record{ } = a .p-prime + open is-composite using (factors) ap=bp : p ≡ p' @@ -217,7 +219,7 @@ record Factorisation (n : Nat) : Type where where work : ∀ x xs → is-prime x → (∀ x → x ∈ₗ xs → is-prime x) → x ∣ product xs → x ∈ₗ xs work x [] xp ps xd = absurd (prime≠1 xp (∣-1 xd)) - work x (y ∷ xs) xp ps xd with x ≡ᵢ? y + work x (y ∷ xs) xp@record{} ps xd with x ≡ᵢ? y ... | yes x=y = here x=y ... | no ¬p = there $ work x xs xp (λ x w → ps x (there w)) (|-*-coprime-cancel x y (product xs) diff --git a/src/Data/Partial/Properties.lagda.md b/src/Data/Partial/Properties.lagda.md index 55ecc0018..8a53550ef 100644 --- a/src/Data/Partial/Properties.lagda.md +++ b/src/Data/Partial/Properties.lagda.md @@ -118,8 +118,6 @@ desc↯ X .def = elΩ (is-contr X) desc↯ X .elt □contr = □-out! □contr .centre ``` - - ## Partial elements are injective types {defines=partial-elements-are-injective} The type of partial elements $\zap X$ is an [[injective object]] for @@ -133,9 +131,8 @@ is inhabited by some $x$ such that $f(x)$ is itself defined. ```agda extend↯ : (X → ↯ A) → (X ↪ Y) → Y → ↯ A extend↯ f e y .def = elΩ (Σ[ y* ∈ fibre (e .fst) y ] ⌞ f (y* .fst) ⌟) -extend↯ f e y .elt = - □-out-rec (Σ-is-hlevel 1 (e .snd y) (λ _ → hlevel 1)) - (λ ((x , _) , fx↓) → f x .elt fx↓) +extend↯ f e y .elt = □-out-rec (Σ-is-hlevel 1 (e .snd y) (λ _ → hlevel 1)) + (λ ((x , _) , fx↓) → f x .elt fx↓) ``` Proving that the extension of $f$ along $e$ with $f$ is a bit of a chore @@ -145,9 +142,8 @@ agree when both are defined essentially by definition. ```agda extends↯ - : ⦃ _ : H-Level A 2 ⦄ - → (f : X → ↯ A) (e : X ↪ Y) - → ∀ (x : X) → extend↯ f e (e · x) ≡ f x + : ⦃ _ : H-Level A 2 ⦄ (f : X → ↯ A) (e : X ↪ Y) + → ∀ x → extend↯ f e (e · x) ≡ f x ```
@@ -159,22 +155,19 @@ ugly. ```agda -extends↯ f e x = - part-ext to from agree - where - to : ⌞ extend↯ f e (e · x) ⌟ → ⌞ f x ⌟ - to = rec! λ x' p fx'↓ → - subst (λ x → ∣ f x .def ∣) - (has-prop-fibres→injective (e .fst) (e .snd) p) - fx'↓ - - from : ⌞ f x ⌟ → ⌞ extend↯ f e (e · x) ⌟ - from fx↓ = pure ((x , refl) , fx↓) - - agree : (fex↓ : ⌞ extend↯ f e (e · x) ⌟) (fx↓ : ⌞ f x ⌟) → extend↯ f e (e · x) .elt fex↓ ≡ f x .elt fx↓ - agree = - □-out-elim (Σ-is-hlevel 1 (e .snd (e · x)) (λ _ → hlevel 1)) λ where - ((x' , ex'=ex) , fx'↓) fx↓ → - ap₂ (λ x fx↓ → f x .elt fx↓) (has-prop-fibres→injective (e .fst) (e .snd) ex'=ex) prop! +extends↯ f e x = part-ext to from agree where + to : ⌞ extend↯ f e (e · x) ⌟ → ⌞ f x ⌟ + to = rec! λ x' p fx'↓ → subst (λ x → ∣ f x .def ∣) + (has-prop-fibres→injective (e .fst) (e .snd) p) + fx'↓ + + from : ⌞ f x ⌟ → ⌞ extend↯ f e (e · x) ⌟ + from fx↓ = pure ((x , refl) , fx↓) + + agree : ∀ fex↓ fx↓ → extend↯ f e (e · x) .elt fex↓ ≡ f x .elt fx↓ + agree = □-out-elim (Σ-is-hlevel 1 (e .snd (e · x)) (λ _ → hlevel 1)) λ where + ((x' , ex'=ex) , fx'↓) fx↓ → ap₂ (λ x fx↓ → f x .elt fx↓) + (has-prop-fibres→injective (e .fst) (e .snd) ex'=ex) + prop! ```
diff --git a/src/Homotopy/Truncation.lagda.md b/src/Homotopy/Truncation.lagda.md index 16544e051..c48559d4a 100644 --- a/src/Homotopy/Truncation.lagda.md +++ b/src/Homotopy/Truncation.lagda.md @@ -467,12 +467,12 @@ opaque n-Tr-Ω¹-inc A n = homogeneous-funext∙ (λ _ → sym (conj-refl _)) n-Tr-Ω¹-inv-inc - : ∀ {ℓ} (A : Type∙ ℓ) n (l : ⌞ Ω¹ A ⌟) + : ∀ {ℓ} (A : Type∙ ℓ) n l → Equiv.from (n-Tr-Ω¹ A n .fst) (Ω¹-map inc∙ .fst l) ≡ inc l n-Tr-Ω¹-inv-inc A n l = sym (Equiv.adjunctl (n-Tr-Ω¹ A n .fst) (n-Tr-Ω¹-inc A n ·ₚ l)) n-Tr-Ω¹-∙ - : ∀ {ℓ} (A : Type∙ ℓ) n (p q : ⌞ Ω¹ A ⌟) + : ∀ {ℓ} (A : Type∙ ℓ) n p q → n-Tr-Ω¹ A n · inc (p ∙ q) ≡ (n-Tr-Ω¹ A n · inc p) ∙ (n-Tr-Ω¹ A n · inc q) n-Tr-Ω¹-∙ A n p q = ap-∙ inc p q ``` @@ -515,25 +515,23 @@ opaque -- n-Tr-Ωⁿ respects path composition. n-Tr-Ωⁿ-∙ - : ∀ {ℓ} (A : Type∙ ℓ) n k - → (p q : ⌞ Ωⁿ (suc k) A ⌟) + : ∀ {ℓ} (A : Type∙ ℓ) n k p q → n-Tr-Ωⁿ A n (suc k) · inc (p ∙ q) ≡ n-Tr-Ωⁿ A n (suc k) · inc p ∙ n-Tr-Ωⁿ A n (suc k) · inc q - n-Tr-Ωⁿ-∙ A n k p q = trace .snd - where - trace - : (n-Tr∙ (Ωⁿ (suc k) A) (1 + n) .fst , inc (p ∙ q)) - ≃∙ (Ωⁿ (suc k) (n-Tr∙ A (suc k + suc n)) .fst - , n-Tr-Ωⁿ A n (suc k) · inc p ∙ n-Tr-Ωⁿ A n (suc k) · inc q) - trace = - ⌞ n-Tr∙ (Ω¹ (Ωⁿ k A)) (suc n) ⌟ , inc (p ∙ q) - ≃∙⟨ n-Tr-Ω¹ _ n .fst , n-Tr-Ω¹-∙ _ _ p q ⟩ - ⌞ Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) ⌟ , _ - ≃∙⟨ Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) .fst , Ω¹-map-∙ (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) _ _ ⟩ - ⌞ Ωⁿ (1 + k) (n-Tr∙ A (k + (2 + n))) ⌟ , _ - ≃∙⟨ Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ _) .fst , Ωⁿ-map-∙ k _ _ _ ⟩ - ⌞ Ωⁿ (1 + k) (n-Tr∙ A (suc k + suc n)) ⌟ , _ - ≃∙∎ + n-Tr-Ωⁿ-∙ A n k p q = trace .snd where + trace + : (n-Tr∙ (Ωⁿ (suc k) A) (1 + n) .fst , inc (p ∙ q)) + ≃∙ ( Ωⁿ (suc k) (n-Tr∙ A (suc k + suc n)) .fst + , n-Tr-Ωⁿ A n (suc k) · inc p ∙ n-Tr-Ωⁿ A n (suc k) · inc q) + trace = + ⌞ n-Tr∙ (Ω¹ (Ωⁿ k A)) (suc n) ⌟ , inc (p ∙ q) + ≃∙⟨ n-Tr-Ω¹ _ n .fst , n-Tr-Ω¹-∙ _ _ p q ⟩ + ⌞ Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) ⌟ , _ + ≃∙⟨ Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) .fst , Ω¹-map-∙ (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) _ _ ⟩ + ⌞ Ωⁿ (1 + k) (n-Tr∙ A (k + (2 + n))) ⌟ , _ + ≃∙⟨ Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ _) .fst , Ωⁿ-map-∙ k _ _ _ ⟩ + ⌞ Ωⁿ (1 + k) (n-Tr∙ A (suc k + suc n)) ⌟ , _ + ≃∙∎ -- n-Tr-Ωⁿ commutes with the obvious inclusions. @@ -541,35 +539,34 @@ opaque : ∀ {ℓ} (A : Type∙ ℓ) n k → Equiv∙.to∙ (n-Tr-Ωⁿ A n k) ∘∙ inc∙ ≡ Ωⁿ-map k inc∙ n-Tr-Ωⁿ-inc A n zero = ∘∙-idl inc∙ - n-Tr-Ωⁿ-inc A n (suc k) = homogeneous-funext∙ λ l → trace l .snd - where - trace - : (l : ⌞ Ωⁿ (suc k) A ⌟) - → (n-Tr∙ (Ωⁿ (suc k) A) (1 + n) .fst , inc l) - ≃∙ (Ωⁿ (suc k) (n-Tr∙ A (suc k + suc n)) .fst , Ωⁿ-map (suc k) inc∙ .fst l) - trace l = - ⌞ n-Tr∙ (Ω¹ (Ωⁿ k A)) (suc n) ⌟ , inc l ≃∙⟨ n-Tr-Ω¹ _ n .fst , n-Tr-Ω¹-inc _ n ·ₚ l ⟩ - ⌞ Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) ⌟ , l¹ ≃∙⟨ Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) .fst , pt1 ⟩ - ⌞ Ωⁿ (1 + k) (n-Tr∙ A (k + (2 + n))) ⌟ , lᵏ ≃∙⟨ Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ _) .fst , pt2 ⟩ - ⌞ Ωⁿ (1 + k) (n-Tr∙ A (1 + k + suc n)) ⌟ , lᵏ ≃∙∎ - where - l¹ : Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) .fst - l¹ = Ω¹-map inc∙ .fst l - - lᵏ : ∀ {n} → ⌞ Ωⁿ (suc k) (n-Tr∙ A n) ⌟ - lᵏ = Ωⁿ-map (1 + k) inc∙ .fst l - - pt1 : Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) · l¹ ≡ lᵏ - pt1 = - Ω¹-map (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) .fst l¹ - ≡⟨ Ω¹-map-∘ (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) inc∙ ·ₚ l ⟩ - Ω¹-map ⌜ Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k) ∘∙ inc∙ ⌝ .fst l - ≡⟨ ap! (n-Tr-Ωⁿ-inc A (suc n) k) ⟩ - Ω¹-map (Ωⁿ-map k inc∙) .fst l - ∎ - - pt2 : Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ (+-sucr k (suc n))) · lᵏ ≡ lᵏ - pt2 = (Ωⁿ-map-∘ (1 + k) _ inc∙ ·ₚ l) - ∙ ap (λ x → Ωⁿ-map (1 + k) x .fst l) (n-Tr∙-reindex-inc (k + (2 + n)) _ _) + n-Tr-Ωⁿ-inc A n (suc k) = homogeneous-funext∙ λ l → trace l .snd where + trace + : (l : ⌞ Ωⁿ (suc k) A ⌟) + → (n-Tr∙ (Ωⁿ (suc k) A) (1 + n) .fst , inc l) + ≃∙ (Ωⁿ (suc k) (n-Tr∙ A (suc k + suc n)) .fst , Ωⁿ-map (suc k) inc∙ .fst l) + trace l = + ⌞ n-Tr∙ (Ω¹ (Ωⁿ k A)) (suc n) ⌟ , inc l ≃∙⟨ n-Tr-Ω¹ _ n .fst , n-Tr-Ω¹-inc _ n ·ₚ l ⟩ + ⌞ Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) ⌟ , l¹ ≃∙⟨ Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) .fst , pt1 ⟩ + ⌞ Ωⁿ (1 + k) (n-Tr∙ A (k + (2 + n))) ⌟ , lᵏ ≃∙⟨ Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ _) .fst , pt2 ⟩ + ⌞ Ωⁿ (1 + k) (n-Tr∙ A (1 + k + suc n)) ⌟ , lᵏ ≃∙∎ + where + l¹ : Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) .fst + l¹ = Ω¹-map inc∙ .fst l + + lᵏ : ∀ {n} → ⌞ Ωⁿ (suc k) (n-Tr∙ A n) ⌟ + lᵏ = Ωⁿ-map (1 + k) inc∙ .fst l + + pt1 : Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) · l¹ ≡ lᵏ + pt1 = + Ω¹-map (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) .fst l¹ + ≡⟨ Ω¹-map-∘ (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) inc∙ ·ₚ l ⟩ + Ω¹-map ⌜ Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k) ∘∙ inc∙ ⌝ .fst l + ≡⟨ ap! (n-Tr-Ωⁿ-inc A (suc n) k) ⟩ + Ω¹-map (Ωⁿ-map k inc∙) .fst l + ∎ + + pt2 : Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ (+-sucr k (suc n))) · lᵏ ≡ lᵏ + pt2 = (Ωⁿ-map-∘ (1 + k) _ inc∙ ·ₚ l) + ∙ ap (λ x → Ωⁿ-map (1 + k) x .fst l) (n-Tr∙-reindex-inc (k + (2 + n)) _ _) ``` --> diff --git a/src/Order/DCPO/Pointed.lagda.md b/src/Order/DCPO/Pointed.lagda.md index 4ee5f0371..49f3d94af 100644 --- a/src/Order/DCPO/Pointed.lagda.md +++ b/src/Order/DCPO/Pointed.lagda.md @@ -179,14 +179,14 @@ namely for any $y$ such that $f y \le y$, $\bigcup (f^{n}(\bot)) \le y$. This follows from som quick induction. ```agda - fⁿ⊥≤fix : ∀ (y : Ob) → f · y ≤ y → ∀ n → fⁿ⊥ n ≤ y + fⁿ⊥≤fix : ∀ y → f · y ≤ y → ∀ n → fⁿ⊥ n ≤ y fⁿ⊥≤fix y p (lift zero) = ¡ fⁿ⊥≤fix y p (lift (suc n)) = f · (fⁿ n bot) ≤⟨ f.monotone (fⁿ⊥≤fix y p (lift n)) ⟩ f · y ≤⟨ p ⟩ y ≤∎ - least-fix : ∀ (y : Ob) → f · y ≤ y → ⋃ fⁿ⊥ fⁿ⊥-dir ≤ y + least-fix : ∀ y → f · y ≤ y → ⋃ fⁿ⊥ fⁿ⊥-dir ≤ y least-fix y p = ⋃.least _ _ _ (fⁿ⊥≤fix y p) ``` @@ -240,7 +240,7 @@ module _ {o ℓ} {D E : DCPO o ℓ} where ```agda is-strictly-scott-continuous : (f : DCPOs.Hom D E) → Type _ is-strictly-scott-continuous f = - ∀ (x : D.Ob) → is-bottom D.poset x → is-bottom E.poset (f · x) + ∀ x → is-bottom D.poset x → is-bottom E.poset (f · x) ``` ```agda diff --git a/src/Order/Frame/Free.lagda.md b/src/Order/Frame/Free.lagda.md index 73d67de25..d805c9352 100644 --- a/src/Order/Frame/Free.lagda.md +++ b/src/Order/Frame/Free.lagda.md @@ -168,7 +168,7 @@ It's also free from the definition of cocompletions that the extended map $\widehat{f}$ satisfies $\widehat{f}(\darr x) = f(x)$. ```agda - mkcomm : ∀ x → mkhom · (↓ (A .fst) x) ≡ f · x + mkcomm : ∀ x → mkhom · ↓ (A .fst) x ≡ f · x mkcomm x = (Lan↓-commutes B.⋃-lubs (f .hom) x) ``` diff --git a/src/Order/Instances/Disjoint.lagda.md b/src/Order/Instances/Disjoint.lagda.md index 3df72c5c8..bab546918 100644 --- a/src/Order/Instances/Disjoint.lagda.md +++ b/src/Order/Instances/Disjoint.lagda.md @@ -90,8 +90,7 @@ function for mapping _out_, by cases: ```agda matchᵖ : ∀ {o ℓ} {R : Poset o ℓ} - → (∀ i → Monotone (F i) R) - → Monotone (Disjoint I F) R + → (∀ i → Monotone (F i) R) → Monotone (Disjoint I F) R matchᵖ cases .hom (i , x) = cases i · x matchᵖ cases .pres-≤ (reflᵢ , x≤y) = cases _ .pres-≤ (x≤y reflᵢ) @@ -116,7 +115,9 @@ Posets-has-set-indexed-coproducts I F = mk where ## Binary coproducts are a special case of indexed coproducts ```agda -⊎≡Disjoint-bool : ∀ {o ℓ} (P Q : Poset o ℓ) → P ⊎ᵖ Q ≡ Disjoint (el! Bool) (if_then P else Q) +⊎≡Disjoint-bool + : ∀ {o ℓ} (P Q : Poset o ℓ) + → P ⊎ᵖ Q ≡ Disjoint (el! Bool) (if_then P else Q) ⊎≡Disjoint-bool P Q = Poset-path λ where .to → match⊎ᵖ (injᵖ true) (injᵖ false) .from → matchᵖ (Bool-elim _ inlᵖ inrᵖ) diff --git a/src/Order/Instances/Lower.lagda.md b/src/Order/Instances/Lower.lagda.md index 5a7c2831f..156776ddb 100644 --- a/src/Order/Instances/Lower.lagda.md +++ b/src/Order/Instances/Lower.lagda.md @@ -109,7 +109,7 @@ operator automatically propositionally truncates.