Merge remote-tracking branch 'origin/main' into flat-records-limits

src/1Lab/Classical.lagda.md

@@ -153,7 +153,7 @@ gives us a section $\Sigma P \to 2$.
 ```agda
 module _ (split : Surjections-split) (P : Ω) where
   section : ∥ ((x : Susp ∣ P ∣) → fibre 2→Σ x) ∥
-  section = split Bool-is-set (Susp-prop-is-set (hlevel 1)) 2→Σ 2→Σ-surjective
+  section = split (hlevel 2) (Susp-prop-is-set (hlevel 1)) 2→Σ 2→Σ-surjective
 ```
 
 But a section is always injective, and the booleans are [[discrete]], so we can

src/1Lab/Equiv.lagda.md

@@ -202,7 +202,7 @@ point with, rather than being a property of points.
 
 ```agda
 fibre : (A → B) → B → Type _
-fibre {A = A} f y = Σ[ x ∈ A ] (f x ≡ y)
+fibre {A = A} f y = Σ[ x ∈ A ] f x ≡ y
 ```
 :::
 
@@ -1094,13 +1094,13 @@ lift-inj p = ap Lift.lower p
 fibre-∘-≃
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
   → {f : B → C} {g : A → B}
-  → ∀ c → fibre (f ∘ g) c ≃ (Σ[ (b , _) ∈ fibre f c ] (fibre g b))
+  → ∀ c → fibre (f ∘ g) c ≃ (Σ[ (b , _) ∈ fibre f c ] fibre g b)
 fibre-∘-≃ {f = f} {g = g} c = Iso→Equiv (fwd , iso bwd invl invr)
     where
-      fwd : fibre (f ∘ g) c → Σ[ (b , _) ∈ fibre f c ] (fibre g b)
+      fwd : fibre (f ∘ g) c → Σ[ (b , _) ∈ fibre f c ] fibre g b
       fwd (a , p) = ((g a) , p) , (a , refl)
 
-      bwd : Σ[ (b , _) ∈ fibre f c ] (fibre g b) → fibre (f ∘ g) c
+      bwd : Σ[ (b , _) ∈ fibre f c ] fibre g b → fibre (f ∘ g) c
       bwd ((b , p) , (a , q)) = a , ap f q ∙ p
 
       invl : ∀ x → fwd (bwd x) ≡ x

src/1Lab/HIT/Truncation.lagda.md

@@ -6,6 +6,7 @@ definition: |
 <!--
 ```agda
 open import 1Lab.Reflection.Induction
+open import 1Lab.Function.Embedding
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HLevel.Closure
 open import 1Lab.Path.Reasoning
@@ -239,16 +240,16 @@ image {A = A} {B = B} f = Σ[ b ∈ B ] ∃[ a ∈ A ] (f a ≡ b)
 
 To see that the `image`{.Agda} indeed implements the concept of image,
 we define a way to factor any map through its image. By the definition
-of image, we have that the map `f-image`{.Agda} is always surjective,
+of image, we have that the map `image-inc`{.Agda} is always surjective,
 and since `∃` is a family of props, the first projection out of
 `image`{.Agda} is an embedding. Thus we factor a map $f$ as $A \epi \im
 f \mono B$.
 
 ```agda
-f-image
+image-inc
   : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
   → (f : A → B) → A → image f
-f-image f x = f x , inc (x , refl)
+image-inc f x = f x , inc (x , refl)
 ```
 
 We now prove the theorem that will let us map out of a propositional
@@ -295,7 +296,7 @@ truncation onto a set using a constant map.
             → ∥ A ∥ → B
 ∥-∥-rec-set {A = A} {B} bset f fconst x =
   ∥-∥-elim {P = λ _ → image f}
-    (λ _ → is-constant→image-is-prop bset f fconst) (f-image f) x .fst
+    (λ _ → is-constant→image-is-prop bset f fconst) (image-inc f) x .fst
 ```
 
 <!--
