π-finite types

module univalent-combinatorics.pi-finite-types where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.0-connected-types
open import foundation.cartesian-product-types
open import foundation.constant-maps
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.decidable-equality
open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equality-cartesian-product-types
open import foundation.equality-coproduct-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.fiber-inclusions
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-set-truncation
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.logical-equivalences
open import foundation.maybe
open import foundation.mere-equality
open import foundation.mere-equivalences
open import foundation.propositional-extensionality
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.set-truncations
open import foundation.sets
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.type-arithmetic-coproduct-types
open import foundation.unit-type
open import foundation.univalence
open import foundation.universal-property-coproduct-types
open import foundation.universal-property-empty-type
open import foundation.universal-property-unit-type
open import foundation.universe-levels

open import univalent-combinatorics.cartesian-product-types
open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.distributivity-of-set-truncation-over-finite-products
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.finitely-presented-types
open import univalent-combinatorics.function-types
open import univalent-combinatorics.image-of-maps
open import univalent-combinatorics.standard-finite-types

Idea

A type is π_n-finite if it has finitely many connected components and all of its homotopy groups up to level n at all base points are finite.

Definition

Locally finite types

is-locally-finite-Prop :
  {l : Level}  UU l  Prop l
is-locally-finite-Prop A =
  Π-Prop A  x  Π-Prop A  y  is-finite-Prop (Id x y)))

is-locally-finite : {l : Level}  UU l  UU l
is-locally-finite A = type-Prop (is-locally-finite-Prop A)

is-prop-is-locally-finite :
  {l : Level} (A : UU l)  is-prop (is-locally-finite A)
is-prop-is-locally-finite A = is-prop-type-Prop (is-locally-finite-Prop A)

Truncated π-finite types

is-truncated-π-finite-Prop : {l : Level} (k : )  UU l  Prop l
is-truncated-π-finite-Prop zero-ℕ X = is-finite-Prop X
is-truncated-π-finite-Prop (succ-ℕ k) X =
  prod-Prop
    ( is-finite-Prop (type-trunc-Set X))
    ( Π-Prop X
      ( λ x  Π-Prop X  y  is-truncated-π-finite-Prop k (Id x y))))

is-truncated-π-finite : {l : Level} (k : )  UU l  UU l
is-truncated-π-finite k A =
  type-Prop (is-truncated-π-finite-Prop k A)

Types with finitely many connected components

has-finite-connected-components-Prop : {l : Level}  UU l  Prop l
has-finite-connected-components-Prop A =
  is-finite-Prop (type-trunc-Set A)

has-finite-connected-components : {l : Level}  UU l  UU l
has-finite-connected-components A =
  type-Prop (has-finite-connected-components-Prop A)

number-of-connected-components :
  {l : Level} {X : UU l}  has-finite-connected-components X  
number-of-connected-components H = number-of-elements-is-finite H

mere-equiv-number-of-connected-components :
  {l : Level} {X : UU l} (H : has-finite-connected-components X) 
  mere-equiv
    ( Fin (number-of-connected-components H))
    ( type-trunc-Set X)
mere-equiv-number-of-connected-components H =
  mere-equiv-is-finite H

π-finite types

is-π-finite-Prop : {l : Level} (k : )  UU l  Prop l
is-π-finite-Prop zero-ℕ X = has-finite-connected-components-Prop X
is-π-finite-Prop (succ-ℕ k) X =
  prod-Prop ( is-π-finite-Prop zero-ℕ X)
            ( Π-Prop X
              ( λ x  Π-Prop X  y  is-π-finite-Prop k (Id x y))))

is-π-finite : {l : Level} (k : )  UU l  UU l
is-π-finite k X = type-Prop (is-π-finite-Prop k X)

is-prop-is-π-finite :
  {l : Level} (k : ) (X : UU l)  is-prop (is-π-finite k X)
is-prop-is-π-finite k X =
  is-prop-type-Prop (is-π-finite-Prop k X)

π-Finite : (l : Level) (k : )  UU (lsuc l)
π-Finite l k = Σ (UU l) (is-π-finite k)

type-π-Finite :
  {l : Level} (k : )  π-Finite l k  UU l
type-π-Finite k = pr1

