Merge branch 'main' into main

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
 ```
 :::
 
@@ -945,7 +945,7 @@ Lift-ap
 Lift-ap (f , eqv) .fst (lift x) = lift (f x)
 Lift-ap f .snd .is-eqv (lift y) .centre = lift (Equiv.from f y) , ap lift (Equiv.ε f y)
 Lift-ap f .snd .is-eqv (lift y) .paths (lift x , q) i = lift (p i .fst) , λ j → lift (p i .snd j)
-  where p = f .snd .is-eqv y .paths (x , ap Lift.lower q)
+  where p = f .snd .is-eqv y .paths (x , ap lower q)
 ```
 
 ### Involutions
@@ -960,10 +960,12 @@ is-involutive→is-equiv inv = is-iso→is-equiv (iso _ inv inv)
 
 ## Closure properties
 
+:::{.definition #two-out-of-three}
 We will now show a rather fundamental property of equivalences: they are
 closed under *two-out-of-three*. This means that, considering $f : A \to
 B$, $g : B \to C$, and $(g \circ f) : A \to C$ as a set of three things,
 if any two are an equivalence, then so is the third:
+:::
 
 <!--
 ```agda
@@ -1088,19 +1090,19 @@ syntax ≃⟨⟩-syntax x q p = x ≃⟨ p ⟩ q
 lift-inj
   : ∀ {ℓ ℓ'} {A : Type ℓ} {a b : A}
   → lift {ℓ = ℓ'} a ≡ lift {ℓ = ℓ'} b → a ≡ b
-lift-inj p = ap Lift.lower p
+lift-inj p = ap lower p
 
 -- Fibres of composites are given by pairs of fibres.
 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

src/1Lab/HLevel/Closure.lagda.md

@@ -188,6 +188,14 @@ between functions is a function into identities:
   (λ f {x} → f x) (λ f x → f) (λ _ → refl)
   (Π-is-hlevel n bhl)
 
+Π-is-hlevel-inst
+  : ∀ {a b} {A : Type a} {B : A → Type b}
+  → (n : Nat) (Bhl : (x : A) → is-hlevel (B x) n)
+  → is-hlevel (⦃ x : A ⦄ → B x) n
+Π-is-hlevel-inst n bhl = retract→is-hlevel n
+  (λ f ⦃ x ⦄ → f x) (λ f x → f ⦃ x ⦄) (λ _ → refl)
+  (Π-is-hlevel n bhl)
+
 Π-is-hlevel²
   : ∀ {a b c} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
   → (n : Nat) (Bhl : (x : A) (y : B x) → is-hlevel (C x y) n)
@@ -266,13 +274,13 @@ successor universe:
 ```agda
 opaque
   Lift-is-hlevel : ∀ n → is-hlevel A n → is-hlevel (Lift ℓ' A) n
-  Lift-is-hlevel n a-hl = retract→is-hlevel n lift Lift.lower (λ _ → refl) a-hl
+  Lift-is-hlevel n a-hl = retract→is-hlevel n lift lower (λ _ → refl) a-hl
 ```
 
 <!--
 ```agda
   Lift-is-hlevel' : ∀ n → is-hlevel (Lift ℓ' A) n → is-hlevel A n
-  Lift-is-hlevel' n lift-hl = retract→is-hlevel n Lift.lower lift (λ _ → refl) lift-hl
+  Lift-is-hlevel' n lift-hl = retract→is-hlevel n lower lift (λ _ → refl) lift-hl
 ```
 -->
 
@@ -376,6 +384,12 @@ instance opaque
     → H-Level (∀ {x} → S x) n
   H-Level-pi' {n = n} .H-Level.has-hlevel = Π-is-hlevel' n λ _ → hlevel n
 
+  H-Level-pi''
+    : ∀ {n} {S : T → Type ℓ}
+    → ⦃ ∀ {x} → H-Level (S x) n ⦄
+    → H-Level (∀ ⦃ x ⦄ → S x) n
+  H-Level-pi'' {n = n} .H-Level.has-hlevel = Π-is-hlevel-inst n λ _ → hlevel n
+
   H-Level-sigma
     : ∀ {n} {S : T → Type ℓ}
     → ⦃ H-Level T n ⦄ → ⦃ ∀ {x} → H-Level (S x) n ⦄

src/1Lab/HLevel/Universe.lagda.md

@@ -193,7 +193,7 @@ Prop ℓ = n-Type ℓ 1
 ```agda
 ¬Set-is-prop : ¬ is-prop (Set ℓ)
 ¬Set-is-prop prop =
-  Lift.lower $
+  lower $
   transport (ap ∣_∣ (prop (el (Lift _ ⊤) (hlevel 2)) (el (Lift _ ⊥) (hlevel 2)))) (lift tt)
 ```
 -->

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/Reflection/Deriving/Show.agda

@@ -11,6 +11,7 @@ open import Data.Char.Base
 open import Data.Fin.Base
 open import Data.Vec.Base hiding (map)
 open import Data.Nat.Base
+open import Data.Int.Base using (Int ; pos ; negsuc)
 
 open import Meta.Foldable
 open import Meta.Append

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}
@@ -77,6 +77,8 @@ record Lift {a} ℓ (A : Type a) : Type (a ⊔ ℓ) where
 
 <!--
 ```agda
+open Lift public
+
 instance
   Lift-instance : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ A ⦄ → Lift ℓ' A
   Lift-instance ⦃ x ⦄ = lift x
@@ -131,5 +133,10 @@ case x return P of f = f x
 
 {-# INLINE case_of_        #-}
 {-# INLINE case_return_of_ #-}
+
+instance
+  Number-Lift : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ Number A ⦄ → Number (Lift ℓ' A)
+  Number-Lift {ℓ' = ℓ'} ⦃ a ⦄ .Number.Constraint n = Lift ℓ' (a .Number.Constraint n)
+  Number-Lift ⦃ a ⦄ .Number.fromNat n ⦃ lift c ⦄ = lift (a .Number.fromNat n ⦃ c ⦄)
 ```
 -->

src/1Lab/Type/Pi.lagda.md

@@ -1,6 +1,7 @@
 <!--
 ```
 open import 1Lab.Path.Cartesian
+open import 1Lab.Type.Sigma
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
@@ -85,6 +86,12 @@ function≃ dom rng = Iso→Equiv the-iso where
   the-iso .snd .is-iso.linv f =
     funext λ x → rng-iso .is-iso.linv _
                ∙ ap f (dom-iso .is-iso.linv _)
+
+equiv≃ : (A ≃ B) → (C ≃ D) → (A ≃ C) ≃ (B ≃ D)
+equiv≃ x y = Σ-ap (function≃ x y) λ f → prop-ext
+  (is-equiv-is-prop _) (is-equiv-is-prop _)
+  (λ e → ∙-is-equiv (∙-is-equiv ((x e⁻¹) .snd) e) (y .snd))
+  λ e → equiv-cancelr ((x e⁻¹) .snd) (equiv-cancell (y .snd) e)
 ```
 
 

src/1Lab/Type/Pointed.lagda.md

@@ -35,6 +35,8 @@ Those are called **pointed maps**.
 ```agda
 _→∙_ : Type∙ ℓ → Type∙ ℓ' → Type _
 (A , a) →∙ (B , b) = Σ[ f ∈ (A → B) ] (f a ≡ b)
+
+infixr 0 _→∙_
 ```
 
 Pointed maps compose in a straightforward way.
@@ -58,3 +60,18 @@ funext∙ : {f g : A →∙ B}
         → f ≡ g
 funext∙ h pth i = funext h i , pth i
 ```
+
+The product of two pointed types is again a pointed type.
+
+```agda
+_×∙_ : Type∙ ℓ → Type∙ ℓ' → Type∙ (ℓ ⊔ ℓ')
+(A , a) ×∙ (B , b) = A × B , a , b
+
+infixr 5 _×∙_
+
+fst∙ : A ×∙ B →∙ A
+fst∙ = fst , refl
+
+snd∙ : A ×∙ B →∙ B
+snd∙ = snd , refl
+```

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
@@ -52,7 +54,10 @@ instance
     : ∀ {ℓ ℓ'} {A : Type ℓ} ⦃ ua : Underlying A ⦄
     → Underlying (Lift ℓ' A)
   Underlying-Lift ⦃ ua ⦄ .ℓ-underlying = ua .ℓ-underlying
-  Underlying-Lift .⌞_⌟ x = ⌞ x .Lift.lower ⌟
+  Underlying-Lift .⌞_⌟ x = ⌞ x .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
@@ -109,6 +114,13 @@ instance
     → Funlike (f ≡ g) A (λ x → f x ≡ g x)
   Funlike-Homotopy = record { _#_ = happly }
 
+  Funlike-Σ
+    : ∀ {ℓ ℓ' ℓx ℓp} {A : Type ℓ} {B : A → Type ℓ'} {X : Type ℓx} {P : X → Type ℓp}
+    → ⦃ Funlike X A B ⦄
+    → Funlike (Σ X P) A B
+  Funlike-Σ = record { _#_ = λ (f , _) → f #_ }
+  {-# OVERLAPPABLE Funlike-Σ #-}
+
 -- Generalised "sections" (e.g. of a presheaf) notation.
 _ʻ_
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {F : Type ℓ''}