Merge branch 'main' into joint-monos

Author: TOTBWF

src/1Lab/Counterexamples/Sigma.lagda.md

@@ -6,7 +6,7 @@ description: |
   the domain of the function.
 ---
 <!--
-```
+```agda
 open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type

src/1Lab/Equiv.lagda.md

@@ -250,7 +250,7 @@ id-equiv .is-eqv y .paths (x , p) i = p (~ i) , λ j → p (~ i ∨ j)
 ```
 
 <!--
-```
+```agda
 -- This helper is for functions f, g that cancel eachother, up to
 -- definitional equality, without any case analysis on the argument:
 
@@ -293,7 +293,7 @@ is-eqv' A B (f , is-equiv) a ψ u0 = inS (
 ```
 
 <!--
-```
+```agda
 equiv-centre : (e : A ≃ B) (y : B) → fibre (e .fst) y
 equiv-centre e y = e .snd .is-eqv y .centre
 

src/1Lab/Equiv/Biinv.lagda.md

@@ -20,7 +20,7 @@ module 1Lab.Equiv.Biinv where
 ```
 
 <!--
-```
+```agda
 private variable
   ℓ : Level
   A B C : Type ℓ

src/1Lab/Equiv/Fibrewise.lagda.md

@@ -31,7 +31,7 @@ x` can be referred as a _fibrewise map_.
 A function like this can be lifted to a function on total spaces:
 
 <!--
-```
+```agda
 private variable
   ℓ : Level
   A B : Type ℓ
@@ -153,3 +153,12 @@ An equivalence over $e$ induces an equivalence of total spaces:
     over→total : P ≃[ e ] Q → Σ A P ≃ Σ B Q
     over→total e' = Σ-ap e λ a → e' a (e.to a) refl
 ```
+
+<!--
+```agda
+subst-fibrewise
+  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {B' : A → Type ℓ''} (g : ∀ x → B x → B' x)
+  → {x y : A} (p : x ≡ y) (h : B x) → subst B' p (g x h) ≡ g y (subst B p h)
+subst-fibrewise {B = B} {B'} g {x} p h = J (λ y p → subst B' p (g x h) ≡ g y (subst B p h)) (transport-refl _ ∙ ap (g x) (sym (transport-refl _))) p
+```
+-->

src/1Lab/Equiv/FromPath.lagda.md

@@ -4,7 +4,7 @@ description: |
   efficient manner, using cubical methods.
 ---
 <!--
-```
+```agda
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path

src/1Lab/Extensionality.agda

@@ -151,20 +151,6 @@ instance
   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 ℓ'}
-    → ⦃ 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)
-
   -- 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
@@ -363,7 +349,12 @@ instance
   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-equiv ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea
+
+  Extensional-emb
+    : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
+    → ⦃ ea : Extensional (A → B) ℓr ⦄ → Extensional (A ↪ B) ℓr
+  Extensional-emb ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea
 
   Extensional-tr-map
     : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}

src/1Lab/Function/Embedding.lagda.md

@@ -24,7 +24,7 @@ module 1Lab.Function.Embedding where
 ```
 
 <!--
-```
+```agda
 private variable
   ℓ ℓ₁ : Level
   A B : Type ℓ

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

@@ -24,7 +24,7 @@ module 1Lab.HLevel.Closure where
 # Closure of h-levels
 
 <!--
-```
+```agda
 private variable
   ℓ ℓ' : Level
   A B C : Type ℓ

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

@@ -2,7 +2,7 @@
 description: Using univalence, we compute the h-level of the universe of n types.
 ---
 <!--
-```
+```agda
 open import 1Lab.HLevel.Closure
 open import 1Lab.Type.Sigma
 open import 1Lab.Univalence
@@ -18,7 +18,7 @@ module 1Lab.HLevel.Universe where
 ```
 
 <!--
-```
+```agda
 private variable
   ℓ : Level
   A B C : Type ℓ

src/1Lab/Membership.agda

@@ -21,7 +21,7 @@ record Membership {ℓ ℓe} (A : Type ℓe) (ℙA : Type ℓ) ℓm : Type (ℓ
   infix 30 _∈_
 
 open Membership ⦃ ... ⦄ using (_∈_) public
-{-# DISPLAY Membership._∈_ i a b = a ∈ b #-}
+{-# DISPLAY Membership._∈_ _ a b = a ∈ b #-}
 
 -- The prototypical instance is given by functions into a universe:
 
@@ -65,7 +65,7 @@ record Inclusion {ℓ} (ℙA : Type ℓ) ℓi : Type (ℓ ⊔ lsuc (ℓi)) where
   infix 30 _⊆_
 
 open Inclusion ⦃ ... ⦄ using (_⊆_) public
-{-# DISPLAY Inclusion._⊆_ i a b = a ⊆ b #-}
+{-# DISPLAY Inclusion._⊆_ _ a b = a ⊆ b #-}
 
 instance
   Inclusion-default