is-π-finite-type-π-Finite :
  {l : Level} (k : ) (A : π-Finite l k) 
  is-π-finite k (type-π-Finite {l} k A)
is-π-finite-type-π-Finite k = pr2

Properties

Locally finite types are closed under equivalences

is-locally-finite-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B) 
  is-locally-finite B  is-locally-finite A
is-locally-finite-equiv e f x y =
  is-finite-equiv' (equiv-ap e x y) (f (map-equiv e x) (map-equiv e y))

is-locally-finite-equiv' :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B) 
  is-locally-finite A  is-locally-finite B
is-locally-finite-equiv' e = is-locally-finite-equiv (inv-equiv e)

types with decidable equality are locally finite

is-locally-finite-has-decidable-equality :
  {l1 : Level} {A : UU l1}  has-decidable-equality A  is-locally-finite A
is-locally-finite-has-decidable-equality d x y = is-finite-eq d

Any proposition is locally finite

is-locally-finite-is-prop :
  {l1 : Level} {A : UU l1}  is-prop A  is-locally-finite A
is-locally-finite-is-prop H x y = is-finite-is-contr (H x y)

Any contractible type is locally finite

is-locally-finite-is-contr :
  {l1 : Level} {A : UU l1}  is-contr A  is-locally-finite A
is-locally-finite-is-contr H =
  is-locally-finite-is-prop (is-prop-is-contr H)

is-locally-finite-unit : is-locally-finite unit
is-locally-finite-unit = is-locally-finite-is-contr is-contr-unit

Any empty type is locally finite

is-locally-finite-is-empty :
  {l1 : Level} {A : UU l1}  is-empty A  is-locally-finite A
is-locally-finite-is-empty H = is-locally-finite-is-prop  x  ex-falso (H x))

is-locally-finite-empty : is-locally-finite empty
is-locally-finite-empty = is-locally-finite-is-empty id

π-finite types are closed under equivalences

is-π-finite-equiv :
  {l1 l2 : Level} (k : ) {A : UU l1} {B : UU l2} (e : A  B) 
  is-π-finite k B  is-π-finite k A
is-π-finite-equiv zero-ℕ e H =
  is-finite-equiv' (equiv-trunc-Set e) H
pr1 (is-π-finite-equiv (succ-ℕ k) e H) = is-π-finite-equiv zero-ℕ e (pr1 H)
pr2 (is-π-finite-equiv (succ-ℕ k) e H) a b =
  is-π-finite-equiv k
    ( equiv-ap e a b)
    ( pr2 H (map-equiv e a) (map-equiv e b))

is-π-finite-equiv' :
  {l1 l2 : Level} (k : ) {A : UU l1} {B : UU l2} (e : A  B) 
  is-π-finite k A  is-π-finite k B
is-π-finite-equiv' k e = is-π-finite-equiv k (inv-equiv e)

The empty type is π-finite

is-π-finite-empty : (k : )  is-π-finite k empty
is-π-finite-empty zero-ℕ =
  is-finite-equiv equiv-unit-trunc-empty-Set is-finite-empty
pr1 (is-π-finite-empty (succ-ℕ k)) = is-π-finite-empty zero-ℕ
pr2 (is-π-finite-empty (succ-ℕ k)) = ind-empty

empty-π-Finite : (k : )  π-Finite lzero k
pr1 (empty-π-Finite k) = empty
pr2 (empty-π-Finite k) = is-π-finite-empty k

Any empty type is π-finite

is-π-finite-is-empty :
  {l : Level} (k : ) {A : UU l}  is-empty A  is-π-finite k A
is-π-finite-is-empty zero-ℕ f =
  is-finite-is-empty (is-empty-trunc-Set f)
pr1 (is-π-finite-is-empty (succ-ℕ k) f) = is-π-finite-is-empty zero-ℕ f
pr2 (is-π-finite-is-empty (succ-ℕ k) f) a = ex-falso (f a)

Any contractible type is π-finite

is-π-finite-is-contr :
  {l : Level} (k : ) {A : UU l}  is-contr A  is-π-finite k A
is-π-finite-is-contr zero-ℕ H =
  is-finite-is-contr (is-contr-trunc-Set H)
