diff --git a/CODINGSTYLE.md b/CODINGSTYLE.md
index e9153c0829..b02c0b2eb0 100644
--- a/CODINGSTYLE.md
+++ b/CODINGSTYLE.md
@@ -128,6 +128,49 @@ strategic endeavour to ensure the longevity, vitality, and success of the
a = construction-of-a
```
+- **Lambda expressions**: When a lambda expression appears as the argument of a
+ function, we always wrap it in parentheses. We do this even if it is the last
+ argument and thus isn't strictly required to be parenthesized. Note that in
+ some rare cases, a lambda expression might appear at the top level. In this
+ case we don't require the lambda expression to be parenthesized.
+
+ There are multiple syntaxes for writing lambda expressions in Agda. Generally,
+ you have the following options:
+
+ 1. Regular lambda expressions without pattern matching:
+
+ ```agda
+ λ x → x
+ ```
+
+ 2. Pattern matching lambda expressions on record types:
+
+ ```agda
+ λ (x , y) → x
+ ```
+
+ This syntax only applies to record types with $η$-equality.
+
+ 3. Pattern matching lambda expressions with `{...}`:
+
+ ```agda
+ λ { (inl x) → ... ; (inr y) → ...}
+ ```
+
+ 4. Pattern matching lambda expressions using the `where` keyword:
+
+ ```agda
+ λ where refl → refl
+ ```
+
+ All four syntaxes are in use in the library, although when possible we try to
+ avoid general pattern matching lambdas, i.e. syntaxes 3 and 4. If need be, we
+ prefer pattern matching using the `where` keyword over the `{...}` syntax.
+ Note that whenever syntax 3 or 4 appear in as part of a construction, the
+ definition should be marked as `abstract`. If computation is necessary for a
+ definition that has these syntaxes in them, this suggests the relevant lambda
+ expression(s) deserve to be factored out as separate definitions.
+
## Code comments
Given that the files in `agda-unimath` are literate Agda markdown files,
diff --git a/scripts/blank_line_conventions.py b/scripts/blank_line_conventions.py
index e1ff9862a0..4a39955f11 100755
--- a/scripts/blank_line_conventions.py
+++ b/scripts/blank_line_conventions.py
@@ -11,7 +11,6 @@
open_tag_pattern = re.compile(r'^```\S+\n', flags=re.MULTILINE)
close_tag_pattern = re.compile(r'\n```$', flags=re.MULTILINE)
-
if __name__ == '__main__':
status = 0
@@ -23,6 +22,10 @@
output = re.sub(r'[ \t]+$', '', inputText, flags=re.MULTILINE)
output = re.sub(r'\n(\s*\n){2,}', '\n\n', output)
+ # Remove blank lines before a `where`
+ output = re.sub(r'\n(\s*\n)+(\s+)where(\s|$)',
+ r'\n\2where\3', output, flags=re.MULTILINE)
+
# # Add blank line after `module ... where`
# output = re.sub(r'(^([ \t]*)module[\s({][^\n]*\n(\2\s[^\n]*\n)*\2\s([^\n]*[\s)}])?where)\s*\n(?=\s*[^\n\s])', r'\1\n\n',
# output, flags=re.MULTILINE)
diff --git a/src/category-theory/category-of-functors.lagda.md b/src/category-theory/category-of-functors.lagda.md
index 346c9bb498..c2486d1ff0 100644
--- a/src/category-theory/category-of-functors.lagda.md
+++ b/src/category-theory/category-of-functors.lagda.md
@@ -82,9 +82,9 @@ module _
( ( equiv-iso-functor-natural-isomorphism-Precategory C D F G) ∘e
( extensionality-functor-is-category-Precategory
C D is-category-D F G))
- ( λ { refl →
- compute-iso-functor-natural-isomorphism-eq-Precategory
- C D F G refl})
+ ( λ where
+ refl →
+ compute-iso-functor-natural-isomorphism-eq-Precategory C D F G refl)
```
## Definitions
diff --git a/src/category-theory/category-of-maps-categories.lagda.md b/src/category-theory/category-of-maps-categories.lagda.md
index 60a307aec2..660aa85375 100644
--- a/src/category-theory/category-of-maps-categories.lagda.md
+++ b/src/category-theory/category-of-maps-categories.lagda.md
@@ -66,7 +66,8 @@ module _
( ( distributive-Π-Σ) ∘e
( equiv-Π-equiv-family
( λ x →
- extensionality-obj-Category (D , is-category-D)
+ extensionality-obj-Category
+ ( D , is-category-D)
( obj-map-Precategory C D F x)
( obj-map-Precategory C D G x))))
( λ K →
@@ -113,10 +114,9 @@ module _
is-equiv-htpy-equiv
( ( equiv-iso-map-natural-isomorphism-map-Precategory C D F G) ∘e
( extensionality-map-is-category-Precategory C D is-category-D F G))
- ( λ
- { refl →
- compute-iso-map-natural-isomorphism-map-eq-Precategory
- C D F G refl})
+ ( λ where
+ refl →
+ compute-iso-map-natural-isomorphism-map-eq-Precategory C D F G refl)
```
## Definitions
diff --git a/src/category-theory/dependent-products-of-categories.lagda.md b/src/category-theory/dependent-products-of-categories.lagda.md
index b5c1aa2c16..6c44867c5b 100644
--- a/src/category-theory/dependent-products-of-categories.lagda.md
+++ b/src/category-theory/dependent-products-of-categories.lagda.md
@@ -50,7 +50,7 @@ module _
equiv-Π-equiv-family
( λ i → extensionality-obj-Category (C i) (x i) (y i)) ∘e
equiv-funext)
- ( λ {refl → refl})
+ ( λ where refl → refl)
Π-Category : Category (l1 ⊔ l2) (l1 ⊔ l3)
pr1 Π-Category = Π-Precategory I (precategory-Category ∘ C)
diff --git a/src/category-theory/dependent-products-of-large-categories.lagda.md b/src/category-theory/dependent-products-of-large-categories.lagda.md
index abb7acd962..3f81e6ee78 100644
--- a/src/category-theory/dependent-products-of-large-categories.lagda.md
+++ b/src/category-theory/dependent-products-of-large-categories.lagda.md
@@ -53,7 +53,7 @@ module _
( equiv-Π-equiv-family
( λ i → extensionality-obj-Large-Category (C i) (x i) (y i))) ∘e
( equiv-funext))
- ( λ {refl → refl})
+ ( λ where refl → refl)
Π-Large-Category : Large-Category (λ l2 → l1 ⊔ α l2) (λ l2 l3 → l1 ⊔ β l2 l3)
large-precategory-Large-Category
diff --git a/src/commutative-algebra/products-ideals-commutative-rings.lagda.md b/src/commutative-algebra/products-ideals-commutative-rings.lagda.md
index cab7a3ee8e..9b7ddaf07d 100644
--- a/src/commutative-algebra/products-ideals-commutative-rings.lagda.md
+++ b/src/commutative-algebra/products-ideals-commutative-rings.lagda.md
@@ -170,25 +170,28 @@ module _
(S : subset-Commutative-Ring l2 A) (T : subset-Commutative-Ring l3 A)
where
- forward-inclusion-preserves-product-ideal-subset-Commutative-Ring :
- leq-ideal-Commutative-Ring A
- ( ideal-subset-Commutative-Ring A (product-subset-Commutative-Ring A S T))
- ( product-ideal-Commutative-Ring A
- ( ideal-subset-Commutative-Ring A S)
- ( ideal-subset-Commutative-Ring A T))
- forward-inclusion-preserves-product-ideal-subset-Commutative-Ring =
- is-ideal-generated-by-subset-ideal-subset-Commutative-Ring A
- ( product-subset-Commutative-Ring A S T)
- ( product-ideal-Commutative-Ring A
- ( ideal-subset-Commutative-Ring A S)
- ( ideal-subset-Commutative-Ring A T))
- ( λ x H →
- apply-universal-property-trunc-Prop H
- ( subset-product-ideal-Commutative-Ring A
- ( ideal-subset-Commutative-Ring A S)
- ( ideal-subset-Commutative-Ring A T)
- ( x))
- ( λ { (s , t , refl) →
+ abstract
+ forward-inclusion-preserves-product-ideal-subset-Commutative-Ring :
+ leq-ideal-Commutative-Ring A
+ ( ideal-subset-Commutative-Ring A
+ ( product-subset-Commutative-Ring A S T))
+ ( product-ideal-Commutative-Ring A
+ ( ideal-subset-Commutative-Ring A S)
+ ( ideal-subset-Commutative-Ring A T))
+ forward-inclusion-preserves-product-ideal-subset-Commutative-Ring =
+ is-ideal-generated-by-subset-ideal-subset-Commutative-Ring A
+ ( product-subset-Commutative-Ring A S T)
+ ( product-ideal-Commutative-Ring A
+ ( ideal-subset-Commutative-Ring A S)
+ ( ideal-subset-Commutative-Ring A T))
+ ( λ x H →
+ apply-universal-property-trunc-Prop H
+ ( subset-product-ideal-Commutative-Ring A
+ ( ideal-subset-Commutative-Ring A S)
+ ( ideal-subset-Commutative-Ring A T)
+ ( x))
+ ( λ where
+ ( s , t , refl) →
contains-product-product-ideal-Commutative-Ring A
( ideal-subset-Commutative-Ring A S)
( ideal-subset-Commutative-Ring A T)
@@ -199,7 +202,7 @@ module _
( pr2 s))
( contains-subset-ideal-subset-Commutative-Ring A T
( pr1 t)
- ( pr2 t))}))
+ ( pr2 t))))
left-backward-inclusion-preserves-product-ideal-subset-Commutative-Ring :
{x s y : type-Commutative-Ring A} →
diff --git a/src/elementary-number-theory/dirichlet-convolution.lagda.md b/src/elementary-number-theory/dirichlet-convolution.lagda.md
index 737e8537a8..0745ebdfe9 100644
--- a/src/elementary-number-theory/dirichlet-convolution.lagda.md
+++ b/src/elementary-number-theory/dirichlet-convolution.lagda.md
@@ -39,8 +39,8 @@ module _
bounded-sum-arithmetic-function-Ring R
( succ-ℕ n)
( λ x → div-ℕ-Decidable-Prop (pr1 x) (succ-ℕ n) (pr2 x))
- ( λ { (pair x K) H →
- mul-Ring R
- ( f ( pair x K))
- ( g ( quotient-div-nonzero-ℕ x (succ-nonzero-ℕ' n) H))})
+ ( λ (x , K) H →
+ mul-Ring R
+ ( f ( pair x K))
+ ( g ( quotient-div-nonzero-ℕ x (succ-nonzero-ℕ' n) H)))
```
diff --git a/src/elementary-number-theory/divisibility-integers.lagda.md b/src/elementary-number-theory/divisibility-integers.lagda.md
index 174731d772..144135cf62 100644
--- a/src/elementary-number-theory/divisibility-integers.lagda.md
+++ b/src/elementary-number-theory/divisibility-integers.lagda.md
@@ -482,7 +482,7 @@ is-zero-sim-unit-ℤ {x} {y} H p =
( λ g → g (inv (β g) ∙ (ap ((u g) *ℤ_) p ∙ right-zero-law-mul-ℤ (u g))))
where
K : is-nonzero-ℤ y → presim-unit-ℤ x y
- K g = H (λ {(pair u v) → g v})
+ K g = H (λ (u , v) → g v)
u : is-nonzero-ℤ y → ℤ
u g = pr1 (pr1 (K g))
v : is-nonzero-ℤ y → ℤ
@@ -547,8 +547,8 @@ transitive-presim-unit-ℤ x y z (pair (pair v K) q) (pair (pair u H) p) =
transitive-sim-unit-ℤ : is-transitive sim-unit-ℤ
transitive-sim-unit-ℤ x y z K H f =
transitive-presim-unit-ℤ x y z
- ( K (λ {(p , q) → f (is-zero-sim-unit-ℤ' H p , q)}))
- ( H (λ {(p , q) → f (p , is-zero-sim-unit-ℤ K q)}))
+ ( K (λ (p , q) → f (is-zero-sim-unit-ℤ' H p , q)))
+ ( H (λ (p , q) → f (p , is-zero-sim-unit-ℤ K q)))
```
### `sim-unit-ℤ x y` holds if and only if `x|y` and `y|x`
diff --git a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
index 992aa4a2fa..dba98f35f5 100644
--- a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
+++ b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
@@ -307,14 +307,15 @@ is-minimal-least-nontrivial-divisor-ℕ n H x K d =
### The least nontrivial divisor of a number `> 1` is nonzero
```agda
-is-nonzero-least-nontrivial-divisor-ℕ :
- (n : ℕ) (H : le-ℕ 1 n) → is-nonzero-ℕ (nat-least-nontrivial-divisor-ℕ n H)
-is-nonzero-least-nontrivial-divisor-ℕ n H =
- is-nonzero-div-ℕ
- ( nat-least-nontrivial-divisor-ℕ n H)
- ( n)
- ( div-least-nontrivial-divisor-ℕ n H)
- ( λ { refl → H})
+abstract
+ is-nonzero-least-nontrivial-divisor-ℕ :
+ (n : ℕ) (H : le-ℕ 1 n) → is-nonzero-ℕ (nat-least-nontrivial-divisor-ℕ n H)
+ is-nonzero-least-nontrivial-divisor-ℕ n H =
+ is-nonzero-div-ℕ
+ ( nat-least-nontrivial-divisor-ℕ n H)
+ ( n)
+ ( div-least-nontrivial-divisor-ℕ n H)
+ ( λ where refl → H)
```
### The least nontrivial divisor of a number `> 1` is prime
diff --git a/src/elementary-number-theory/powers-of-two.lagda.md b/src/elementary-number-theory/powers-of-two.lagda.md
index 9efb3ca6ba..836612d431 100644
--- a/src/elementary-number-theory/powers-of-two.lagda.md
+++ b/src/elementary-number-theory/powers-of-two.lagda.md
@@ -55,49 +55,51 @@ is-nonzero-pair-expansion u v =
( is-nonzero-exp-ℕ 2 u is-nonzero-two-ℕ)
( is-nonzero-succ-ℕ _)
-has-pair-expansion-is-even-or-odd :
- (n : ℕ) → is-even-ℕ n + is-odd-ℕ n → pair-expansion n
-has-pair-expansion-is-even-or-odd n =
- strong-ind-ℕ
- ( λ m → (is-even-ℕ m + is-odd-ℕ m) → (pair-expansion m))
- ( λ x → (0 , 0) , refl)
- ( λ k f →
- ( λ {
- ( inl x) →
- ( let s = has-odd-expansion-is-odd k (is-odd-is-even-succ-ℕ k x)
- in pair
- ( 0 , (succ-ℕ (pr1 s)))
- ( ( ap ((succ-ℕ ∘ succ-ℕ) ∘ succ-ℕ) (left-unit-law-add-ℕ _)) ∙
- ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 s))))) ;
- ( inr x) →
- ( let e : is-even-ℕ k
- e = is-even-is-odd-succ-ℕ k x
-
- t : (pr1 e) ≤-ℕ k
- t = leq-quotient-div-ℕ' 2 k is-nonzero-two-ℕ e
-
- s : (pair-expansion (pr1 e))
- s = f (pr1 e) t (is-decidable-is-even-ℕ (pr1 e))
- in
- pair
- ( succ-ℕ (pr1 (pr1 s)) , pr2 (pr1 s))
- ( ( ap
- ( _*ℕ (succ-ℕ ((pr2 (pr1 s)) *ℕ 2)))
- ( commutative-mul-ℕ (exp-ℕ 2 (pr1 (pr1 s))) 2)) ∙
- ( ( associative-mul-ℕ 2
- ( exp-ℕ 2 (pr1 (pr1 s)))
- ( succ-ℕ ((pr2 (pr1 s)) *ℕ 2))) ∙
- ( ( ap (2 *ℕ_) (pr2 s)) ∙
- ( ( ap succ-ℕ
- ( left-successor-law-add-ℕ (0 +ℕ (pr1 e)) (pr1 e))) ∙
- ( ( ap
- ( succ-ℕ ∘ succ-ℕ)
- ( ap (_+ℕ (pr1 e)) (left-unit-law-add-ℕ (pr1 e)))) ∙
+abstract
+ has-pair-expansion-is-even-or-odd :
+ (n : ℕ) → is-even-ℕ n + is-odd-ℕ n → pair-expansion n
+ has-pair-expansion-is-even-or-odd n =
+ strong-ind-ℕ
+ ( λ m → (is-even-ℕ m + is-odd-ℕ m) → (pair-expansion m))
+ ( λ x → (0 , 0) , refl)
+ ( λ k f →
+ ( λ where
+ ( inl x) →
+ ( let s = has-odd-expansion-is-odd k (is-odd-is-even-succ-ℕ k x)
+ in
+ pair
+ ( 0 , (succ-ℕ (pr1 s)))
+ ( ( ap ((succ-ℕ ∘ succ-ℕ) ∘ succ-ℕ) (left-unit-law-add-ℕ _)) ∙
+ ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 s)))))
+ ( inr x) →
+ ( let e : is-even-ℕ k
+ e = is-even-is-odd-succ-ℕ k x
+
+ t : (pr1 e) ≤-ℕ k
+ t = leq-quotient-div-ℕ' 2 k is-nonzero-two-ℕ e
+
+ s : (pair-expansion (pr1 e))
+ s = f (pr1 e) t (is-decidable-is-even-ℕ (pr1 e))
+ in
+ pair
+ ( succ-ℕ (pr1 (pr1 s)) , pr2 (pr1 s))
+ ( ( ap
+ ( _*ℕ (succ-ℕ ((pr2 (pr1 s)) *ℕ 2)))
+ ( commutative-mul-ℕ (exp-ℕ 2 (pr1 (pr1 s))) 2)) ∙
+ ( ( associative-mul-ℕ 2
+ ( exp-ℕ 2 (pr1 (pr1 s)))
+ ( succ-ℕ ((pr2 (pr1 s)) *ℕ 2))) ∙
+ ( ( ap (2 *ℕ_) (pr2 s)) ∙
+ ( ( ap succ-ℕ
+ ( left-successor-law-add-ℕ (0 +ℕ (pr1 e)) (pr1 e))) ∙
( ( ap
( succ-ℕ ∘ succ-ℕ)
- ( inv (right-two-law-mul-ℕ (pr1 e)))) ∙
- ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 e))))))))))}))
- ( n)
+ ( ap (_+ℕ (pr1 e)) (left-unit-law-add-ℕ (pr1 e)))) ∙
+ ( ( ap
+ ( succ-ℕ ∘ succ-ℕ)
+ ( inv (right-two-law-mul-ℕ (pr1 e)))) ∙
+ ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 e))))))))))))
+ ( n)
has-pair-expansion : (n : ℕ) → pair-expansion n
has-pair-expansion n =
diff --git a/src/finite-group-theory/concrete-quaternion-group.lagda.md b/src/finite-group-theory/concrete-quaternion-group.lagda.md
index d03507a4e9..c7c9128a36 100644
--- a/src/finite-group-theory/concrete-quaternion-group.lagda.md
+++ b/src/finite-group-theory/concrete-quaternion-group.lagda.md
@@ -12,11 +12,11 @@ open import elementary-number-theory.natural-numbers
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
-open import foundation.isolated-points
+open import foundation.isolated-elements
open import foundation.transport-along-identifications
open import foundation.universe-levels
-open import univalent-combinatorics.complements-isolated-points
+open import univalent-combinatorics.complements-isolated-elements
open import univalent-combinatorics.cubes
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.equivalences-cubes
@@ -37,7 +37,7 @@ equiv-face-cube :
( map-axis-equiv-cube (succ-ℕ k) X Y e d a))
equiv-face-cube k X Y e d a =
pair
- ( equiv-complement-point-UU-Fin k
+ ( equiv-complement-element-UU-Fin k
( pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
( pair
( dim-cube-UU-Fin (succ-ℕ k) Y)
@@ -48,7 +48,7 @@ equiv-face-cube k X Y e d a =
( equiv-tr
( axis-cube (succ-ℕ k) Y)
( inv
- ( natural-inclusion-equiv-complement-isolated-point
+ ( natural-inclusion-equiv-complement-isolated-element
( dim-equiv-cube (succ-ℕ k) X Y e)
( pair d
( λ z →
@@ -68,7 +68,7 @@ equiv-face-cube k X Y e d a =
( refl)
( d')))) ∘e
( axis-equiv-cube (succ-ℕ k) X Y e
- ( inclusion-complement-point-UU-Fin k
+ ( inclusion-complement-element-UU-Fin k
( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')))
cube-with-labeled-faces :
diff --git a/src/finite-group-theory/orbits-permutations.lagda.md b/src/finite-group-theory/orbits-permutations.lagda.md
index fb5cbb2b6e..b3549cb019 100644
--- a/src/finite-group-theory/orbits-permutations.lagda.md
+++ b/src/finite-group-theory/orbits-permutations.lagda.md
@@ -463,12 +463,11 @@ module _
apply-universal-property-trunc-Prop
( Q)
( pr1 same-orbits-permutation a c)
- ( λ { (k2 , q) →
- ( unit-trunc-Prop
- ( pair
- ( k2 +ℕ k1)
- ( (iterate-add-ℕ k2 k1 (map-equiv f) a) ∙
- ( ap (iterate k2 (map-equiv f)) p ∙ q))))}))
+ ( λ (k2 , q) →
+ unit-trunc-Prop
+ ( ( k2 +ℕ k1) ,
+ ( ( iterate-add-ℕ k2 k1 (map-equiv f) a) ∙
+ ( ap (iterate k2 (map-equiv f)) p ∙ q)))))
abstract
is-decidable-same-orbits-permutation :
@@ -1126,23 +1125,25 @@ module _
(λ pa → lemma2 g (pair (pr1 pa) (inl (pr2 pa)))))
( is-equiv-is-prop is-prop-type-trunc-Prop
( is-prop-type-Prop (coprod-sim-Equivalence-Relation-a-b-Prop g P x))
- ( λ {
- (inl T) →
- apply-universal-property-trunc-Prop T
- ( prop-Equivalence-Relation (same-orbits-permutation-count g) x a)
- ( λ pa →
- lemma3
- ( lemma2
- ( composition-transposition-a-b g)
- ( pair (pr1 pa) (inl (pr2 pa))))) ;
- (inr T) →
- apply-universal-property-trunc-Prop T
- ( prop-Equivalence-Relation (same-orbits-permutation-count g) x a)
- ( λ pa →
- lemma3
- ( lemma2
- ( composition-transposition-a-b g)
- ( pair (pr1 pa) (inr (pr2 pa)))))}))
+ ( λ where
+ ( inl T) →
+ apply-universal-property-trunc-Prop T
+ ( prop-Equivalence-Relation
+ ( same-orbits-permutation-count g) x a)
+ ( λ pa →
+ lemma3
+ ( lemma2
+ ( composition-transposition-a-b g)
+ ( pair (pr1 pa) (inl (pr2 pa)))))
+ ( inr T) →
+ apply-universal-property-trunc-Prop T
+ ( prop-Equivalence-Relation
+ ( same-orbits-permutation-count g) x a)
+ ( λ pa →
+ lemma3
+ ( lemma2
+ ( composition-transposition-a-b g)
+ ( (pr1 pa) , (inr (pr2 pa)))))))
where
minimal-element-iterate-2-a-b :
( g : X ≃ X) →
@@ -1170,17 +1171,18 @@ module _
equal-iterate-transposition-same-orbits g pa k ineq =
equal-iterate-transposition x g
( λ k' → le-ℕ k' (pr1 (minimal-element-iterate-2-a-b g pa)))
- ( λ k' p → pair
- ( λ q →
- contradiction-le-ℕ k'
- ( pr1 (minimal-element-iterate-2-a-b g pa))
- ( p)
- ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inl q)))
- ( λ r →
- contradiction-le-ℕ k'
- ( pr1 (minimal-element-iterate-2-a-b g pa))
- ( p)
- ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inr r))))
+ ( λ k' p →
+ pair
+ ( λ q →
+ contradiction-le-ℕ k'
+ ( pr1 (minimal-element-iterate-2-a-b g pa))
+ ( p)
+ ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inl q)))
+ ( λ r →
+ contradiction-le-ℕ k'
+ ( pr1 (minimal-element-iterate-2-a-b g pa))
+ ( p)
+ ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inr r))))
( λ k' ineq' _ →
transitive-le-ℕ k'
( succ-ℕ k')
diff --git a/src/finite-group-theory/transpositions.lagda.md b/src/finite-group-theory/transpositions.lagda.md
index 6e2f1f1ff4..eea267b7ed 100644
--- a/src/finite-group-theory/transpositions.lagda.md
+++ b/src/finite-group-theory/transpositions.lagda.md
@@ -263,19 +263,19 @@ module _
is-not-identity-swap-2-Element-Type
( 2-element-type-2-Element-Decidable-Subtype P)
( eq-htpy-equiv
- ( λ { (pair x p) →
- eq-pair-Σ
- ( ( ap
- ( map-transposition' P x)
- ( eq-is-prop
- ( is-prop-is-decidable
- ( is-prop-is-in-2-Element-Decidable-Subtype P x))
- { y =
- is-decidable-subtype-subtype-2-Element-Decidable-Subtype
- ( P)
- ( x)})) ∙
- ( htpy-eq f x))
- ( eq-is-in-2-Element-Decidable-Subtype P)}))
+ ( λ (x , p) →
+ eq-pair-Σ
+ ( ( ap
+ ( map-transposition' P x)
+ ( eq-is-prop
+ ( is-prop-is-decidable
+ ( is-prop-is-in-2-Element-Decidable-Subtype P x))
+ { y =
+ is-decidable-subtype-subtype-2-Element-Decidable-Subtype
+ ( P)
+ ( x)})) ∙
+ ( htpy-eq f x))
+ ( eq-is-in-2-Element-Decidable-Subtype P)))
```
### Any transposition on a type equipped with a counting is a standard transposition
diff --git a/src/foundation-core/empty-types.lagda.md b/src/foundation-core/empty-types.lagda.md
index 09db14d352..273b55df60 100644
--- a/src/foundation-core/empty-types.lagda.md
+++ b/src/foundation-core/empty-types.lagda.md
@@ -101,6 +101,9 @@ abstract
empty-Prop : Prop lzero
pr1 empty-Prop = empty
pr2 empty-Prop = is-prop-empty
+
+is-prop-is-empty : {l : Level} {A : UU l} → is-empty A → is-prop A
+is-prop-is-empty is-empty-A = ex-falso ∘ is-empty-A
```
### The empty type is a set
diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md
index 0521f57df2..fe08804f1a 100644
--- a/src/foundation-core/equivalences.lagda.md
+++ b/src/foundation-core/equivalences.lagda.md
@@ -548,40 +548,41 @@ module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where
- is-emb-is-equiv :
- {f : A → B} → is-equiv f → (x y : A) → is-equiv (ap f {x} {y})
- is-emb-is-equiv {f} H x y =
- is-equiv-is-invertible
- ( λ p →
- ( inv (is-retraction-map-inv-is-equiv H x)) ∙
- ( ( ap (map-inv-is-equiv H) p) ∙
- ( is-retraction-map-inv-is-equiv H y)))
- ( λ p →
- ( ap-concat f
- ( inv (is-retraction-map-inv-is-equiv H x))
- ( ap (map-inv-is-equiv H) p ∙ is-retraction-map-inv-is-equiv H y)) ∙
- ( ( ap-binary
- ( λ u v → u ∙ v)
- ( ap-inv f (is-retraction-map-inv-is-equiv H x))
- ( ( ap-concat f
- ( ap (map-inv-is-equiv H) p)
- ( is-retraction-map-inv-is-equiv H y)) ∙
- ( ap-binary
- ( λ u v → u ∙ v)
- ( inv (ap-comp f (map-inv-is-equiv H) p))
- ( inv (coherence-map-inv-is-equiv H y))))) ∙
- ( inv
- ( left-transpose-eq-concat
- ( ap f (is-retraction-map-inv-is-equiv H x))
- ( p)
- ( ( ap (f ∘ map-inv-is-equiv H) p) ∙
- ( is-section-map-inv-is-equiv H (f y)))
- ( ( ap-binary
+ abstract
+ is-emb-is-equiv :
+ {f : A → B} → is-equiv f → (x y : A) → is-equiv (ap f {x} {y})
+ is-emb-is-equiv {f} H x y =
+ is-equiv-is-invertible
+ ( λ p →
+ ( inv (is-retraction-map-inv-is-equiv H x)) ∙
+ ( ( ap (map-inv-is-equiv H) p) ∙
+ ( is-retraction-map-inv-is-equiv H y)))
+ ( λ p →
+ ( ap-concat f
+ ( inv (is-retraction-map-inv-is-equiv H x))
+ ( ap (map-inv-is-equiv H) p ∙ is-retraction-map-inv-is-equiv H y)) ∙
+ ( ( ap-binary
+ ( λ u v → u ∙ v)
+ ( ap-inv f (is-retraction-map-inv-is-equiv H x))
+ ( ( ap-concat f
+ ( ap (map-inv-is-equiv H) p)
+ ( is-retraction-map-inv-is-equiv H y)) ∙
+ ( ap-binary
( λ u v → u ∙ v)
- ( inv (coherence-map-inv-is-equiv H x))
- ( inv (ap-id p))) ∙
- ( nat-htpy (is-section-map-inv-is-equiv H) p))))))
- ( λ {refl → left-inv (is-retraction-map-inv-is-equiv H x)})
+ ( inv (ap-comp f (map-inv-is-equiv H) p))
+ ( inv (coherence-map-inv-is-equiv H y))))) ∙
+ ( inv
+ ( left-transpose-eq-concat
+ ( ap f (is-retraction-map-inv-is-equiv H x))
+ ( p)
+ ( ( ap (f ∘ map-inv-is-equiv H) p) ∙
+ ( is-section-map-inv-is-equiv H (f y)))
+ ( ( ap-binary
+ ( λ u v → u ∙ v)
+ ( inv (coherence-map-inv-is-equiv H x))
+ ( inv (ap-id p))) ∙
+ ( nat-htpy (is-section-map-inv-is-equiv H) p))))))
+ ( λ where refl → left-inv (is-retraction-map-inv-is-equiv H x))
equiv-ap :
(e : A ≃ B) (x y : A) → (x ＝ y) ≃ (map-equiv e x ＝ map-equiv e y)
diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md
index fadb971eba..f55b64f2b5 100644
--- a/src/foundation-core/propositions.lagda.md
+++ b/src/foundation-core/propositions.lagda.md
@@ -160,7 +160,7 @@ module _
abstract
is-prop-equiv : A ≃ B → is-prop B → is-prop A
- is-prop-equiv (pair f is-equiv-f) = is-prop-is-equiv is-equiv-f
+ is-prop-equiv (f , is-equiv-f) = is-prop-is-equiv is-equiv-f
module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
@@ -173,7 +173,7 @@ module _
abstract
is-prop-equiv' : A ≃ B → is-prop A → is-prop B
- is-prop-equiv' (pair f is-equiv-f) = is-prop-is-equiv' is-equiv-f
+ is-prop-equiv' (f , is-equiv-f) = is-prop-is-equiv' is-equiv-f
```
### Propositions are closed under dependent pair types
@@ -250,8 +250,7 @@ abstract
((x : A) → is-prop (B x)) → is-prop ({x : A} → B x)
is-prop-Π' {l1} {l2} {A} {B} H =
is-prop-equiv
- ( pair
- ( λ f x → f {x})
+ ( ( λ f x → f {x}) ,
( is-equiv-is-invertible
( λ g {x} → g x)
( refl-htpy)
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index e243af330c..3e4e87a3c6 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -158,7 +158,7 @@ open import foundation.interchange-law public
open import foundation.intersections-subtypes public
open import foundation.invertible-maps public
open import foundation.involutions public
-open import foundation.isolated-points public
+open import foundation.isolated-elements public
open import foundation.isomorphisms-of-sets public
open import foundation.iterated-cartesian-product-types public
open import foundation.iterating-automorphisms public
diff --git a/src/foundation/0-connected-types.lagda.md b/src/foundation/0-connected-types.lagda.md
index 85c43e399e..021246d291 100644
--- a/src/foundation/0-connected-types.lagda.md
+++ b/src/foundation/0-connected-types.lagda.md
@@ -96,14 +96,15 @@ is-0-connected-is-surjective-point a H =
( mere-eq-Prop a x)
( λ u → unit-trunc-Prop (pr2 u)))
-is-surjective-point-is-0-connected :
- {l1 : Level} {A : UU l1} (a : A) →
- is-0-connected A → is-surjective (point a)
-is-surjective-point-is-0-connected a H x =
- apply-universal-property-trunc-Prop
- ( mere-eq-is-0-connected H a x)
- ( trunc-Prop (fiber (point a) x))
- ( λ {refl → unit-trunc-Prop (pair star refl)})
+abstract
+ is-surjective-point-is-0-connected :
+ {l1 : Level} {A : UU l1} (a : A) →
+ is-0-connected A → is-surjective (point a)
+ is-surjective-point-is-0-connected a H x =
+ apply-universal-property-trunc-Prop
+ ( mere-eq-is-0-connected H a x)
+ ( trunc-Prop (fiber (point a) x))
+ ( λ where refl → unit-trunc-Prop (star , refl))
is-trunc-map-ev-point-is-connected :
{l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (a : A) →
@@ -117,7 +118,7 @@ is-trunc-map-ev-point-is-connected k {A} {B} a H K =
( universal-property-contr-is-contr star is-contr-unit B))
( is-trunc-map-precomp-Π-is-surjective k
( is-surjective-point-is-0-connected a H)
- ( λ _ → pair B K))
+ ( λ _ → (B , K)))
equiv-dependent-universal-property-is-0-connected :
{l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
@@ -140,11 +141,11 @@ abstract
is-surjective-fiber-inclusion :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
is-0-connected A → (a : A) → is-surjective (fiber-inclusion B a)
- is-surjective-fiber-inclusion {B = B} C a (pair x b) =
+ is-surjective-fiber-inclusion {B = B} C a (x , b) =
apply-universal-property-trunc-Prop
( mere-eq-is-0-connected C a x)
- ( trunc-Prop (fiber (fiber-inclusion B a) (pair x b)))
- ( λ { refl → unit-trunc-Prop (pair b refl)})
+ ( trunc-Prop (fiber (fiber-inclusion B a) (x , b)))
+ ( λ where refl → unit-trunc-Prop (b , refl))
abstract
mere-eq-is-surjective-fiber-inclusion :
@@ -153,7 +154,7 @@ abstract
(x : A) → mere-eq a x
mere-eq-is-surjective-fiber-inclusion a H x =
apply-universal-property-trunc-Prop
- ( H (λ x → unit) (pair x star))
+ ( H (λ x → unit) (x , star))
( mere-eq-Prop a x)
( λ u → unit-trunc-Prop (ap pr1 (pr2 u)))
diff --git a/src/foundation/apartness-relations.lagda.md b/src/foundation/apartness-relations.lagda.md
index cdeaaa2db6..b2dcc72e84 100644
--- a/src/foundation/apartness-relations.lagda.md
+++ b/src/foundation/apartness-relations.lagda.md
@@ -186,29 +186,31 @@ module _
unit-trunc-Prop
( x , symmetric-apart-Type-With-Apartness Y (f x) (g x) a))
- is-cotransitive-apart-function-into-Type-With-Apartness :
- is-cotransitive (rel-apart-function-into-Type-With-Apartness X Y)
- is-cotransitive-apart-function-into-Type-With-Apartness f g h H =
- apply-universal-property-trunc-Prop H
- ( disj-Prop
- ( rel-apart-function-into-Type-With-Apartness X Y f h)
- ( rel-apart-function-into-Type-With-Apartness X Y g h))
- ( λ (x , a) →
- apply-universal-property-trunc-Prop
- ( cotransitive-apart-Type-With-Apartness Y (f x) (g x) (h x) a)
- ( disj-Prop
- ( rel-apart-function-into-Type-With-Apartness X Y f h)
- ( rel-apart-function-into-Type-With-Apartness X Y g h))
- ( λ { (inl b) →
+ abstract
+ is-cotransitive-apart-function-into-Type-With-Apartness :
+ is-cotransitive (rel-apart-function-into-Type-With-Apartness X Y)
+ is-cotransitive-apart-function-into-Type-With-Apartness f g h H =
+ apply-universal-property-trunc-Prop H
+ ( disj-Prop
+ ( rel-apart-function-into-Type-With-Apartness X Y f h)
+ ( rel-apart-function-into-Type-With-Apartness X Y g h))
+ ( λ (x , a) →
+ apply-universal-property-trunc-Prop
+ ( cotransitive-apart-Type-With-Apartness Y (f x) (g x) (h x) a)
+ ( disj-Prop
+ ( rel-apart-function-into-Type-With-Apartness X Y f h)
+ ( rel-apart-function-into-Type-With-Apartness X Y g h))
+ ( λ where
+ ( inl b) →
inl-disj-Prop
( rel-apart-function-into-Type-With-Apartness X Y f h)
( rel-apart-function-into-Type-With-Apartness X Y g h)
- ( unit-trunc-Prop (x , b)) ;
- (inr b) →
+ ( unit-trunc-Prop (x , b))
+ ( inr b) →
inr-disj-Prop
( rel-apart-function-into-Type-With-Apartness X Y f h)
( rel-apart-function-into-Type-With-Apartness X Y g h)
- ( unit-trunc-Prop (x , b))}))
+ ( unit-trunc-Prop (x , b))))
exp-Type-With-Apartness : Type-With-Apartness (l1 ⊔ l2) (l1 ⊔ l3)
pr1 exp-Type-With-Apartness = X → type-Type-With-Apartness Y
diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md
index 5aaa57af12..fe2331b54d 100644
--- a/src/foundation/connected-types.lagda.md
+++ b/src/foundation/connected-types.lagda.md
@@ -106,6 +106,6 @@ module _
( trunc (succ-𝕋 k) A)
( unit-trunc a)
( unit-trunc x))
- ( λ { refl → refl})
+ ( λ where refl → refl)
( center (K a x)))))
```
diff --git a/src/foundation/coproduct-decompositions-subuniverse.lagda.md b/src/foundation/coproduct-decompositions-subuniverse.lagda.md
index 16e7edb589..cd0f85fdbe 100644
--- a/src/foundation/coproduct-decompositions-subuniverse.lagda.md
+++ b/src/foundation/coproduct-decompositions-subuniverse.lagda.md
@@ -511,7 +511,7 @@ module _
( inclusion-subuniverse P (pr1 x))
( equiv-is-empty is-empty-raise-empty ( pr2 x)))
( eq-is-prop (is-prop-type-Prop (P _))))
- ( eq-is-prop is-prop-is-empty)))
+ ( eq-is-prop is-property-is-empty)))
( ( raise-empty l1 , C1) , is-empty-raise-empty)) ∘e
( ( inv-associative-Σ _ _ _) ∘e
( ( equiv-tot (λ _ → commutative-prod)) ∘e
diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md
index 718e1505c1..8d29fe181e 100644
--- a/src/foundation/embeddings.lagda.md
+++ b/src/foundation/embeddings.lagda.md
@@ -276,10 +276,11 @@ module _
is-emb f
is-emb-equiv-refl-to-refl e p x y =
is-equiv-htpy-equiv
- (inv-equiv (e x y))
- λ { refl →
- inv (is-retraction-map-inv-equiv (e x x) refl) ∙
- ap (map-equiv (inv-equiv (e x x))) (p x)}
+ ( inv-equiv (e x y))
+ ( λ where
+ refl →
+ inv (is-retraction-map-inv-equiv (e x x) refl) ∙
+ ap (map-equiv (inv-equiv (e x x))) (p x))
```
### Embeddings are closed under pullback
diff --git a/src/foundation/empty-types.lagda.md b/src/foundation/empty-types.lagda.md
index fdd6b8876b..5f689d7bfa 100644
--- a/src/foundation/empty-types.lagda.md
+++ b/src/foundation/empty-types.lagda.md
@@ -93,16 +93,16 @@ raise-ex-falso-emb l =
### Being empty is a proposition
```agda
-is-prop-is-empty : {l : Level} {A : UU l} → is-prop (is-empty A)
-is-prop-is-empty = is-prop-function-type is-prop-empty
+is-property-is-empty : {l : Level} {A : UU l} → is-prop (is-empty A)
+is-property-is-empty = is-prop-function-type is-prop-empty
is-empty-Prop : {l1 : Level} → UU l1 → Prop l1
pr1 (is-empty-Prop A) = is-empty A
-pr2 (is-empty-Prop A) = is-prop-is-empty
+pr2 (is-empty-Prop A) = is-property-is-empty
is-nonempty-Prop : {l1 : Level} → UU l1 → Prop l1
pr1 (is-nonempty-Prop A) = is-nonempty A
-pr2 (is-nonempty-Prop A) = is-prop-is-empty
+pr2 (is-nonempty-Prop A) = is-property-is-empty
```
```agda
@@ -163,5 +163,5 @@ pr2 (is-contr-type-is-empty l) x =
( equiv-is-empty
is-empty-raise-empty
( is-in-subuniverse-inclusion-subuniverse is-empty-Prop x)))
- ( eq-is-prop is-prop-is-empty)
+ ( eq-is-prop is-property-is-empty)
```
diff --git a/src/foundation/functoriality-coproduct-types.lagda.md b/src/foundation/functoriality-coproduct-types.lagda.md
index 0cb0368127..ff730932bc 100644
--- a/src/foundation/functoriality-coproduct-types.lagda.md
+++ b/src/foundation/functoriality-coproduct-types.lagda.md
@@ -247,11 +247,11 @@ module _
is-surjective-map-coprod s s' (inl x) =
apply-universal-property-trunc-Prop (s x)
( trunc-Prop (fiber (map-coprod _ _) (inl x)))
- ( λ {(a , p) → unit-trunc-Prop (inl a , ap inl p)})
+ ( λ (a , p) → unit-trunc-Prop (inl a , ap inl p))
is-surjective-map-coprod s s' (inr x) =
apply-universal-property-trunc-Prop (s' x)
( trunc-Prop (fiber (map-coprod _ _) (inr x)))
- ( λ {(a , p) → unit-trunc-Prop (inr a , ap inr p)})
+ ( λ (a , p) → unit-trunc-Prop (inr a , ap inr p))
```
### For any two maps `f : A → B` and `g : C → D`, there is at most one pair of maps `f' : A → B` and `g' : C → D` such that `f' + g' = f + g`
@@ -517,20 +517,22 @@ module _
(eq-equiv-eq-map-equiv refl)
(eq-equiv-eq-map-equiv refl)
- is-section-map-inv-mutually-exclusive-coprod :
- (map-inv-mutually-exclusive-coprod ∘ map-mutually-exclusive-coprod) ~ id
- is-section-map-inv-mutually-exclusive-coprod e =
- eq-htpy-equiv (
- λ { (inl p) →
+ abstract
+ is-section-map-inv-mutually-exclusive-coprod :
+ (map-inv-mutually-exclusive-coprod ∘ map-mutually-exclusive-coprod) ~ id
+ is-section-map-inv-mutually-exclusive-coprod e =
+ eq-htpy-equiv
+ ( λ where
+ ( inl p) →
ap
( pr1)
( is-retraction-map-inv-equiv-left-summand
- ( map-equiv e (inl p) , left-to-left ¬PQ' e (inl p) star)) ;
- (inr q) →
+ ( map-equiv e (inl p) , left-to-left ¬PQ' e (inl p) star))
+ ( inr q) →
ap
( pr1)
( is-retraction-map-inv-equiv-right-summand
- ( map-equiv e (inr q) , right-to-right ¬P'Q e (inr q) star))})
+ ( map-equiv e (inr q) , right-to-right ¬P'Q e (inr q) star)))
equiv-mutually-exclusive-coprod :
((P + Q) ≃ (P' + Q')) ≃ ((P ≃ P') × (Q ≃ Q'))
diff --git a/src/foundation/functoriality-set-truncation.lagda.md b/src/foundation/functoriality-set-truncation.lagda.md
index 9756288cf2..c7bd3f85a4 100644
--- a/src/foundation/functoriality-set-truncation.lagda.md
+++ b/src/foundation/functoriality-set-truncation.lagda.md
@@ -199,11 +199,10 @@ module _
apply-universal-property-trunc-Prop
( H b)
( trunc-Prop (fiber (map-trunc-Set f) (unit-trunc-Set b)))
- ( λ { (pair a p) →
- unit-trunc-Prop
- ( pair
- ( unit-trunc-Set a)
- ( naturality-unit-trunc-Set f a ∙ ap unit-trunc-Set p))}))
+ ( λ (a , p) →
+ unit-trunc-Prop
+ ( ( unit-trunc-Set a) ,
+ ( naturality-unit-trunc-Set f a ∙ ap unit-trunc-Set p))))
```
### If the set truncation of a map `f` is surjective, then `f` is surjective
@@ -216,16 +215,17 @@ module _
apply-universal-property-trunc-Prop
( H (unit-trunc-Set b))
( trunc-Prop (fiber f b))
- ( λ { (pair x p) →
- apply-universal-property-trunc-Prop
- ( is-surjective-unit-trunc-Set A x)
- ( trunc-Prop (fiber f b))
- ( λ { (pair a refl) →
- apply-universal-property-trunc-Prop
- ( apply-effectiveness-unit-trunc-Set
- ( inv (naturality-unit-trunc-Set f a) ∙ p))
- ( trunc-Prop (fiber f b))
- ( λ q → unit-trunc-Prop (pair a q))})})
+ ( λ (x , p) →
+ apply-universal-property-trunc-Prop
+ ( is-surjective-unit-trunc-Set A x)
+ ( trunc-Prop (fiber f b))
+ ( λ where
+ ( a , refl) →
+ apply-universal-property-trunc-Prop
+ ( apply-effectiveness-unit-trunc-Set
+ ( inv (naturality-unit-trunc-Set f a) ∙ p))
+ ( trunc-Prop (fiber f b))
+ ( λ q → unit-trunc-Prop (a , q))))
```
### Set truncation preserves the image of a map
@@ -248,7 +248,8 @@ module _
( is-injective-is-emb (is-emb-inclusion-im f)))
emb-trunc-im-Set : type-trunc-Set (im f) ↪ type-trunc-Set B
- emb-trunc-im-Set = pair inclusion-trunc-im-Set is-emb-inclusion-trunc-im-Set
+ pr1 emb-trunc-im-Set = inclusion-trunc-im-Set
+ pr2 emb-trunc-im-Set = is-emb-inclusion-trunc-im-Set
abstract
is-injective-inclusion-trunc-im-Set : is-injective inclusion-trunc-im-Set
@@ -265,8 +266,8 @@ module _
( preserves-comp-map-trunc-Set (inclusion-im f) (map-unit-im f))
hom-slice-trunc-im-Set : hom-slice (map-trunc-Set f) inclusion-trunc-im-Set
- hom-slice-trunc-im-Set =
- pair map-hom-slice-trunc-im-Set triangle-hom-slice-trunc-im-Set
+ pr1 hom-slice-trunc-im-Set = map-hom-slice-trunc-im-Set
+ pr2 hom-slice-trunc-im-Set = triangle-hom-slice-trunc-im-Set
abstract
is-surjective-map-hom-slice-trunc-im-Set :
@@ -361,17 +362,15 @@ module _
unit-im-map-trunc-Set :
im f → im (map-trunc-Set f)
- unit-im-map-trunc-Set x =
- pair
- ( unit-trunc-Set (pr1 x))
- ( apply-universal-property-trunc-Prop (pr2 x)
- ( trunc-Prop (fiber (map-trunc-Set f) (unit-trunc-Set (pr1 x))))
- ( λ u →
- unit-trunc-Prop
- ( pair
- ( unit-trunc-Set (pr1 u))
- ( naturality-unit-trunc-Set f (pr1 u) ∙
- ap unit-trunc-Set (pr2 u)))))
+ pr1 (unit-im-map-trunc-Set x) = unit-trunc-Set (pr1 x)
+ pr2 (unit-im-map-trunc-Set x) =
+ apply-universal-property-trunc-Prop (pr2 x)
+ ( trunc-Prop (fiber (map-trunc-Set f) (unit-trunc-Set (pr1 x))))
+ ( λ u →
+ unit-trunc-Prop
+ ( ( unit-trunc-Set (pr1 u)) ,
+ ( naturality-unit-trunc-Set f (pr1 u) ∙
+ ap unit-trunc-Set (pr2 u))))
left-square-unit-im-map-trunc-Set :
( map-unit-im (map-trunc-Set f) ∘ unit-trunc-Set) ~
diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md
index ef44d6ca31..2d48de1898 100644
--- a/src/foundation/identity-types.lagda.md
+++ b/src/foundation/identity-types.lagda.md
@@ -97,14 +97,33 @@ module _
pr1 (equiv-concat p z) = concat p z
pr2 (equiv-concat p z) = is-equiv-concat p z
+ map-equiv-concat-equiv :
+ {x x' : A} → ((y : A) → (x ＝ y) ≃ (x' ＝ y)) → (x' ＝ x)
+ map-equiv-concat-equiv {x} e = map-equiv (e x) refl
+
+ is-section-equiv-concat :
+ {x x' : A} → map-equiv-concat-equiv {x} {x'} ∘ equiv-concat ~ id
+ is-section-equiv-concat refl = refl
+
+ abstract
+ is-retraction-equiv-concat :
+ {x x' : A} → equiv-concat ∘ map-equiv-concat-equiv {x} {x'} ~ id
+ is-retraction-equiv-concat e =
+ eq-htpy (λ y → eq-htpy-equiv (λ where refl → right-unit))
+
+ abstract
+ is-equiv-map-equiv-concat-equiv :
+ {x x' : A} → is-equiv (map-equiv-concat-equiv {x} {x'})
+ is-equiv-map-equiv-concat-equiv =
+ is-equiv-is-invertible
+ ( equiv-concat)
+ ( is-section-equiv-concat)
+ ( is-retraction-equiv-concat)
+
equiv-concat-equiv :
{x x' : A} → ((y : A) → (x ＝ y) ≃ (x' ＝ y)) ≃ (x' ＝ x)
- pr1 (equiv-concat-equiv {x}) e = map-equiv (e x) refl
- pr2 equiv-concat-equiv =
- is-equiv-is-invertible
- equiv-concat
- (λ { refl → refl})
- (λ e → eq-htpy (λ y → eq-htpy-equiv (λ { refl → right-unit})))
+ pr1 equiv-concat-equiv = map-equiv-concat-equiv
+ pr2 equiv-concat-equiv = is-equiv-map-equiv-concat-equiv
inv-concat' : (x : A) {y z : A} → y ＝ z → x ＝ z → x ＝ y
inv-concat' x q = concat' x (inv q)
diff --git a/src/foundation/isolated-elements.lagda.md b/src/foundation/isolated-elements.lagda.md
new file mode 100644
index 0000000000..db5c06554f
--- /dev/null
+++ b/src/foundation/isolated-elements.lagda.md
@@ -0,0 +1,393 @@
+# Isolated elements
+
+```agda
+module foundation.isolated-elements where
+```
+
+Imports
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.constant-maps
+open import foundation.decidable-embeddings
+open import foundation.decidable-equality
+open import foundation.decidable-maps
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-types
+open import foundation.maybe
+open import foundation.negation
+open import foundation.type-arithmetic-unit-type
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.contractible-types
+open import foundation-core.coproduct-types
+open import foundation-core.decidable-propositions
+open import foundation-core.empty-types
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.homotopies
+open import foundation-core.injective-maps
+open import foundation-core.propositions
+open import foundation-core.sets
+open import foundation-core.subtypes
+open import foundation-core.transport-along-identifications
+```
+
+Imports
-
-```agda
-open import foundation.action-on-identifications-functions
-open import foundation.constant-maps
-open import foundation.decidable-embeddings
-open import foundation.decidable-equality
-open import foundation.decidable-maps
-open import foundation.decidable-types
-open import foundation.dependent-pair-types
-open import foundation.embeddings
-open import foundation.fundamental-theorem-of-identity-types
-open import foundation.identity-types
-open import foundation.maybe
-open import foundation.negation
-open import foundation.type-arithmetic-unit-type
-open import foundation.unit-type
-open import foundation.universe-levels
-
-open import foundation-core.contractible-types
-open import foundation-core.coproduct-types
-open import foundation-core.decidable-propositions
-open import foundation-core.empty-types
-open import foundation-core.equivalences
-open import foundation-core.function-types
-open import foundation-core.functoriality-dependent-pair-types
-open import foundation-core.homotopies
-open import foundation-core.injective-maps
-open import foundation-core.propositions
-open import foundation-core.sets
-open import foundation-core.subtypes
-open import foundation-core.transport-along-identifications
-```
-
-Imports
@@ -13,7 +13,7 @@ open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.equivalences-maybe
open import foundation.identity-types
-open import foundation.isolated-points
+open import foundation.isolated-elements
open import foundation.maybe
open import foundation.propositional-truncations
open import foundation.universe-levels
@@ -26,89 +26,89 @@ open import univalent-combinatorics.finite-types
## Idea
-For any point `x` in a [finite type](univalent-combinatorics.finite-types.md)
+For any element `x` in a [finite type](univalent-combinatorics.finite-types.md)
`X` of [cardinality](set-theory.cardinalities.md) `n+1`, we can construct its
**complement**, which is a type of cardinality `n`.
## Definition
-### The complement of a point in a k-element type of arbitrary universe level
+### The complement of a element in a `k`-element type of arbitrary universe level
```agda
-isolated-point-UU-Fin :
+isolated-element-UU-Fin :
{l : Level} (k : ℕ) (X : UU-Fin l (succ-ℕ k)) →
type-UU-Fin (succ-ℕ k) X →
- isolated-point (type-UU-Fin (succ-ℕ k) X)
-pr1 (isolated-point-UU-Fin k X x) = x
-pr2 (isolated-point-UU-Fin k X x) =
+ isolated-element (type-UU-Fin (succ-ℕ k) X)
+pr1 (isolated-element-UU-Fin k X x) = x
+pr2 (isolated-element-UU-Fin k X x) =
has-decidable-equality-has-cardinality
( succ-ℕ k)
( has-cardinality-type-UU-Fin (succ-ℕ k) X)
( x)
-type-complement-point-UU-Fin :
+type-complement-element-UU-Fin :
{l1 : Level} (k : ℕ) →
Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k)) → UU l1
-type-complement-point-UU-Fin k (X , x) =
- complement-isolated-point
+type-complement-element-UU-Fin k (X , x) =
+ complement-isolated-element
( type-UU-Fin (succ-ℕ k) X)
- ( isolated-point-UU-Fin k X x)
+ ( isolated-element-UU-Fin k X x)
-equiv-maybe-structure-point-UU-Fin :
+equiv-maybe-structure-element-UU-Fin :
{l : Level} (k : ℕ) (X : UU-Fin l (succ-ℕ k)) →
(x : type-UU-Fin (succ-ℕ k) X) →
- Maybe (type-complement-point-UU-Fin k (pair X x)) ≃
+ Maybe (type-complement-element-UU-Fin k (pair X x)) ≃
type-UU-Fin (succ-ℕ k) X
-equiv-maybe-structure-point-UU-Fin k X x =
- equiv-maybe-structure-isolated-point
+equiv-maybe-structure-element-UU-Fin k X x =
+ equiv-maybe-structure-isolated-element
( type-UU-Fin (succ-ℕ k) X)
- ( isolated-point-UU-Fin k X x)
+ ( isolated-element-UU-Fin k X x)
-has-cardinality-type-complement-point-UU-Fin :
+has-cardinality-type-complement-element-UU-Fin :
{l1 : Level} (k : ℕ)
(X : Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k))) →
- has-cardinality k (type-complement-point-UU-Fin k X)
-has-cardinality-type-complement-point-UU-Fin k (pair (pair X H) x) =
+ has-cardinality k (type-complement-element-UU-Fin k X)
+has-cardinality-type-complement-element-UU-Fin k (pair (pair X H) x) =
apply-universal-property-trunc-Prop H
( has-cardinality-Prop k
- ( type-complement-point-UU-Fin k (pair (pair X H) x)))
+ ( type-complement-element-UU-Fin k (pair (pair X H) x)))
( λ e →
unit-trunc-Prop
( equiv-equiv-Maybe
( ( inv-equiv
- ( equiv-maybe-structure-point-UU-Fin k (pair X H) x)) ∘e
+ ( equiv-maybe-structure-element-UU-Fin k (pair X H) x)) ∘e
( e))))
-complement-point-UU-Fin :
+complement-element-UU-Fin :
{l1 : Level} (k : ℕ) →
Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k)) →
UU-Fin l1 k
-pr1 (complement-point-UU-Fin k T) =
- type-complement-point-UU-Fin k T
-pr2 (complement-point-UU-Fin k T) =
- has-cardinality-type-complement-point-UU-Fin k T
+pr1 (complement-element-UU-Fin k T) =
+ type-complement-element-UU-Fin k T
+pr2 (complement-element-UU-Fin k T) =
+ has-cardinality-type-complement-element-UU-Fin k T
-inclusion-complement-point-UU-Fin :
+inclusion-complement-element-UU-Fin :
{l1 : Level} (k : ℕ)
(X : Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k))) →
- type-complement-point-UU-Fin k X → type-UU-Fin (succ-ℕ k) (pr1 X)
-inclusion-complement-point-UU-Fin k X x = pr1 x
+ type-complement-element-UU-Fin k X → type-UU-Fin (succ-ℕ k) (pr1 X)
+inclusion-complement-element-UU-Fin k X x = pr1 x
```
### The action of equivalences on complements of isolated points
```agda
-equiv-complement-point-UU-Fin :
+equiv-complement-element-UU-Fin :
{l1 : Level} (k : ℕ)
(X Y : Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k))) →
(e : equiv-UU-Fin (succ-ℕ k) (pr1 X) (pr1 Y))
(p : Id (map-equiv e (pr2 X)) (pr2 Y)) →
equiv-UU-Fin k
- ( complement-point-UU-Fin k X)
- ( complement-point-UU-Fin k Y)
-equiv-complement-point-UU-Fin
+ ( complement-element-UU-Fin k X)
+ ( complement-element-UU-Fin k Y)
+equiv-complement-element-UU-Fin
k S T e p =
- equiv-complement-isolated-point e
+ equiv-complement-isolated-element e
( pair x (λ x' → has-decidable-equality-has-cardinality (succ-ℕ k) H x x'))
( pair y (λ y' → has-decidable-equality-has-cardinality (succ-ℕ k) K y y'))
( p)
@@ -121,7 +121,7 @@ equiv-complement-point-UU-Fin
## Properties
-### The map from a pointed `k+1`-element type to the complement of the point is an equivalence
+### The map from a pointed `k+1`-element type to the complement of the element is an equivalence
This remains to be shown.
[#744](https://github.com/UniMath/agda-unimath/issues/744)
diff --git a/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md b/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md
index 113a923e90..8739e219ca 100644
--- a/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md
+++ b/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md
@@ -45,63 +45,64 @@ open import univalent-combinatorics.standard-finite-types
### The elements of a decidable subtype of a type equipped with a counting can be counted
```agda
-count-decidable-subtype' :
- {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) →
- (k : ℕ) (e : Fin k ≃ X) → count (type-decidable-subtype P)
-count-decidable-subtype' P zero-ℕ e =
- count-is-empty
- ( is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl ∘ pr1)
-count-decidable-subtype' P (succ-ℕ k) e
- with is-decidable-decidable-subtype P (map-equiv e (inr star))
-... | inl p =
- count-equiv
- ( equiv-Σ (is-in-decidable-subtype P) e (λ x → id-equiv))
- ( count-equiv'
- ( right-distributive-Σ-coprod
- ( Fin k)
- ( unit)
- ( λ x → is-in-decidable-subtype P (map-equiv e x)))
- ( pair
- ( succ-ℕ
- ( number-of-elements-count
- ( count-decidable-subtype'
- ( λ x → P (map-equiv e (inl x)))
- ( k)
- ( id-equiv))))
- ( equiv-coprod
- ( equiv-count
- ( count-decidable-subtype'
- ( λ x → P (map-equiv e (inl x)))
- ( k)
- ( id-equiv)))
- ( equiv-is-contr
- ( is-contr-unit)
- ( is-contr-Σ
+abstract
+ count-decidable-subtype' :
+ {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) →
+ (k : ℕ) (e : Fin k ≃ X) → count (type-decidable-subtype P)
+ count-decidable-subtype' P zero-ℕ e =
+ count-is-empty
+ ( is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl ∘ pr1)
+ count-decidable-subtype' P (succ-ℕ k) e
+ with is-decidable-decidable-subtype P (map-equiv e (inr star))
+ ... | inl p =
+ count-equiv
+ ( equiv-Σ (is-in-decidable-subtype P) e (λ x → id-equiv))
+ ( count-equiv'
+ ( right-distributive-Σ-coprod
+ ( Fin k)
+ ( unit)
+ ( λ x → is-in-decidable-subtype P (map-equiv e x)))
+ ( pair
+ ( succ-ℕ
+ ( number-of-elements-count
+ ( count-decidable-subtype'
+ ( λ x → P (map-equiv e (inl x)))
+ ( k)
+ ( id-equiv))))
+ ( equiv-coprod
+ ( equiv-count
+ ( count-decidable-subtype'
+ ( λ x → P (map-equiv e (inl x)))
+ ( k)
+ ( id-equiv)))
+ ( equiv-is-contr
( is-contr-unit)
- ( star)
- ( is-proof-irrelevant-is-prop
- ( is-prop-is-in-decidable-subtype P
- ( map-equiv e (inr star)))
- ( p)))))))
-... | inr f =
- count-equiv
- ( equiv-Σ (is-in-decidable-subtype P) e (λ x → id-equiv))
- ( count-equiv'
- ( right-distributive-Σ-coprod
- ( Fin k)
- ( unit)
- ( λ x → is-in-decidable-subtype P (map-equiv e x)))
+ ( is-contr-Σ
+ ( is-contr-unit)
+ ( star)
+ ( is-proof-irrelevant-is-prop
+ ( is-prop-is-in-decidable-subtype P
+ ( map-equiv e (inr star)))
+ ( p)))))))
+ ... | inr f =
+ count-equiv
+ ( equiv-Σ (is-in-decidable-subtype P) e (λ x → id-equiv))
( count-equiv'
- ( right-unit-law-coprod-is-empty
- ( Σ ( Fin k)
- ( λ x → is-in-decidable-subtype P (map-equiv e (inl x))))
- ( Σ ( unit)
- ( λ x → is-in-decidable-subtype P (map-equiv e (inr x))))
- ( λ { (pair star p) → f p}))
- ( count-decidable-subtype'
- ( λ x → P (map-equiv e (inl x)))
- ( k)
- ( id-equiv))))
+ ( right-distributive-Σ-coprod
+ ( Fin k)
+ ( unit)
+ ( λ x → is-in-decidable-subtype P (map-equiv e x)))
+ ( count-equiv'
+ ( right-unit-law-coprod-is-empty
+ ( Σ ( Fin k)
+ ( λ x → is-in-decidable-subtype P (map-equiv e (inl x))))
+ ( Σ ( unit)
+ ( λ x → is-in-decidable-subtype P (map-equiv e (inr x))))
+ ( λ where (star , p) → f p))
+ ( count-decidable-subtype'
+ ( λ x → P (map-equiv e (inl x)))
+ ( k)
+ ( id-equiv))))
count-decidable-subtype :
{l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) →
diff --git a/src/univalent-combinatorics/cubes.lagda.md b/src/univalent-combinatorics/cubes.lagda.md
index 921803394c..0c9ea342e7 100644
--- a/src/univalent-combinatorics/cubes.lagda.md
+++ b/src/univalent-combinatorics/cubes.lagda.md
@@ -12,7 +12,7 @@ open import elementary-number-theory.natural-numbers
open import foundation.dependent-pair-types
open import foundation.universe-levels
-open import univalent-combinatorics.complements-isolated-points
+open import univalent-combinatorics.complements-isolated-elements
open import univalent-combinatorics.finite-types
```
@@ -106,9 +106,9 @@ face-cube :
(k : ℕ) (X : cube (succ-ℕ k)) (d : dim-cube (succ-ℕ k) X)
(a : axis-cube (succ-ℕ k) X d) → cube k
pr1 (face-cube k X d a) =
- complement-point-UU-Fin k (pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
+ complement-element-UU-Fin k (pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
pr2 (face-cube k X d a) d' =
axis-cube-UU-2 (succ-ℕ k) X
- ( inclusion-complement-point-UU-Fin k
+ ( inclusion-complement-element-UU-Fin k
( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')
```
diff --git a/src/univalent-combinatorics/cyclic-types.lagda.md b/src/univalent-combinatorics/cyclic-types.lagda.md
index 478cb328e5..a543df9eea 100644
--- a/src/univalent-combinatorics/cyclic-types.lagda.md
+++ b/src/univalent-combinatorics/cyclic-types.lagda.md
@@ -493,17 +493,19 @@ is-retraction-equiv-Eq-Cyclic-Type k e =
( ℤ-Mod-Cyclic-Type k)
( e)))
-is-equiv-Eq-equiv-Cyclic-Type :
- (k : ℕ) (X : Cyclic-Type lzero k) → is-equiv (Eq-equiv-Cyclic-Type k X)
-is-equiv-Eq-equiv-Cyclic-Type k X =
- apply-universal-property-trunc-Prop
- ( mere-eq-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) X)
- ( is-equiv-Prop (Eq-equiv-Cyclic-Type k X))
- ( λ { refl →
+abstract
+ is-equiv-Eq-equiv-Cyclic-Type :
+ (k : ℕ) (X : Cyclic-Type lzero k) → is-equiv (Eq-equiv-Cyclic-Type k X)
+ is-equiv-Eq-equiv-Cyclic-Type k X =
+ apply-universal-property-trunc-Prop
+ ( mere-eq-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) X)
+ ( is-equiv-Prop (Eq-equiv-Cyclic-Type k X))
+ ( λ where
+ refl →
is-equiv-is-invertible
( equiv-Eq-Cyclic-Type k)
( is-section-equiv-Eq-Cyclic-Type k)
- ( is-retraction-equiv-Eq-Cyclic-Type k)})
+ ( is-retraction-equiv-Eq-Cyclic-Type k))
equiv-compute-Ω-Cyclic-Type :
(k : ℕ) → type-Ω (pair (Cyclic-Type lzero k) (ℤ-Mod-Cyclic-Type k)) ≃ ℤ-Mod k
diff --git a/src/univalent-combinatorics/finitely-presented-types.lagda.md b/src/univalent-combinatorics/finitely-presented-types.lagda.md
index 10aa729402..f5963031c2 100644
--- a/src/univalent-combinatorics/finitely-presented-types.lagda.md
+++ b/src/univalent-combinatorics/finitely-presented-types.lagda.md
@@ -92,7 +92,7 @@ has-cardinality-components-has-presentation-of-cardinality :
has-cardinality-components-has-presentation-of-cardinality {l} k {A} H =
apply-universal-property-trunc-Prop H
( has-cardinality-components-Prop k A)
- ( λ { (pair f E) → unit-trunc-Prop (pair (unit-trunc-Set ∘ f) E)})
+ ( λ (f , E) → unit-trunc-Prop (unit-trunc-Set ∘ f , E))
```
### To be finitely presented is a property
diff --git a/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md b/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
index cea1c935a0..dee4973e2e 100644
--- a/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
+++ b/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
@@ -19,7 +19,7 @@ open import foundation.set-truncations
open import foundation.universe-levels
open import foundation.unordered-tuples
-open import univalent-combinatorics.complements-isolated-points
+open import univalent-combinatorics.complements-isolated-elements
open import univalent-combinatorics.decidable-subtypes
open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.finite-types
@@ -122,7 +122,7 @@ is-π-finite-Main-Class-Latin-Hypercube-of-Order k n m =
is-finite-Π
( is-finite-Π
( is-finite-has-cardinality n
- ( has-cardinality-type-complement-point-UU-Fin n
+ ( has-cardinality-type-complement-element-UU-Fin n
( pair (type-unordered-tuple-UU-Fin (succ-ℕ n) A) i)))
( λ j →
is-finite-type-UU-Fin m
diff --git a/src/univalent-combinatorics/pi-finite-types.lagda.md b/src/univalent-combinatorics/pi-finite-types.lagda.md
index b084ebfc98..e51a3e9f56 100644
--- a/src/univalent-combinatorics/pi-finite-types.lagda.md
+++ b/src/univalent-combinatorics/pi-finite-types.lagda.md
@@ -368,7 +368,7 @@ pr2 (Fin-π-Finite k n) = is-π-finite-Fin k n
```agda
is-π-finite-count :
{l : Level} (k : ℕ) {A : UU l} → count A → is-π-finite k A
-is-π-finite-count k (pair n e) =
+is-π-finite-count k (n , e) =
is-π-finite-equiv' k e (is-π-finite-Fin k n)
```
@@ -411,14 +411,14 @@ pr2 (is-π-finite-UU-Fin (succ-ℕ k) n) x y =
( equiv-equiv-eq-UU-Fin n x y)
( is-π-finite-is-finite k
( is-finite-≃
- ( is-finite-has-finite-cardinality (pair n (pr2 x)))
- ( is-finite-has-finite-cardinality (pair n (pr2 y)))))
+ ( is-finite-has-finite-cardinality (n , (pr2 x)))
+ ( is-finite-has-finite-cardinality (n , (pr2 y)))))
is-finite-has-finite-connected-components :
{l : Level} {A : UU l} →
is-set A → has-finite-connected-components A → is-finite A
is-finite-has-finite-connected-components H =
- is-finite-equiv' (equiv-unit-trunc-Set (pair _ H))
+ is-finite-equiv' (equiv-unit-trunc-Set (_ , H))
has-finite-connected-components-is-π-finite :
{l : Level} (k : ℕ) {A : UU l} →
@@ -449,7 +449,7 @@ is-finite-is-π-finite :
is-π-finite k A → is-finite A
is-finite-is-π-finite k H K =
is-finite-equiv'
- ( equiv-unit-trunc-Set (pair _ H))
+ ( equiv-unit-trunc-Set (_ , H))
( has-finite-connected-components-is-π-finite k K)
is-truncated-π-finite-is-π-finite :
@@ -466,7 +466,7 @@ is-π-finite-is-truncated-π-finite :
is-truncated-π-finite k A → is-π-finite k A
is-π-finite-is-truncated-π-finite zero-ℕ H =
is-finite-equiv
- ( equiv-unit-trunc-Set (pair _ (is-set-is-finite H)))
+ ( equiv-unit-trunc-Set (_ , (is-set-is-finite H)))
( H)
pr1 (is-π-finite-is-truncated-π-finite (succ-ℕ k) H) = pr1 H
pr2 (is-π-finite-is-truncated-π-finite (succ-ℕ k) H) x y =
@@ -504,7 +504,7 @@ is-locally-finite-Π-Fin {l1} (succ-ℕ k) {B} f =
is-locally-finite-Π-count :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} → count A →
((x : A) → is-locally-finite (B x)) → is-locally-finite ((x : A) → B x)
-is-locally-finite-Π-count {l1} {l2} {A} {B} (pair k e) g =
+is-locally-finite-Π-count {l1} {l2} {A} {B} (k , e) g =
is-locally-finite-equiv
( equiv-precomp-Π e B)
( is-locally-finite-Π-Fin k (λ x → g (map-equiv e x)))
@@ -553,9 +553,9 @@ is-locally-finite-Σ :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
is-locally-finite A → ((x : A) → is-locally-finite (B x)) →
is-locally-finite (Σ A B)
-is-locally-finite-Σ {B = B} H K (pair x y) (pair x' y') =
+is-locally-finite-Σ {B = B} H K (x , y) (x' , y') =
is-finite-equiv'
- ( equiv-pair-eq-Σ (pair x y) (pair x' y'))
+ ( equiv-pair-eq-Σ (x , y) (x' , y'))
( is-finite-Σ (H x x') (λ p → K x' (tr B p y) y'))
```
@@ -572,7 +572,6 @@ has-finite-connected-components-Σ-is-0-connected {A = A} {B} C H K =
( is-inhabited-is-0-connected C)
( is-π-finite-Prop zero-ℕ (Σ A B))
( α)
-
where
α : A → is-π-finite zero-ℕ (Σ A B)
α a =
@@ -588,51 +587,46 @@ has-finite-connected-components-Σ-is-0-connected {A = A} {B} C H K =
( type-trunc-Set (Σ A B))
( λ y → is-decidable-Prop (Id-Prop (trunc-Set (Σ A B)) x y))))
( β))
-
where
β : (x : Σ A B) (v : type-trunc-Set (Σ A B)) →
is-decidable (Id (unit-trunc-Set x) v)
- β (pair x y) =
+ β (x , y) =
apply-dependent-universal-property-trunc-Set'
( λ u →
set-Prop
( is-decidable-Prop
- ( Id-Prop (trunc-Set (Σ A B)) (unit-trunc-Set (pair x y)) u)))
+ ( Id-Prop (trunc-Set (Σ A B)) (unit-trunc-Set (x , y)) u)))
( γ)
-
where
γ : (v : Σ A B) →
- is-decidable (Id (unit-trunc-Set (pair x y)) (unit-trunc-Set v))
- γ (pair x' y') =
+ is-decidable (Id (unit-trunc-Set (x , y)) (unit-trunc-Set v))
+ γ (x' , y') =
is-decidable-equiv
( is-effective-unit-trunc-Set
( Σ A B)
- ( pair x y)
- ( pair x' y'))
+ ( x , y)
+ ( x' , y'))
( apply-universal-property-trunc-Prop
( mere-eq-is-0-connected C a x)
( is-decidable-Prop
- ( mere-eq-Prop (pair x y) (pair x' y')))
+ ( mere-eq-Prop (x , y) (x' , y')))
( δ))
-
where
- δ : Id a x → is-decidable (mere-eq (pair x y) (pair x' y'))
+ δ : Id a x → is-decidable (mere-eq (x , y) (x' , y'))
δ refl =
apply-universal-property-trunc-Prop
( mere-eq-is-0-connected C a x')
( is-decidable-Prop
- ( mere-eq-Prop (pair a y) (pair x' y')))
+ ( mere-eq-Prop (a , y) (x' , y')))
( ε)
-
where
- ε : Id a x' → is-decidable (mere-eq (pair x y) (pair x' y'))
+ ε : Id a x' → is-decidable (mere-eq (x , y) (x' , y'))
ε refl =
is-decidable-equiv e
( is-decidable-type-trunc-Prop-is-finite
( is-finite-Σ
( pr2 H a a)
( λ ω → is-finite-is-decidable-Prop (P ω) (d ω))))
-
where
ℙ : is-contr
( Σ ( type-hom-Set (trunc-Set (Id a a)) (Prop-Set _))
@@ -664,38 +658,37 @@ has-finite-connected-components-Σ-is-0-connected {A = A} {B} C H K =
( unit-trunc-Set y'))))
f : type-hom-Prop
( trunc-Prop (Σ (type-trunc-Set (Id a a)) (type-Prop ∘ P)))
- ( mere-eq-Prop {A = Σ A B} (pair a y) (pair a y'))
+ ( mere-eq-Prop {A = Σ A B} (a , y) (a , y'))
f t = apply-universal-property-trunc-Prop t
- ( mere-eq-Prop (pair a y) (pair a y'))
- λ { (pair u v) →
- apply-dependent-universal-property-trunc-Set'
- ( λ u' →
- hom-Set
- ( set-Prop (P u'))
- ( set-Prop
- ( mere-eq-Prop (pair a y) (pair a y'))))
- ( λ ω v' →
- apply-universal-property-trunc-Prop
- ( map-equiv (compute-P ω) v')
- ( mere-eq-Prop (pair a y) (pair a y'))
- ( λ p → unit-trunc-Prop (eq-pair-Σ ω p)))
- ( u)
- ( v)}
- e : mere-eq {A = Σ A B} (pair a y) (pair a y') ≃
+ ( mere-eq-Prop (a , y) (a , y'))
+ λ (u , v) →
+ apply-dependent-universal-property-trunc-Set'
+ ( λ u' →
+ hom-Set
+ ( set-Prop (P u'))
+ ( set-Prop
+ ( mere-eq-Prop (a , y) (a , y'))))
+ ( λ ω v' →
+ apply-universal-property-trunc-Prop
+ ( map-equiv (compute-P ω) v')
+ ( mere-eq-Prop (a , y) (a , y'))
+ ( λ p → unit-trunc-Prop (eq-pair-Σ ω p)))
+ ( u)
+ ( v)
+ e : mere-eq {A = Σ A B} (a , y) (a , y') ≃
type-trunc-Prop (Σ (type-trunc-Set (Id a a)) (type-Prop ∘ P))
e = equiv-iff
- ( mere-eq-Prop (pair a y) (pair a y'))
+ ( mere-eq-Prop (a , y) (a , y'))
( trunc-Prop (Σ (type-trunc-Set (Id a a)) (type-Prop ∘ P)))
( λ t →
apply-universal-property-trunc-Prop t
( trunc-Prop _)
- ( ( λ { (pair ω r) →
- unit-trunc-Prop
- ( pair
- ( unit-trunc-Set ω)
- ( map-inv-equiv
- ( compute-P ω)
- ( unit-trunc-Prop r)))}) ∘
+ ( ( λ ( ω , r) →
+ unit-trunc-Prop
+ ( ( unit-trunc-Set ω) ,
+ ( map-inv-equiv
+ ( compute-P ω)
+ ( unit-trunc-Prop r)))) ∘
( pair-eq-Σ)))
( f)
```
@@ -718,26 +711,27 @@ module _
triangle-is-coprod-codomain (inl x) = refl
triangle-is-coprod-codomain (inr x) = refl
- is-emb-map-is-coprod-codomain : is-emb map-is-coprod-codomain
- is-emb-map-is-coprod-codomain =
- is-emb-coprod
- ( is-emb-inclusion-subtype (λ b → trunc-Prop _))
- ( is-emb-inclusion-subtype (λ b → trunc-Prop _))
- ( λ { (pair b1 u) (pair b2 v) →
+ abstract
+ is-emb-map-is-coprod-codomain : is-emb map-is-coprod-codomain
+ is-emb-map-is-coprod-codomain =
+ is-emb-coprod
+ ( is-emb-inclusion-subtype (λ b → trunc-Prop _))
+ ( is-emb-inclusion-subtype (λ b → trunc-Prop _))
+ ( λ (b1 , u) (b2 , v) →
apply-universal-property-trunc-Prop u
( function-Prop _ empty-Prop)
- ( λ
- { (pair x refl) →
+ ( λ where
+ ( x , refl) →
apply-universal-property-trunc-Prop v
( function-Prop _ empty-Prop)
- ( λ
- { (pair y refl) r →
+ ( λ where
+ ( y , refl) r →
is-empty-eq-coprod-inl-inr x y
( is-injective-is-equiv
( is-equiv-map-equiv e)
( ( inv (H (inl x))) ∙
- ( ( ap unit-trunc-Set r) ∙
- ( H (inr y)))))})})})
+ ( ap unit-trunc-Set r) ∙
+ ( H (inr y)))))))
is-surjective-map-is-coprod-codomain : is-surjective map-is-coprod-codomain
is-surjective-map-is-coprod-codomain b =
@@ -747,8 +741,7 @@ module _
( trunc-Prop (fiber map-is-coprod-codomain b))
( λ p →
unit-trunc-Prop
- ( pair
- ( map-coprod (map-unit-im (f ∘ inl)) (map-unit-im (f ∘ inr)) a)
+ ( ( map-coprod (map-unit-im (f ∘ inl)) (map-unit-im (f ∘ inr)) a) ,
( triangle-is-coprod-codomain a ∙ inv p)))
where
a = map-inv-equiv e (unit-trunc-Set b)
@@ -764,137 +757,137 @@ is-0-connected-unit : is-0-connected unit
is-0-connected-unit =
is-contr-equiv' unit equiv-unit-trunc-unit-Set is-contr-unit
-is-contr-im :
- {l1 l2 : Level} {A : UU l1} (B : Set l2) {f : A → type-Set B}
- (a : A) (H : f ~ const A (type-Set B) (f a)) → is-contr (im f)
-pr1 (is-contr-im B {f} a H) = map-unit-im f a
-pr2 (is-contr-im B {f} a H) (pair x u) =
- apply-dependent-universal-property-trunc-Prop
- ( λ v → Id-Prop (im-Set B f) (map-unit-im f a) (pair x v))
- ( u)
- ( λ { (pair a' refl) →
- eq-Eq-im f (map-unit-im f a) (map-unit-im f a') (inv (H a'))})
-
-is-0-connected-im :
- {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
- is-0-connected A → is-0-connected (im f)
-is-0-connected-im {l1} {l2} {A} {B} f C =
- apply-universal-property-trunc-Prop
- ( is-inhabited-is-0-connected C)
- ( is-contr-Prop _)
- ( λ a →
- is-contr-equiv'
- ( im (map-trunc-Set f))
- ( equiv-trunc-im-Set f)
- ( is-contr-im
- ( trunc-Set B)
- ( unit-trunc-Set a)
- ( apply-dependent-universal-property-trunc-Set'
- ( λ x →
- set-Prop
- ( Id-Prop
- ( trunc-Set B)
- ( map-trunc-Set f x)
- ( map-trunc-Set f (unit-trunc-Set a))))
- ( λ a' →
- apply-universal-property-trunc-Prop
- ( mere-eq-is-0-connected C a' a)
- ( Id-Prop
- ( trunc-Set B)
- ( map-trunc-Set f (unit-trunc-Set a'))
- ( map-trunc-Set f (unit-trunc-Set a)))
- ( λ {refl → refl})))))
+abstract
+ is-contr-im :
+ {l1 l2 : Level} {A : UU l1} (B : Set l2) {f : A → type-Set B}
+ (a : A) (H : f ~ const A (type-Set B) (f a)) → is-contr (im f)
+ pr1 (is-contr-im B {f} a H) = map-unit-im f a
+ pr2 (is-contr-im B {f} a H) (x , u) =
+ apply-dependent-universal-property-trunc-Prop
+ ( λ v → Id-Prop (im-Set B f) (map-unit-im f a) (x , v))
+ ( u)
+ ( λ where
+ ( a' , refl) →
+ eq-Eq-im f (map-unit-im f a) (map-unit-im f a') (inv (H a')))
+
+abstract
+ is-0-connected-im :
+ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
+ is-0-connected A → is-0-connected (im f)
+ is-0-connected-im {l1} {l2} {A} {B} f C =
+ apply-universal-property-trunc-Prop
+ ( is-inhabited-is-0-connected C)
+ ( is-contr-Prop _)
+ ( λ a →
+ is-contr-equiv'
+ ( im (map-trunc-Set f))
+ ( equiv-trunc-im-Set f)
+ ( is-contr-im
+ ( trunc-Set B)
+ ( unit-trunc-Set a)
+ ( apply-dependent-universal-property-trunc-Set'
+ ( λ x →
+ set-Prop
+ ( Id-Prop
+ ( trunc-Set B)
+ ( map-trunc-Set f x)
+ ( map-trunc-Set f (unit-trunc-Set a))))
+ ( λ a' →
+ apply-universal-property-trunc-Prop
+ ( mere-eq-is-0-connected C a' a)
+ ( Id-Prop
+ ( trunc-Set B)
+ ( map-trunc-Set f (unit-trunc-Set a'))
+ ( map-trunc-Set f (unit-trunc-Set a)))
+ ( λ where refl → refl)))))
is-0-connected-im-unit :
{l1 : Level} {A : UU l1} (f : unit → A) → is-0-connected (im f)
is-0-connected-im-unit f =
is-0-connected-im f is-0-connected-unit
-has-finite-connected-components-Σ' :
- {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
- (k : ℕ) → (Fin k ≃ (type-trunc-Set A)) →
- ((x y : A) → has-finite-connected-components (Id x y)) →
- ((x : A) → has-finite-connected-components (B x)) →
- has-finite-connected-components (Σ A B)
-has-finite-connected-components-Σ' zero-ℕ e H K =
- is-π-finite-is-empty zero-ℕ
- ( is-empty-is-empty-trunc-Set (map-inv-equiv e) ∘ pr1)
-has-finite-connected-components-Σ' {l1} {l2} {A} {B} (succ-ℕ k) e H K =
- apply-universal-property-trunc-Prop
- ( has-presentation-of-cardinality-has-cardinality-components
- ( succ-ℕ k)
- ( unit-trunc-Prop e))
- ( has-finite-connected-components-Prop (Σ A B))
- ( α)
- where
- α : Σ (Fin (succ-ℕ k) → A) (λ f → is-equiv (unit-trunc-Set ∘ f)) →
- has-finite-connected-components (Σ A B)
- α (pair f Eηf) =
- is-finite-equiv
- ( equiv-trunc-Set g)
- ( is-finite-equiv'
- ( equiv-distributive-trunc-coprod-Set
- ( Σ (im (f ∘ inl)) (B ∘ pr1))
- ( Σ (im (f ∘ inr)) (B ∘ pr1)))
- ( is-finite-coprod
- ( has-finite-connected-components-Σ' k
- ( h)
- ( λ x y →
- is-finite-equiv'
- ( equiv-trunc-Set
- ( equiv-ap-emb
- ( pair pr1
- ( is-emb-inclusion-subtype
- ( λ u → trunc-Prop _)))))
- ( H (pr1 x) (pr1 y)))
- ( λ x → K (pr1 x)))
- ( has-finite-connected-components-Σ-is-0-connected
- ( is-0-connected-im (f ∘ inr) is-0-connected-unit)
- ( pair
- ( is-finite-is-contr
- ( is-0-connected-im (f ∘ inr) is-0-connected-unit))
- ( λ x y →
- is-π-finite-equiv zero-ℕ
- ( equiv-Eq-eq-im (f ∘ inr) x y)
- ( H (pr1 x) (pr1 y))))
- ( λ x → K (pr1 x)))))
+abstract
+ has-finite-connected-components-Σ' :
+ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+ (k : ℕ) → (Fin k ≃ (type-trunc-Set A)) →
+ ((x y : A) → has-finite-connected-components (Id x y)) →
+ ((x : A) → has-finite-connected-components (B x)) →
+ has-finite-connected-components (Σ A B)
+ has-finite-connected-components-Σ' zero-ℕ e H K =
+ is-π-finite-is-empty zero-ℕ
+ ( is-empty-is-empty-trunc-Set (map-inv-equiv e) ∘ pr1)
+ has-finite-connected-components-Σ' {l1} {l2} {A} {B} (succ-ℕ k) e H K =
+ apply-universal-property-trunc-Prop
+ ( has-presentation-of-cardinality-has-cardinality-components
+ ( succ-ℕ k)
+ ( unit-trunc-Prop e))
+ ( has-finite-connected-components-Prop (Σ A B))
+ ( α)
where
- g : ((Σ (im (f ∘ inl)) (B ∘ pr1)) + (Σ (im (f ∘ inr)) (B ∘ pr1))) ≃
- Σ A B
- g = ( equiv-Σ B
- ( is-coprod-codomain f
- ( pair (unit-trunc-Set ∘ f) Eηf)
- ( refl-htpy))
- ( λ { (inl x) → id-equiv ;
- (inr x) → id-equiv})) ∘e
- ( inv-equiv
- ( right-distributive-Σ-coprod
- ( im (f ∘ inl))
- ( im (f ∘ inr))
- ( ind-coprod (λ x → UU l2) (B ∘ pr1) (B ∘ pr1))))
- i : Fin k → type-trunc-Set (im (f ∘ inl))
- i = unit-trunc-Set ∘ map-unit-im (f ∘ inl)
- is-surjective-i : is-surjective i
- is-surjective-i =
- is-surjective-comp
- ( is-surjective-unit-trunc-Set (im (f ∘ inl)))
- ( is-surjective-map-unit-im (f ∘ inl))
- is-emb-i : is-emb i
- is-emb-i =
- is-emb-right-factor-htpy
- ( (unit-trunc-Set ∘ f) ∘ inl)
- ( inclusion-trunc-im-Set (f ∘ inl))
- ( i)
- ( ( inv-htpy (naturality-unit-trunc-Set (inclusion-im (f ∘ inl)))) ·r
- ( map-unit-im (f ∘ inl)))
- ( is-emb-inclusion-trunc-im-Set (f ∘ inl))
- ( is-emb-comp
- ( unit-trunc-Set ∘ f)
- ( inl)
- ( is-emb-is-equiv Eηf)
- ( is-emb-inl (Fin k) unit))
- h : Fin k ≃ type-trunc-Set (im (f ∘ inl))
- h = pair i (is-equiv-is-emb-is-surjective is-surjective-i is-emb-i)
+ α : Σ (Fin (succ-ℕ k) → A) (λ f → is-equiv (unit-trunc-Set ∘ f)) →
+ has-finite-connected-components (Σ A B)
+ α (f , Eηf) =
+ is-finite-equiv
+ ( equiv-trunc-Set g)
+ ( is-finite-equiv'
+ ( equiv-distributive-trunc-coprod-Set
+ ( Σ (im (f ∘ inl)) (B ∘ pr1))
+ ( Σ (im (f ∘ inr)) (B ∘ pr1)))
+ ( is-finite-coprod
+ ( has-finite-connected-components-Σ' k
+ ( h)
+ ( λ x y →
+ is-finite-equiv'
+ ( equiv-trunc-Set
+ ( equiv-ap-emb
+ ( pr1 , is-emb-inclusion-subtype ( λ u → trunc-Prop _))))
+ ( H (pr1 x) (pr1 y)))
+ ( λ x → K (pr1 x)))
+ ( has-finite-connected-components-Σ-is-0-connected
+ ( is-0-connected-im (f ∘ inr) is-0-connected-unit)
+ ( ( is-finite-is-contr
+ ( is-0-connected-im (f ∘ inr) is-0-connected-unit)) ,
+ ( λ x y →
+ is-π-finite-equiv zero-ℕ
+ ( equiv-Eq-eq-im (f ∘ inr) x y)
+ ( H (pr1 x) (pr1 y))))
+ ( λ x → K (pr1 x)))))
+ where
+ g : ((Σ (im (f ∘ inl)) (B ∘ pr1)) + (Σ (im (f ∘ inr)) (B ∘ pr1))) ≃
+ Σ A B
+ g = ( equiv-Σ B
+ ( is-coprod-codomain f
+ ( unit-trunc-Set ∘ f , Eηf)
+ ( refl-htpy))
+ ( λ { (inl x) → id-equiv ; (inr x) → id-equiv})) ∘e
+ ( inv-equiv
+ ( right-distributive-Σ-coprod
+ ( im (f ∘ inl))
+ ( im (f ∘ inr))
+ ( ind-coprod (λ x → UU l2) (B ∘ pr1) (B ∘ pr1))))
+ i : Fin k → type-trunc-Set (im (f ∘ inl))
+ i = unit-trunc-Set ∘ map-unit-im (f ∘ inl)
+ is-surjective-i : is-surjective i
+ is-surjective-i =
+ is-surjective-comp
+ ( is-surjective-unit-trunc-Set (im (f ∘ inl)))
+ ( is-surjective-map-unit-im (f ∘ inl))
+ is-emb-i : is-emb i
+ is-emb-i =
+ is-emb-right-factor-htpy
+ ( (unit-trunc-Set ∘ f) ∘ inl)
+ ( inclusion-trunc-im-Set (f ∘ inl))
+ ( i)
+ ( ( inv-htpy (naturality-unit-trunc-Set (inclusion-im (f ∘ inl)))) ·r
+ ( map-unit-im (f ∘ inl)))
+ ( is-emb-inclusion-trunc-im-Set (f ∘ inl))
+ ( is-emb-comp
+ ( unit-trunc-Set ∘ f)
+ ( inl)
+ ( is-emb-is-equiv Eηf)
+ ( is-emb-inl (Fin k) unit))
+ h : Fin k ≃ type-trunc-Set (im (f ∘ inl))
+ h = i , (is-equiv-is-emb-is-surjective is-surjective-i is-emb-i)
has-finite-connected-components-Σ :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} → is-π-finite 1 A →
@@ -904,25 +897,25 @@ has-finite-connected-components-Σ {l1} {l2} {A} {B} H K =
apply-universal-property-trunc-Prop
( pr1 H)
( has-finite-connected-components-Prop (Σ A B))
- ( λ { (pair k e) →
- has-finite-connected-components-Σ' k e (λ x y → pr2 H x y) K})
-
-is-π-finite-Σ :
- {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} →
- is-π-finite (succ-ℕ k) A → ((x : A) → is-π-finite k (B x)) →
- is-π-finite k (Σ A B)
-is-π-finite-Σ zero-ℕ {A} {B} H K = has-finite-connected-components-Σ H K
-pr1 (is-π-finite-Σ (succ-ℕ k) H K) =
- has-finite-connected-components-Σ
- ( is-π-finite-one-is-π-finite-succ-ℕ (succ-ℕ k) H)
- ( λ x →
- has-finite-connected-components-is-π-finite (succ-ℕ k) (K x))
-pr2 (is-π-finite-Σ (succ-ℕ k) H K) (pair x u) (pair y v) =
- is-π-finite-equiv k
- ( equiv-pair-eq-Σ (pair x u) (pair y v))
- ( is-π-finite-Σ k
- ( pr2 H x y)
- ( λ { refl → pr2 (K x) u v}))
+ ( λ (k , e) → has-finite-connected-components-Σ' k e (λ x y → pr2 H x y) K)
+
+abstract
+ is-π-finite-Σ :
+ {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} →
+ is-π-finite (succ-ℕ k) A → ((x : A) → is-π-finite k (B x)) →
+ is-π-finite k (Σ A B)
+ is-π-finite-Σ zero-ℕ {A} {B} H K = has-finite-connected-components-Σ H K
+ pr1 (is-π-finite-Σ (succ-ℕ k) H K) =
+ has-finite-connected-components-Σ
+ ( is-π-finite-one-is-π-finite-succ-ℕ (succ-ℕ k) H)
+ ( λ x →
+ has-finite-connected-components-is-π-finite (succ-ℕ k) (K x))
+ pr2 (is-π-finite-Σ (succ-ℕ k) H K) (x , u) (y , v) =
+ is-π-finite-equiv k
+ ( equiv-pair-eq-Σ (x , u) (y , v))
+ ( is-π-finite-Σ k
+ ( pr2 H x y)
+ ( λ where refl → pr2 (K x) u v))
π-Finite-Σ :
{l1 l2 : Level} (k : ℕ) (A : π-Finite l1 (succ-ℕ k))
diff --git a/src/univalent-combinatorics/symmetric-difference.lagda.md b/src/univalent-combinatorics/symmetric-difference.lagda.md
index 3625fab642..cda7db8697 100644
--- a/src/univalent-combinatorics/symmetric-difference.lagda.md
+++ b/src/univalent-combinatorics/symmetric-difference.lagda.md
@@ -35,7 +35,6 @@ module _
{l l1 l2 : Level} (X : UU l) (F : is-finite X)
(P : decidable-subtype l1 X)
(Q : decidable-subtype l2 X)
-
where
eq-symmetric-difference :
diff --git a/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md b/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md
index 2126d8134a..414fa68110 100644
--- a/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md
@@ -94,8 +94,7 @@ module _
is-retraction-map-inv-ev-zero-one-Fin-two-ℕ :
map-inv-ev-zero-one-Fin-two-ℕ ∘ ev-zero-one-Fin-two-ℕ ~ id
is-retraction-map-inv-ev-zero-one-Fin-two-ℕ f =
- eq-htpy
- ( λ { (inl (inr star)) → refl ; (inr star) → refl})
+ eq-htpy (λ { (inl (inr star)) → refl ; (inr star) → refl})
dependent-universal-property-Fin-two-ℕ :
is-equiv ev-zero-one-Fin-two-ℕ
diff --git a/src/universal-algebra/algebraic-theory-of-groups.lagda.md b/src/universal-algebra/algebraic-theory-of-groups.lagda.md
index ac491c3c8f..90bf61b51d 100644
--- a/src/universal-algebra/algebraic-theory-of-groups.lagda.md
+++ b/src/universal-algebra/algebraic-theory-of-groups.lagda.md
@@ -43,12 +43,10 @@ data group-ops : UU lzero where
unit-group-op mul-group-op inv-group-op : group-ops
group-signature : signature lzero
-group-signature =
- pair
- group-ops
- ( λ { unit-group-op → 0 ;
- mul-group-op → 2 ;
- inv-group-op → 1})
+pr1 group-signature = group-ops
+pr2 group-signature unit-group-op = 0
+pr2 group-signature mul-group-op = 2
+pr2 group-signature inv-group-op = 1
data group-laws : UU lzero where
associative-l-group-laws : group-laws
@@ -58,39 +56,31 @@ data group-laws : UU lzero where
idr-r-group-laws : group-laws
group-Theory : Theory group-signature lzero
-group-Theory =
- pair
- ( group-laws)
- ( λ { associative-l-group-laws →
- pair
- ( op mul-group-op
- ( ( op mul-group-op
- ( var 0 ∷ var 1 ∷ empty-vec)) ∷
- ( var 2) ∷ empty-vec))
- ( op mul-group-op
- ( var 0 ∷
- ( op mul-group-op (var 1 ∷ var 2 ∷ empty-vec)) ∷ empty-vec)) ;
- invl-l-group-laws →
- pair
- ( op mul-group-op
- ( op inv-group-op (var 0 ∷ empty-vec) ∷ var 0 ∷ empty-vec))
- (op unit-group-op empty-vec) ;
- invr-r-group-laws →
- pair
- ( op mul-group-op
- ( var 0 ∷ op inv-group-op (var 0 ∷ empty-vec) ∷ empty-vec))
- (op unit-group-op empty-vec) ;
- idl-l-group-laws →
- pair
- (op mul-group-op (op unit-group-op empty-vec ∷ var 0 ∷ empty-vec))
- (var 0) ;
- idr-r-group-laws →
- pair
- (op mul-group-op (var 0 ∷ op unit-group-op empty-vec ∷ empty-vec))
- (var 0)})
- where
- op = op-Term
- var = var-Term
+pr1 group-Theory = group-laws
+pr2 group-Theory =
+ λ where
+ associative-l-group-laws →
+ ( op mul-group-op
+ ( ( op mul-group-op (var 0 ∷ var 1 ∷ empty-vec)) ∷ var 2 ∷ empty-vec)) ,
+ ( op mul-group-op
+ ( var 0 ∷ (op mul-group-op (var 1 ∷ var 2 ∷ empty-vec)) ∷ empty-vec))
+ invl-l-group-laws →
+ ( op mul-group-op
+ ( op inv-group-op (var 0 ∷ empty-vec) ∷ var 0 ∷ empty-vec)) ,
+ ( op unit-group-op empty-vec)
+ invr-r-group-laws →
+ ( op mul-group-op
+ ( var 0 ∷ op inv-group-op (var 0 ∷ empty-vec) ∷ empty-vec)) ,
+ ( op unit-group-op empty-vec)
+ idl-l-group-laws →
+ ( op mul-group-op (op unit-group-op empty-vec ∷ var 0 ∷ empty-vec)) ,
+ ( var 0)
+ idr-r-group-laws →
+ ( op mul-group-op (var 0 ∷ op unit-group-op empty-vec ∷ empty-vec)) ,
+ ( var 0)
+ where
+ op = op-Term
+ var = var-Term
group-Algebra : (l : Level) → UU (lsuc l)
group-Algebra l = Algebra group-signature group-Theory l
@@ -105,29 +95,24 @@ group-Algebra-Group :
{l : Level} →
Algebra group-signature group-Theory l →
Group l
-group-Algebra-Group (((A , is-set-A) , models-A) , satisfies-A) =
- pair
- ( pair
- ( pair A is-set-A)
- ( pair
- ( λ x y →
- ( models-A mul-group-op (x ∷ y ∷ empty-vec)))
- ( λ x y z →
- ( satisfies-A associative-l-group-laws
- ( λ { zero-ℕ → x ;
- ( succ-ℕ zero-ℕ) → y ;
- ( succ-ℕ (succ-ℕ n)) → z})))))
- ( pair
- ( pair
- ( models-A unit-group-op empty-vec)
- ( pair
- ( λ x → satisfies-A idl-l-group-laws (λ _ → x))
- ( λ x → satisfies-A idr-r-group-laws (λ _ → x))))
- ( pair
- ( λ x → models-A inv-group-op (x ∷ empty-vec))
- ( pair
- ( λ x → satisfies-A invl-l-group-laws (λ _ → x))
- ( λ x → satisfies-A invr-r-group-laws (λ _ → x)))))
+pr1 (pr1 (group-Algebra-Group ((A-Set , models-A) , satisfies-A))) = A-Set
+pr1 (pr2 (pr1 (group-Algebra-Group ((A-Set , models-A) , satisfies-A)))) x y =
+ models-A mul-group-op (x ∷ y ∷ empty-vec)
+pr2 (pr2 (pr1 (group-Algebra-Group ((A-Set , models-A) , satisfies-A)))) x y z =
+ satisfies-A associative-l-group-laws
+ ( λ { 0 → x ; 1 → y ; (succ-ℕ (succ-ℕ n)) → z})
+pr1 (pr1 (pr2 (group-Algebra-Group ((A-Set , models-A) , satisfies-A)))) =
+ models-A unit-group-op empty-vec
+pr1 (pr2 (pr1 (pr2 (group-Algebra-Group (_ , satisfies-A))))) x =
+ satisfies-A idl-l-group-laws (λ _ → x)
+pr2 (pr2 (pr1 (pr2 (group-Algebra-Group (_ , satisfies-A))))) x =
+ satisfies-A idr-r-group-laws (λ _ → x)
+pr1 (pr2 (pr2 (group-Algebra-Group ((A-Set , models-A) , satisfies-A)))) x =
+ models-A inv-group-op (x ∷ empty-vec)
+pr1 (pr2 (pr2 (pr2 (group-Algebra-Group (_ , satisfies-A))))) x =
+ satisfies-A invl-l-group-laws (λ _ → x)
+pr2 (pr2 (pr2 (pr2 (group-Algebra-Group (_ , satisfies-A))))) x =
+ satisfies-A invr-r-group-laws (λ _ → x)
Group-group-Algebra :
{l : Level} →
@@ -137,42 +122,43 @@ Group-group-Algebra G =
pair
( pair
( ( set-Group G))
- ( λ { unit-group-op v → unit-Group G ;
- mul-group-op (x ∷ y ∷ empty-vec) → mul-Group G x y ;
- inv-group-op (x ∷ empty-vec) → inv-Group G x}))
- ( λ { associative-l-group-laws assign →
- associative-mul-Group G (assign 0) (assign 1) (assign 2) ;
- invl-l-group-laws assign →
- left-inverse-law-mul-Group G (assign 0) ;
- invr-r-group-laws assign →
- right-inverse-law-mul-Group G (assign 0) ;
- idl-l-group-laws assign →
- left-unit-law-mul-Group G (assign 0) ;
- idr-r-group-laws assign →
- right-unit-law-mul-Group G (assign 0)})
-
-equiv-group-Algebra-Group :
- {l : Level} →
- Algebra group-signature group-Theory l ≃
- Group l
-pr1 equiv-group-Algebra-Group = group-Algebra-Group
-pr1 (pr1 (pr2 equiv-group-Algebra-Group)) = Group-group-Algebra
-pr2 (pr1 (pr2 equiv-group-Algebra-Group)) G =
- eq-pair-Σ refl (eq-is-prop (is-prop-is-group (semigroup-Group G)))
-pr1 (pr2 (pr2 equiv-group-Algebra-Group)) = Group-group-Algebra
-pr2 (pr2 (pr2 equiv-group-Algebra-Group)) A =
- eq-pair-Σ
- ( eq-pair-Σ
- ( refl)
- ( eq-htpy
- ( λ { unit-group-op →
- ( eq-htpy λ {empty-vec → refl}) ;
- mul-group-op →
- ( eq-htpy λ { (x ∷ y ∷ empty-vec) → refl}) ;
- inv-group-op →
- ( eq-htpy λ { (x ∷ empty-vec) → refl})})))
- ( eq-is-prop
- ( is-prop-is-algebra
- ( group-signature) ( group-Theory)
- ( model-Algebra group-signature group-Theory A)))
+ ( λ where
+ unit-group-op v → unit-Group G
+ mul-group-op (x ∷ y ∷ empty-vec) → mul-Group G x y
+ inv-group-op (x ∷ empty-vec) → inv-Group G x))
+ ( λ where
+ associative-l-group-laws assign →
+ associative-mul-Group G (assign 0) (assign 1) (assign 2)
+ invl-l-group-laws assign →
+ left-inverse-law-mul-Group G (assign 0)
+ invr-r-group-laws assign →
+ right-inverse-law-mul-Group G (assign 0)
+ idl-l-group-laws assign →
+ left-unit-law-mul-Group G (assign 0)
+ idr-r-group-laws assign →
+ right-unit-law-mul-Group G (assign 0))
+
+abstract
+ equiv-group-Algebra-Group :
+ {l : Level} →
+ Algebra group-signature group-Theory l ≃
+ Group l
+ pr1 equiv-group-Algebra-Group = group-Algebra-Group
+ pr1 (pr1 (pr2 equiv-group-Algebra-Group)) = Group-group-Algebra
+ pr2 (pr1 (pr2 equiv-group-Algebra-Group)) G =
+ eq-pair-Σ refl (eq-is-prop (is-prop-is-group (semigroup-Group G)))
+ pr1 (pr2 (pr2 equiv-group-Algebra-Group)) = Group-group-Algebra
+ pr2 (pr2 (pr2 equiv-group-Algebra-Group)) A =
+ eq-pair-Σ
+ ( eq-pair-Σ
+ ( refl)
+ ( eq-htpy
+ ( λ where
+ unit-group-op → eq-htpy (λ where empty-vec → refl)
+ mul-group-op → eq-htpy (λ where (x ∷ y ∷ empty-vec) → refl)
+ inv-group-op → eq-htpy (λ where (x ∷ empty-vec) → refl))))
+ ( eq-is-prop
+ ( is-prop-is-algebra
+ ( group-signature) ( group-Theory)
+ ( model-Algebra group-signature group-Theory A)))
```