@@ -491,3 +492,24 @@ instance
     go (squash x y i) f = squash (go x f) (go y f) i
 ```
 -->
+
+<!--
+```agda
+is-embedding→image-inc-is-equiv
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B}
+  → is-embedding f
+  → is-equiv (image-inc f)
+is-embedding→image-inc-is-equiv {f = f} f-emb =
+  is-iso→is-equiv $
+  iso (λ im → fst $ ∥-∥-out (f-emb _) (im .snd))
+    (λ im → Σ-prop-path! (snd $ ∥-∥-out (f-emb _) (im .snd)))
+    (λ _ → refl)
+
+is-embedding→image-equiv
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B}
+  → is-embedding f
+  → A ≃ image f
+is-embedding→image-equiv {f = f} f-emb =
+  image-inc f , is-embedding→image-inc-is-equiv f-emb
+```
+-->

src/1Lab/HLevel.lagda.md

@@ -204,7 +204,7 @@ proof (used in the *definition* of path induction), we can demonstrate
 the application of path induction:
 
 ```agda
-_ : (a : A) → is-contr (Σ[ b ∈ A ] (b ≡ a))
+_ : (a : A) → is-contr (Σ[ b ∈ A ] b ≡ a)
 _ = λ t → record
   { centre = (t , refl)
   ; paths  = λ (s , p) → J' (λ s t p → (t , refl) ≡ (s , p)) (λ t → refl) p
@@ -741,5 +741,15 @@ is-set→cast-pathp
   → PathP (λ i → P (q i)) px py
 is-set→cast-pathp {p = p} {q = q} P {px} {py} set  r =
   coe0→1 (λ i → PathP (λ j → P (set _ _ p q i j)) px py) r
+
+is-set→subst-refl
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {x : A}
+  → (P : A → Type ℓ')
+  → is-set A
+  → (p : x ≡ x)
+  → (px : P x)
+  → subst P p px ≡ px
+is-set→subst-refl {x = x} P set p px i =
+  transp (λ j → P (set x x p refl i j)) i px
 ```
 -->

src/1Lab/Membership.agda

@@ -45,7 +45,7 @@ infix 30 _∉_
 ∫ₚ
   : ∀ {ℓ ℓ' ℓ''} {X : Type ℓ} {ℙX : Type ℓ'} ⦃ m : Membership X ℙX ℓ'' ⦄
   → ℙX → Type _
-∫ₚ {X = X} P = Σ[ x ∈ X ] (x ∈ P)
+∫ₚ {X = X} P = Σ[ x ∈ X ] x ∈ P
 
 -- Notation typeclass for _⊆_. We could always define
 --

src/1Lab/Path.lagda.md

@@ -771,7 +771,7 @@ In Cubical Agda, the relevant *primitive* is the function
 for now. To start with, this is where paths show their difference from
 the notion of equality in set-level type theories: it says that we have
 a function from paths $p : A \is B$ to functions $A \to B$. However,
-it's *not* the case that every $p, q : A \to B$ gives back the *same*
+it's *not* the case that every $p, q : A \is B$ gives back the *same*
 function $A \to B$. Which function you get depends on (and determines) the
 path you put in!
 
@@ -1044,7 +1044,7 @@ inhabitant!
 
 ```agda
 Singleton : ∀ {ℓ} {A : Type ℓ} → A → Type _
-Singleton x = Σ[ y ∈ _ ] (x ≡ y)
+Singleton x = Σ[ y ∈ _ ] x ≡ y
 ```
 
 We're given an inhabitant $y : A$ and a path $p : x \is y$. To identify
@@ -2378,5 +2378,8 @@ _$ₚ_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂} {f g : 
      → f ≡ g → ∀ x → f x ≡ g x
 (f $ₚ x) i = f i x
 {-# INLINE _$ₚ_ #-}
+
+_≠_ : ∀ {ℓ} {A : Type ℓ} → A → A → Type ℓ
+x ≠ y = ¬ x ≡ y
 ```
 -->

src/1Lab/Path/IdentitySystem.lagda.md

@@ -332,12 +332,7 @@ This is known as **Hedberg's theorem**.
 
 opaque
   Discrete→is-set : ∀ {ℓ} {A : Type ℓ} → Discrete A → is-set A
-  Discrete→is-set {A = A} dec =
-    identity-system→hlevel 1 (¬¬-stable-identity-system stable) λ x y f g →
-      funext λ h → absurd (g h)
-    where
-      stable : {x y : A} → ¬ ¬ x ≡ y → x ≡ y
-      stable {x = x} {y = y} ¬¬p with dec {x} {y}
-      ... | yes p = p
-      ... | no ¬p = absurd (¬¬p ¬p)
+  Discrete→is-set {A = A} dec = identity-system→hlevel 1
+    (¬¬-stable-identity-system (dec→dne ⦃ dec ⦄))
+    λ x y f g → funext λ h → absurd (g h)
 ```

src/1Lab/Resizing.lagda.md

@@ -227,9 +227,9 @@ disjunctions, and implications.
 
 <!--
 ```agda
-infixr 6 _∧Ω_
-infixr 5 _∨Ω_
-infixr 4 _→Ω_
+infixr 10 _∧Ω_
+infixr 9 _∨Ω_
+infixr 8 _→Ω_
 ```
 -->
 

src/1Lab/Type.lagda.md

@@ -49,7 +49,7 @@ absurd ()
 
 ¬_ : ∀ {ℓ} → Type ℓ → Type ℓ
 ¬ A = A → ⊥
-infix 3 ¬_
+infix 6 ¬_
 ```
 
 :::{.definition #product-type}

src/1Lab/Underlying.agda

@@ -6,6 +6,8 @@ open import 1Lab.HLevel
 open import 1Lab.Path
 open import 1Lab.Type hiding (Σ-syntax)
 
+open import Data.Bool.Base
+
 module 1Lab.Underlying where
 
 -- Notation class for types which have a chosen projection into a
@@ -54,6 +56,9 @@ instance
   Underlying-Lift ⦃ ua ⦄ .ℓ-underlying = ua .ℓ-underlying
   Underlying-Lift .⌞_⌟ x = ⌞ x .Lift.lower ⌟
 
+  Underlying-Bool : Underlying Bool
+  Underlying-Bool = record { ⌞_⌟ = So }
+
 -- The converse of to-is-true, generalised slightly. If P and Q are
 -- identical inhabitants of some type of structured types, and Q's
 -- underlying type is contractible, then P is inhabited. P's underlying

src/1Lab/Univalence.lagda.md

@@ -95,7 +95,7 @@ open import 1Lab.Equiv.FromPath
 ```agda
 Glue : (A : Type ℓ)
      → {φ : I}
-     → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] (T ≃ A)))
+     → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
      → Type ℓ'
 ```
 

src/Algebra/Group/Cat/Base.lagda.md

@@ -23,7 +23,7 @@ import Cat.Reasoning as CR
 ```
 -->
 
-# The category of groups
+# The category of groups {defines="category-of-groups"}
 
 The category of groups, as the name implies, has its objects the
 `Groups`{.Agda ident=Group}, with the morphisms between them the `group

src/Algebra/Group/Cat/FinitelyComplete.lagda.md

@@ -42,7 +42,7 @@ _forced_ to do this since [right adjoints preserve limits].
 [underlying set]: Algebra.Group.Cat.Base.html#the-underlying-set
 [right adjoints preserve limits]: Cat.Functor.Adjoint.Continuous.html
 
-## The zero group
+## The zero group {defines="zero-group"}
 
 The zero object in the category of groups is given by the unit type,
 equipped with its unique group structure. Correspondingly, we may refer

src/Algebra/Magma.lagda.md

@@ -138,7 +138,7 @@ set, this obviously defines a magma:
 ```agda
 private
   is-magma-imp : is-magma imp
-  is-magma-imp .has-is-set = Bool-is-set
+  is-magma-imp .has-is-set = hlevel 2
 ```
 
 We show it is not commutative or associative by giving counterexamples:

src/Algebra/Ring/Solver.agda

@@ -12,7 +12,6 @@ Horner normal forms are not sparse).
 open import 1Lab.Reflection.Variables
 open import 1Lab.Reflection.Solver
 open import 1Lab.Reflection
-open import 1Lab.Rewrite
 
 open import Algebra.Ring.Cat.Initial
 open import Algebra.Ring.Commutative