pr1 (is-π-finite-is-contr (succ-ℕ k) H) = is-π-finite-is-contr zero-ℕ H
pr2 (is-π-finite-is-contr (succ-ℕ k) H) x y =
  is-π-finite-is-contr k ( is-prop-is-contr H x y)

The unit type is π-finite

is-π-finite-unit :
  (k : )  is-π-finite k unit
is-π-finite-unit k = is-π-finite-is-contr k is-contr-unit

unit-π-Finite : (k : )  π-Finite lzero k
pr1 (unit-π-Finite k) = unit
pr2 (unit-π-Finite k) = is-π-finite-unit k

Coproducts of π-finite types are π-finite

is-π-finite-coprod :
  {l1 l2 : Level} (k : ) {A : UU l1} {B : UU l2} 
  is-π-finite k A  is-π-finite k B 
  is-π-finite k (A + B)
is-π-finite-coprod zero-ℕ H K =
  is-finite-equiv'
    ( equiv-distributive-trunc-coprod-Set _ _)
    ( is-finite-coprod H K)
pr1 (is-π-finite-coprod (succ-ℕ k) H K) =
  is-π-finite-coprod zero-ℕ (pr1 H) (pr1 K)
pr2 (is-π-finite-coprod (succ-ℕ k) H K) (inl x) (inl y) =
  is-π-finite-equiv k
    ( compute-eq-coprod-inl-inl x y)
    ( pr2 H x y)
pr2 (is-π-finite-coprod (succ-ℕ k) H K) (inl x) (inr y) =
  is-π-finite-equiv k
    ( compute-eq-coprod-inl-inr x y)
    ( is-π-finite-empty k)
pr2 (is-π-finite-coprod (succ-ℕ k) H K) (inr x) (inl y) =
  is-π-finite-equiv k
    ( compute-eq-coprod-inr-inl x y)
    ( is-π-finite-empty k)
pr2 (is-π-finite-coprod (succ-ℕ k) H K) (inr x) (inr y) =
  is-π-finite-equiv k
    ( compute-eq-coprod-inr-inr x y)
    ( pr2 K x y)

coprod-π-Finite :
  {l1 l2 : Level} (k : ) 
  π-Finite l1 k  π-Finite l2 k  π-Finite (l1  l2) k
pr1 (coprod-π-Finite k A B) = (type-π-Finite k A + type-π-Finite k B)
pr2 (coprod-π-Finite k A B) =
  is-π-finite-coprod k
    ( is-π-finite-type-π-Finite k A)
    ( is-π-finite-type-π-Finite k B)

Maybe A of any π-finite type A is π-finite

Maybe-π-Finite :
  {l : Level} (k : )  π-Finite l k  π-Finite l k
Maybe-π-Finite k A =
  coprod-π-Finite k A (unit-π-Finite k)

is-π-finite-Maybe :
  {l : Level} (k : ) {A : UU l} 
  is-π-finite k A  is-π-finite k (Maybe A)
is-π-finite-Maybe k H =
  is-π-finite-coprod k H (is-π-finite-unit k)

Any stanadard finite type is π-finite

is-π-finite-Fin :
  (k n : )  is-π-finite k (Fin n)
is-π-finite-Fin k zero-ℕ =
  is-π-finite-empty k
is-π-finite-Fin k (succ-ℕ n) =
  is-π-finite-Maybe k (is-π-finite-Fin k n)

Fin-π-Finite : (k : ) (n : )  π-Finite lzero k
pr1 (Fin-π-Finite k n) = Fin n
pr2 (Fin-π-Finite k n) = is-π-finite-Fin k n

Any type equipped with a counting is π-finite

is-π-finite-count :
  {l : Level} (k : ) {A : UU l}  count A  is-π-finite k A
is-π-finite-count k (pair n e) =
  is-π-finite-equiv' k e (is-π-finite-Fin k n)

Any finite type is π-finite

is-π-finite-is-finite :
  {l : Level} (k : ) {A : UU l}  is-finite A  is-π-finite k A
is-π-finite-is-finite k {A} H =
  apply-universal-property-trunc-Prop H
    ( is-π-finite-Prop k A)
    ( is-π-finite-count k)

π-finite-𝔽 : {l : Level} (k : )  𝔽 l  π-Finite l k
pr1 (π-finite-𝔽 k A) = type-𝔽 A
pr2 (π-finite-𝔽 k A) = is-π-finite-is-finite k (is-finite-type-𝔽 A)

