Kőnig's theorem

src/finite-group-theory/transpositions.lagda.md

@@ -446,11 +446,11 @@ module _
       apply-universal-property-trunc-Prop (pr2 Y)
         ( coproduct-Prop
           ( Id-Prop
-            ( pair X (is-set-count eX))
+            ( set-type-count eX)
             ( pr1 two-elements-transposition)
             ( x))
           ( Id-Prop
-            ( pair X (is-set-count eX))
+            ( set-type-count eX)
             ( pr1 (pr2 two-elements-transposition))
             ( x))
           ( λ q r →

src/foundation-core/fibers-of-maps.lagda.md

@@ -63,6 +63,24 @@ module _
 
 ## Properties
 
+### Fibers of compositions
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (g : B → X) (h : A → B) {x : X}
+  where
+
+  inclusion-fiber-comp : (t : fiber g x) → fiber h (pr1 t) → fiber (g ∘ h) x
+  inclusion-fiber-comp (b , q) (a , p) = (a , ap g p ∙ q)
+
+  left-fiber-comp : fiber (g ∘ h) x → fiber g x
+  left-fiber-comp (a , r) = (h a , r)
+
+  right-fiber-comp : (q : fiber (g ∘ h) x) → fiber h (pr1 (left-fiber-comp q))
+  right-fiber-comp (a , r) = (a , refl)
+```
+
 ### Characterization of the identity types of the fibers of a map
 
 #### The case of `fiber`
@@ -376,15 +394,11 @@ module _
 
   map-compute-fiber-comp :
     fiber (g ∘ h) x → Σ (fiber g x) (λ t → fiber h (pr1 t))
-  pr1 (pr1 (map-compute-fiber-comp (a , p))) = h a
-  pr2 (pr1 (map-compute-fiber-comp (a , p))) = p
-  pr1 (pr2 (map-compute-fiber-comp (a , p))) = a
-  pr2 (pr2 (map-compute-fiber-comp (a , p))) = refl
+  map-compute-fiber-comp t = (left-fiber-comp g h t , right-fiber-comp g h t)
 
   map-inv-compute-fiber-comp :
     Σ (fiber g x) (λ t → fiber h (pr1 t)) → fiber (g ∘ h) x
-  pr1 (map-inv-compute-fiber-comp t) = pr1 (pr2 t)
-  pr2 (map-inv-compute-fiber-comp t) = ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t)
+  map-inv-compute-fiber-comp (t , s) = inclusion-fiber-comp g h t s
 
   is-section-map-inv-compute-fiber-comp :
     is-section map-compute-fiber-comp map-inv-compute-fiber-comp

src/foundation.lagda.md

@@ -308,6 +308,7 @@ open import foundation.maps-in-global-subuniverses public
 open import foundation.maps-in-subuniverses public
 open import foundation.maximum-truncation-levels public
 open import foundation.maybe public
+open import foundation.mere-decidable-embeddings public
 open import foundation.mere-embeddings public
 open import foundation.mere-equality public
 open import foundation.mere-equivalences public
@@ -338,6 +339,7 @@ open import foundation.negated-equality public
 open import foundation.negation public
 open import foundation.noncontractible-types public
 open import foundation.noninjective-maps public
+open import foundation.nonsurjective-maps public
 open import foundation.null-homotopic-maps public
 open import foundation.operations-span-diagrams public
 open import foundation.operations-spans public

src/foundation/0-connected-types.lagda.md

@@ -159,22 +159,24 @@ is-trunc-map-ev-is-connected k {A} {B} a H K =
 ### The dependent universal property of 0-connected types
 
 ```agda
-equiv-dependent-universal-property-is-0-connected :
-  {l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
-  ( {l : Level} (P : A → Prop l) →
-    ((x : A) → type-Prop (P x)) ≃ type-Prop (P a))
-equiv-dependent-universal-property-is-0-connected a H P =
-  ( equiv-universal-property-unit (type-Prop (P a))) ∘e
-  ( equiv-dependent-universal-property-surjection-is-surjective
-    ( point a)
-    ( is-surjective-point-is-0-connected a H)
-    ( P))
-
-apply-dependent-universal-property-is-0-connected :
-  {l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
-  {l : Level} (P : A → Prop l) → type-Prop (P a) → (x : A) → type-Prop (P x)
-apply-dependent-universal-property-is-0-connected a H P =
-  map-inv-equiv (equiv-dependent-universal-property-is-0-connected a H P)
+module _
+  {l1 : Level} {A : UU l1} (a : A) (H : is-0-connected A)
+  {l : Level} (P : A → Prop l)
+  where
+
+  equiv-dependent-universal-property-is-0-connected :
+    ((x : A) → type-Prop (P x)) ≃ type-Prop (P a)
+  equiv-dependent-universal-property-is-0-connected =
+    ( equiv-universal-property-unit (type-Prop (P a))) ∘e
+    ( equiv-dependent-universal-property-surjection-is-surjective
+      ( point a)
+      ( is-surjective-point-is-0-connected a H)
+      ( P))
+
+  apply-dependent-universal-property-is-0-connected :
+    type-Prop (P a) → (x : A) → type-Prop (P x)
+  apply-dependent-universal-property-is-0-connected =
+    map-inv-equiv equiv-dependent-universal-property-is-0-connected
 ```
 
 ### A type `A` is 0-connected if and only if every fiber inclusion `B a → Σ A B` is surjective

src/foundation/axiom-of-choice.lagda.md

@@ -102,7 +102,7 @@ is-set-projective-AC0 :
 is-set-projective-AC0 ac X A B f h =
   map-trunc-Prop
     ( ( map-Σ
-        ( λ g → ((map-surjection f) ∘ g) ＝ h)
+        ( λ g → map-surjection f ∘ g ＝ h)
         ( precomp h A)
         ( λ s H → htpy-postcomp X H h)) ∘
       ( section-is-split-surjective (map-surjection f)))

src/foundation/cantor-schroder-bernstein-escardo.lagda.md

@@ -43,7 +43,7 @@ Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for
 
 ```agda
 module _
-  {l1 l2 : Level} (lem : LEM (l1 ⊔ l2))
+  {l1 l2 : Level} (lem : level-LEM (l1 ⊔ l2))
   {A : UU l1} {B : UU l2}
   where abstract
 
@@ -68,7 +68,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (lem : LEM (l1 ⊔ l2))
+  {l1 l2 : Level} (lem : level-LEM (l1 ⊔ l2))
   (A : Set l1) (B : Set l2)
   where abstract
 

src/foundation/connected-maps.lagda.md

@@ -54,19 +54,19 @@ if its [fibers](foundation-core.fibers-of-maps.md) are
 ### Connected maps
 
 ```agda
-is-connected-map-Prop :
-  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} → (A → B) → Prop (l1 ⊔ l2)
-is-connected-map-Prop k {B = B} f =
-  Π-Prop B (λ b → is-connected-Prop k (fiber f b))
-
-is-connected-map :
-  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2)
-is-connected-map k f = type-Prop (is-connected-map-Prop k f)
-
-is-prop-is-connected-map :
-  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) →
-  is-prop (is-connected-map k f)
-is-prop-is-connected-map k f = is-prop-type-Prop (is-connected-map-Prop k f)
+module _
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-connected-map-Prop : Prop (l1 ⊔ l2)
+  is-connected-map-Prop =
+    Π-Prop B (λ b → is-connected-Prop k (fiber f b))
+
+  is-connected-map : UU (l1 ⊔ l2)
+  is-connected-map = type-Prop is-connected-map-Prop
+
+  is-prop-is-connected-map : is-prop is-connected-map
+  is-prop-is-connected-map = is-prop-type-Prop is-connected-map-Prop
 ```
 
 ### The type of connected maps between two types
@@ -325,6 +325,34 @@ is-connected-map-left-factor k {g = g} {h} H GH z =
     ( is-connected-equiv' (compute-fiber-comp g h z) (GH z))
 ```
 
+### Composition and cancellation in commuting triangles
+
+```agda
+module _
+  {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) (h : A → B) (K : f ~ g ∘ h)
+  where
+
+  abstract
+    is-connected-map-left-map-triangle :
+      is-connected-map k h →
+      is-connected-map k g →
+      is-connected-map k f
+    is-connected-map-left-map-triangle H G =
+      is-connected-map-htpy k K
+        ( is-connected-map-comp k G H)
+
+  abstract
+    is-connected-map-right-map-triangle :
+      is-connected-map k f →
+      is-connected-map k h →
+      is-connected-map k g
+    is-connected-map-right-map-triangle F H =
+      is-connected-map-left-factor k
+        ( H)
+        ( is-connected-map-htpy' k K F)
+```
+
 ### The total map induced by a family of maps is `k`-connected if and only if all maps in the family are `k`-connected
 
 ```agda
@@ -377,14 +405,26 @@ module _
     is-equiv (precomp-Π f (λ b → type-Truncated-Type (P b)))
 
 module _
-  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f : A → B}
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B}
+  (H : is-connected-map k f)
   where
 
-  dependent-universal-property-is-connected-map :
-    is-connected-map k f → dependent-universal-property-connected-map k f
-  dependent-universal-property-is-connected-map H P =
-    is-equiv-precomp-Π-fiber-condition
-      ( λ b → is-equiv-diagonal-exponential-is-connected (P b) (H b))
+  abstract
+    dependent-universal-property-is-connected-map :
+      dependent-universal-property-connected-map k f
+    dependent-universal-property-is-connected-map P =
+      is-equiv-precomp-Π-fiber-condition
+        ( λ b → is-equiv-diagonal-exponential-is-connected (P b) (H b))
+
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : connected-map k A B)
+  where
+
+  dup-connected-map :
+    dependent-universal-property-connected-map k (map-connected-map f)
+  dup-connected-map =
+    dependent-universal-property-is-connected-map
+      ( is-connected-map-connected-map f)
 
 module _
   {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : connected-map k A B)
@@ -397,11 +437,54 @@ module _
   pr1 (equiv-dependent-universal-property-is-connected-map P) =
     precomp-Π (map-connected-map f) (λ b → type-Truncated-Type (P b))
   pr2 (equiv-dependent-universal-property-is-connected-map P) =
-    dependent-universal-property-is-connected-map k
+    dependent-universal-property-is-connected-map
       ( is-connected-map-connected-map f)
       ( P)
 ```
 
+### The induction principle for connected maps
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B}
+  (H : is-connected-map k f)
+  where
+
+  ind-is-connected-map :
+    {l3 : Level} (P : B → Truncated-Type l3 k) →
+    ((a : A) → type-Truncated-Type (P (f a))) →
+    (b : B) → type-Truncated-Type (P b)
+  ind-is-connected-map P =
+    map-inv-is-equiv (dependent-universal-property-is-connected-map H P)
+
+  compute-ind-is-connected-map :
+    {l3 : Level} (P : B → Truncated-Type l3 k) →
+    (g : (a : A) → type-Truncated-Type (P (f a))) →
+    (x : A) → ind-is-connected-map P g (f x) ＝ g x
+  compute-ind-is-connected-map P f =
+    htpy-eq
+      ( is-section-map-inv-is-equiv
+        ( dependent-universal-property-is-connected-map H P)
+        ( f))
+
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : connected-map k A B)
+  where
+
+  ind-connected-map :
+    {l3 : Level} (P : B → Truncated-Type l3 k) →
+    ((a : A) → type-Truncated-Type (P (map-connected-map f a))) →
+    (b : B) → type-Truncated-Type (P b)
+  ind-connected-map = ind-is-connected-map (is-connected-map-connected-map f)
+
+  compute-ind-connected-map :
+    {l3 : Level} (P : B → Truncated-Type l3 k) →
+    (g : (a : A) → type-Truncated-Type (P (map-connected-map f a))) →
+    (x : A) → ind-connected-map P g (map-connected-map f x) ＝ g x
+  compute-ind-connected-map =
+    compute-ind-is-connected-map (is-connected-map-connected-map f)
+```
+
 ### A map that satisfies the dependent universal property for connected maps is a connected map
 
 **Proof:** Consider a map `f : A → B` such that the precomposition function
@@ -510,7 +593,7 @@ abstract
       ( precomp-Π f (λ b → type-Truncated-Type (P b)))
   is-trunc-map-precomp-Π-is-connected-map k neg-two-𝕋 H P =
     is-contr-map-is-equiv
-      ( dependent-universal-property-is-connected-map k H
+      ( dependent-universal-property-is-connected-map H
         ( λ b →
           pair
             ( type-Truncated-Type (P b))

src/foundation/decidable-embeddings.lagda.md

@@ -219,8 +219,8 @@ is-decidable-emb-id :
   {l : Level} {A : UU l} → is-decidable-emb (id {A = A})
 is-decidable-emb-id = (is-emb-id , is-decidable-map-id)
 
-decidable-emb-id : {l : Level} {A : UU l} → A ↪ᵈ A
-decidable-emb-id = (id , is-decidable-emb-id)
+id-decidable-emb : {l : Level} {A : UU l} → A ↪ᵈ A
+id-decidable-emb = (id , is-decidable-emb-id)
 
 is-decidable-prop-map-id :
   {l : Level} {A : UU l} → is-decidable-prop-map (id {A = A})

src/foundation/diaconescus-theorem.lagda.md

@@ -80,7 +80,7 @@ instance-theorem-Diaconescu P ac-P =
     ( ac-P is-surjective-map-surjection-bool-suspension)
 
 theorem-Diaconescu :
-  {l : Level} → level-AC0 l l → LEM l
+  {l : Level} → level-AC0 l l → level-LEM l
 theorem-Diaconescu ac P =
   instance-theorem-Diaconescu P
     ( ac (suspension-set-Prop P) (fiber map-surjection-bool-suspension))

src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md

@@ -95,7 +95,7 @@ is-epimorphism-is-truncation-equivalence-Truncated-Type :
   is-truncation-equivalence k f →
   is-epimorphism-Truncated-Type k f
 is-epimorphism-is-truncation-equivalence-Truncated-Type k f H X =
-  is-emb-is-equiv (is-equiv-precomp-is-truncation-equivalence k f H X)
+  is-emb-is-equiv (is-equiv-precomp-is-truncation-equivalence H X)
 ```
 
 ### A map is a `k`-epimorphism if and only if its `k`-truncation is a `k`-epimorphism
@@ -283,8 +283,7 @@ module _
     is-epimorphism-Truncated-Type k f →
     is-truncation-equivalence k (codiagonal-map f)
   is-truncation-equivalence-codiagonal-map-is-epimorphism-Truncated-Type e =
-    is-truncation-equivalence-is-equiv-precomp k
-      ( codiagonal-map f)
+    is-truncation-equivalence-is-equiv-precomp
       ( λ l X →
         is-equiv-right-factor
           ( ( horizontal-map-cocone f f) ∘
@@ -330,7 +329,7 @@ module _
       ( is-equiv-comp
         ( map-equiv (equiv-up-pushout f f (type-Truncated-Type X)))
         ( precomp (codiagonal-map f) (type-Truncated-Type X))
-        ( is-equiv-precomp-is-truncation-equivalence k (codiagonal-map f) e X)
+        (is-equiv-precomp-is-truncation-equivalence e X)
         ( is-equiv-map-equiv (equiv-up-pushout f f (type-Truncated-Type X))))
 
   is-epimorphism-is-truncation-equivalence-codiagonal-map-Truncated-Type :