# Finite discrete Σ-decompositions

Content created by Fredrik Bakke and Victor Blanchi.

Created on 2023-03-21.

module univalent-combinatorics.discrete-sigma-decompositions where

open import foundation.discrete-sigma-decompositions public

Imports
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import univalent-combinatorics.finite-types
open import univalent-combinatorics.sigma-decompositions


## Definitions

module _
{l1 : Level} (l2 : Level) (A : 𝔽 l1)
where

discrete-Σ-Decomposition-𝔽 :
Σ-Decomposition-𝔽 l1 l2 A
discrete-Σ-Decomposition-𝔽 =
map-Σ-Decomposition-𝔽-subtype-is-finite
( A)
( ( discrete-Σ-Decomposition l2 (type-𝔽 A)) ,
( is-finite-type-𝔽 A ,
λ x → is-finite-raise-unit))

module _
{l1 l2 l3 : Level} (A : 𝔽 l1)
(D : Σ-Decomposition-𝔽 l2 l3 A)
where

is-discrete-Prop-Σ-Decomposition-𝔽 :
Prop (l2 ⊔ l3)
is-discrete-Prop-Σ-Decomposition-𝔽 =
Π-Prop
( indexing-type-Σ-Decomposition-𝔽 A D)
( λ x → is-contr-Prop (cotype-Σ-Decomposition-𝔽 A D x))

is-discrete-Σ-Decomposition-𝔽 :
UU (l2 ⊔ l3)
is-discrete-Σ-Decomposition-𝔽 =
type-Prop is-discrete-Prop-Σ-Decomposition-𝔽

is-discrete-discrete-Σ-Decomposition-𝔽 :
{l1 l2 : Level} (A : 𝔽 l1) →
is-discrete-Σ-Decomposition-𝔽
( A)
( discrete-Σ-Decomposition-𝔽 l2 A)
is-discrete-discrete-Σ-Decomposition-𝔽 _ =
is-discrete-discrete-Σ-Decomposition

type-discrete-Σ-Decomposition-𝔽 :
{l1 l2 l3 : Level} (A : 𝔽 l1) → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3)
type-discrete-Σ-Decomposition-𝔽 {l1} {l2} {l3} A =
type-subtype (is-discrete-Prop-Σ-Decomposition-𝔽 {l1} {l2} {l3} A)


## Propositions

module _
{l1 l2 l3 l4 : Level} (A : 𝔽 l1)
(D : Σ-Decomposition-𝔽 l2 l3 A)
( is-discrete : is-discrete-Σ-Decomposition-𝔽 A D)
where

equiv-discrete-is-discrete-Σ-Decomposition-𝔽 :
equiv-Σ-Decomposition-𝔽
( A)
( D)
( discrete-Σ-Decomposition-𝔽
( l4)
( A))
equiv-discrete-is-discrete-Σ-Decomposition-𝔽 =
equiv-discrete-is-discrete-Σ-Decomposition
( Σ-Decomposition-Σ-Decomposition-𝔽 A D)
( is-discrete)

is-contr-type-discrete-Σ-Decomposition-𝔽 :
{l1 l2 : Level} (A : 𝔽 l1) →
is-contr (type-discrete-Σ-Decomposition-𝔽 {l1} {l1} {l2} A)
pr1 ( is-contr-type-discrete-Σ-Decomposition-𝔽 {l1} {l2} A) =
( discrete-Σ-Decomposition-𝔽 l2 A ,
is-discrete-discrete-Σ-Decomposition-𝔽 A)
pr2 ( is-contr-type-discrete-Σ-Decomposition-𝔽 {l1} {l2} A) =
( λ x →
eq-type-subtype
( is-discrete-Prop-Σ-Decomposition-𝔽 A)
( inv
( eq-equiv-Σ-Decomposition-𝔽
( A)
( pr1 x)
( discrete-Σ-Decomposition-𝔽 l2 A)
( equiv-discrete-is-discrete-Σ-Decomposition-𝔽 A (pr1 x) (pr2 x)))))