Any 0-connected type has finitely many connected components

has-finite-connected-components-is-0-connected :
  {l : Level} {A : UU l} 
  is-0-connected A  has-finite-connected-components A
has-finite-connected-components-is-0-connected C =
  is-finite-is-contr C

The type of all n-element types in UU l is π-finite

is-π-finite-UU-Fin :
  {l : Level} (k n : )  is-π-finite k (UU-Fin l n)
is-π-finite-UU-Fin zero-ℕ n =
  has-finite-connected-components-is-0-connected
    ( is-0-connected-UU-Fin n)
pr1 (is-π-finite-UU-Fin (succ-ℕ k) n) = is-π-finite-UU-Fin zero-ℕ n
pr2 (is-π-finite-UU-Fin (succ-ℕ k) n) x y =
  is-π-finite-equiv k
    ( 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-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))

has-finite-connected-components-is-π-finite :
  {l : Level} (k : ) {A : UU l} 
  is-π-finite k A  has-finite-connected-components A
has-finite-connected-components-is-π-finite zero-ℕ H = H
has-finite-connected-components-is-π-finite (succ-ℕ k) H = pr1 H

is-π-finite-is-π-finite-succ-ℕ :
  {l : Level} (k : ) {A : UU l} 
  is-π-finite (succ-ℕ k) A  is-π-finite k A
is-π-finite-is-π-finite-succ-ℕ zero-ℕ H =
  has-finite-connected-components-is-π-finite 1 H
pr1 (is-π-finite-is-π-finite-succ-ℕ (succ-ℕ k) H) =
  has-finite-connected-components-is-π-finite (succ-ℕ (succ-ℕ k)) H
pr2 (is-π-finite-is-π-finite-succ-ℕ (succ-ℕ k) H) x y =
  is-π-finite-is-π-finite-succ-ℕ k (pr2 H x y)

is-π-finite-one-is-π-finite-succ-ℕ :
  {l : Level} (k : ) {A : UU l} 
  is-π-finite (succ-ℕ k) A  is-π-finite 1 A
is-π-finite-one-is-π-finite-succ-ℕ zero-ℕ H = H
is-π-finite-one-is-π-finite-succ-ℕ (succ-ℕ k) H =
  is-π-finite-one-is-π-finite-succ-ℕ k
    ( is-π-finite-is-π-finite-succ-ℕ (succ-ℕ k) H)

is-finite-is-π-finite :
  {l : Level} (k : ) {A : UU l}  is-set A 
  is-π-finite k A  is-finite A
is-finite-is-π-finite k H K =
  is-finite-equiv'
    ( equiv-unit-trunc-Set (pair _ H))
    ( has-finite-connected-components-is-π-finite k K)

is-truncated-π-finite-is-π-finite :
  {l : Level} (k : ) {A : UU l}  is-trunc (truncation-level-ℕ k) A 
  is-π-finite k A  is-truncated-π-finite k A
is-truncated-π-finite-is-π-finite zero-ℕ H K =
  is-finite-is-π-finite zero-ℕ H K
pr1 (is-truncated-π-finite-is-π-finite (succ-ℕ k) H K) = pr1 K
pr2 (is-truncated-π-finite-is-π-finite (succ-ℕ k) H K) x y =
  is-truncated-π-finite-is-π-finite k (H x y) (pr2 K x y)

is-π-finite-is-truncated-π-finite :
  {l : Level} (k : ) {A : UU l} 
  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)))
    ( H)
pr1 (is-π-finite-is-truncated-π-finite (succ-ℕ k) H) = pr1 H
pr2 (is-π-finite-is-truncated-π-finite (succ-ℕ k) H) x y =
  is-π-finite-is-truncated-π-finite k (pr2 H x y)

Proposition 1.5

The dependent product of locally finite types

is-locally-finite-prod :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  is-locally-finite A  is-locally-finite B  is-locally-finite (A × B)
is-locally-finite-prod f g x y =
  is-finite-equiv
    ( equiv-eq-pair x y)
    ( is-finite-prod (f (pr1 x) (pr1 y)) (g (pr2 x) (pr2 y)))

is-locally-finite-Π-Fin :
  {l1 : Level} (k : ) {B : Fin k  UU l1} 
  ((x : Fin k)  is-locally-finite (B x)) 
  is-locally-finite ((x : Fin k)  B x)
is-locally-finite-Π-Fin {l1} zero-ℕ {B} f =
  is-locally-finite-is-contr (dependent-universal-property-empty' B)
is-locally-finite-Π-Fin {l1} (succ-ℕ k) {B} f =
  is-locally-finite-equiv
    ( equiv-dependent-universal-property-coprod B)
    ( is-locally-finite-prod
      ( is-locally-finite-Π-Fin k  x  f (inl x)))
      ( is-locally-finite-equiv
        ( equiv-dependent-universal-property-unit (B  inr))
        ( f (inr star))))

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-equiv
    ( equiv-precomp-Π e B)
    ( is-locally-finite-Π-Fin k  x  g (map-equiv e x)))

is-locally-finite-Π :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2}  is-finite A 
  ((x : A)  is-locally-finite (B x))  is-locally-finite ((x : A)  B x)
is-locally-finite-Π {l1} {l2} {A} {B} f g =
  apply-universal-property-trunc-Prop f
    ( is-locally-finite-Prop ((x : A)  B x))
    ( λ e  is-locally-finite-Π-count e g)

Finite products of π-finite types

is-π-finite-Π :
  {l1 l2 : Level} (k : ) {A : UU l1} {B : A  UU l2} 
  is-finite A  ((a : A)  is-π-finite k (B a)) 
  is-π-finite k ((a : A)  B a)
is-π-finite-Π zero-ℕ {A} {B} H K =
  is-finite-equiv'
    ( equiv-distributive-trunc-Π-is-finite-Set B H)
    ( is-finite-Π H K)
pr1 (is-π-finite-Π (succ-ℕ k) H K) = is-π-finite-Π zero-ℕ H  a  pr1 (K a))
pr2 (is-π-finite-Π (succ-ℕ k) H K) f g =
  is-π-finite-equiv k
    ( equiv-funext)
    ( is-π-finite-Π k H  a  pr2 (K a) (f a) (g a)))

π-Finite-Π :
  {l1 l2 : Level} (k : ) (A : 𝔽 l1) (B : type-𝔽 A  π-Finite l2 k) 
  π-Finite (l1  l2) k
pr1 (π-Finite-Π k A B) =
  (x : type-𝔽 A)  (type-π-Finite k (B x))
pr2 (π-Finite-Π k A B) =
  is-π-finite-Π k
    ( is-finite-type-𝔽 A)
    ( λ x  is-π-finite-type-π-Finite k (B x))

Proposition 1.6

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-finite-equiv'
    ( equiv-pair-eq-Σ (pair x y) (pair x' y'))
    ( is-finite-Σ (H x x')  p  K x' (tr B p y) y'))

Proposition 1.7

has-finite-connected-components-Σ-is-0-connected :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
  is-0-connected A  is-π-finite 1 A 
  ((x : A)  has-finite-connected-components (B x)) 
  has-finite-connected-components (Σ A B)
has-finite-connected-components-Σ-is-0-connected {A = A} {B} C H K =
  apply-universal-property-trunc-Prop
    ( is-inhabited-is-0-connected C)
    ( is-π-finite-Prop zero-ℕ (Σ A B))
    ( α)

  where
  α : A  is-π-finite zero-ℕ (Σ A B)
  α a =
    is-finite-codomain
      ( K a)
      ( is-surjective-map-trunc-Set
        ( fiber-inclusion B a)
        ( is-surjective-fiber-inclusion C a))
      ( apply-dependent-universal-property-trunc-Set'
        ( λ x 
          set-Prop
            ( Π-Prop
              ( 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) =
      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)))
        ( γ)

      where
      γ : (v : Σ A B) 
          is-decidable (Id (unit-trunc-Set (pair x y)) (unit-trunc-Set v))
      γ (pair x' y') =
        is-decidable-equiv
          ( is-effective-unit-trunc-Set
            ( Σ A B)
            ( pair x y)
            ( pair 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')))
              ( δ))

        where
        δ : Id a x  is-decidable (mere-eq (pair x y) (pair 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')))
            ( ε)

          where
          ε : Id a x'  is-decidable (mere-eq (pair x y) (pair 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 _))
                    ( λ h 
                      ( λ a₁  h (unit-trunc-Set a₁)) ~
                      ( λ ω₁  trunc-Prop (Id (tr B ω₁ y) y'))))
             = universal-property-trunc-Set
                ( Id a a)
                ( Prop-Set _)
                ( λ ω  trunc-Prop (Id (tr B ω y) y'))
            P : type-trunc-Set (Id a a)  Prop _
            P = pr1 (center )
            compute-P :
              ( ω : Id a a) 
              type-Prop (P (unit-trunc-Set ω)) 
              type-trunc-Prop (Id (tr B ω y) y')
            compute-P ω = equiv-eq (ap pr1 (pr2 (center ) ω))
            d : (t : type-trunc-Set (Id a a))  is-decidable (type-Prop (P t))
            d = apply-dependent-universal-property-trunc-Set'
                ( λ t  set-Prop (is-decidable-Prop (P t)))
                ( λ ω 
                  is-decidable-equiv'
                    ( inv-equiv (compute-P ω))
                    ( is-decidable-equiv'
                      ( is-effective-unit-trunc-Set (B a) (tr B ω y) y')
                      ( has-decidable-equality-is-finite
                        ( K a)
                        ( unit-trunc-Set (tr B ω y))
                        ( 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'))
            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') 
                type-trunc-Prop (Σ (type-trunc-Set (Id a a)) (type-Prop  P))
            e = equiv-iff
                  ( mere-eq-Prop (pair a y) (pair 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)))}) 
                        ( pair-eq-Σ)))
                  ( f)

Proposition 1.8

module _
  {l1 l2 l3 : Level} {A1 : UU l1} {A2 : UU l2} {B : UU l3}
  (f : A1 + A2  B) (e : (A1 + A2)  type-trunc-Set B)
  (H : (unit-trunc-Set  f) ~ map-equiv e)
  where

  map-is-coprod-codomain : (im (f  inl) + im (f  inr))  B
  map-is-coprod-codomain = ind-coprod  x  B) pr1 pr1

  triangle-is-coprod-codomain :
    ( ( map-is-coprod-codomain) 
      ( map-coprod (map-unit-im (f  inl)) (map-unit-im (f  inr)))) ~ f
  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) 
          apply-universal-property-trunc-Prop u
            ( function-Prop _ empty-Prop)
            ( λ
              { (pair x refl) 
                apply-universal-property-trunc-Prop v
                  ( function-Prop _ empty-Prop)
                  ( λ
                    { (pair 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)))))})})})

  is-surjective-map-is-coprod-codomain : is-surjective map-is-coprod-codomain
  is-surjective-map-is-coprod-codomain b =
    apply-universal-property-trunc-Prop
      ( apply-effectiveness-unit-trunc-Set
        ( inv (issec-map-inv-equiv e (unit-trunc-Set b))  inv (H a)))
      ( trunc-Prop (fib map-is-coprod-codomain b))
      ( λ p 
        unit-trunc-Prop
          ( pair
            ( 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)

  is-coprod-codomain : (im (f  inl) + im (f  inr))  B
  pr1 is-coprod-codomain = map-is-coprod-codomain
  pr2 is-coprod-codomain =
    is-equiv-is-emb-is-surjective
      is-surjective-map-is-coprod-codomain
      is-emb-map-is-coprod-codomain

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})))))

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)))))
    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)

has-finite-connected-components-Σ :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2}  is-π-finite 1 A 
  ((x : A)  has-finite-connected-components (B x)) 
  has-finite-connected-components (Σ A B)
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}))

π-Finite-Σ :
  {l1 l2 : Level} (k : ) (A : π-Finite l1 (succ-ℕ k))
  (B : (x : type-π-Finite (succ-ℕ k) A)  π-Finite l2 k) 
  π-Finite (l1  l2) k
pr1 (π-Finite-Σ k A B) =
  Σ (type-π-Finite (succ-ℕ k) A)  x  type-π-Finite k (B x))
pr2 (π-Finite-Σ k A B) =
  is-π-finite-Σ k
    ( is-π-finite-type-π-Finite (succ-ℕ k) A)
    ( λ x  is-π-finite-type-π-Finite k (B x))