The binomial types

module univalent-combinatorics.binomial-types where
Imports
open import elementary-number-theory.binomial-coefficients
open import elementary-number-theory.natural-numbers

open import foundation.booleans
open import foundation.connected-components-universes
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.decidable-embeddings
open import foundation.decidable-propositions
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equivalences
open import foundation.equivalences-maybe
open import foundation.fibers-of-maps
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-function-types
open import foundation.functoriality-propositional-truncation
open import foundation.logical-equivalences
open import foundation.maybe
open import foundation.mere-equivalences
open import foundation.negation
open import foundation.propositional-extensionality
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-empty-type
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universal-property-empty-type
open import foundation.universal-property-maybe
open import foundation.universe-levels

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

The binomial types are a categorification of the binomial coefficients. The binomial type (A choose B) is the type of decidable embeddings from types merely equal to B into A.

Definitions

binomial-type-Level :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2)  UU (lsuc l  l1  l2)
binomial-type-Level l X Y =
  Σ (component-UU-Level l Y)  Z  type-component-UU-Level Z ↪d X)

type-binomial-type-Level :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} 
  binomial-type-Level l3 X Y  UU l3
type-binomial-type-Level Z = type-component-UU-Level (pr1 Z)

abstract
  mere-compute-binomial-type-Level :
    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
    (Z : binomial-type-Level l3 X Y) 
    mere-equiv Y (type-binomial-type-Level Z)
  mere-compute-binomial-type-Level Z = mere-equiv-component-UU-Level (pr1 Z)

decidable-emb-binomial-type-Level :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (Z : binomial-type-Level l3 X Y) 
  type-binomial-type-Level Z ↪d X
decidable-emb-binomial-type-Level Z = pr2 Z

map-decidable-emb-binomial-type-Level :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (Z : binomial-type-Level l3 X Y) 
  type-binomial-type-Level Z  X
map-decidable-emb-binomial-type-Level Z =
  map-decidable-emb (decidable-emb-binomial-type-Level Z)

abstract
  is-emb-map-emb-binomial-type-Level :
    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
    (Z : binomial-type-Level l3 X Y) 
    is-emb (map-decidable-emb-binomial-type-Level Z)
  is-emb-map-emb-binomial-type-Level Z =
    is-emb-map-decidable-emb (decidable-emb-binomial-type-Level Z)

The standard binomial types

We now define the standard binomial types.

binomial-type : {l1 l2 : Level} (X : UU l1) (Y : UU l2)  UU (lsuc (l1  l2))
binomial-type {l1} {l2} X Y = binomial-type-Level (l1  l2) X Y

type-binomial-type :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}  binomial-type X Y  UU (l1  l2)
type-binomial-type Z = type-component-UU-Level (pr1 Z)

abstract
  mere-compute-binomial-type :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (Z : binomial-type X Y) 
    mere-equiv Y (type-binomial-type Z)
  mere-compute-binomial-type Z = mere-equiv-component-UU-Level (pr1 Z)

decidable-emb-binomial-type :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (Z : binomial-type X Y) 
  type-binomial-type Z ↪d X
decidable-emb-binomial-type Z = pr2 Z

map-decidable-emb-binomial-type :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (Z : binomial-type X Y) 
  type-binomial-type Z  X
map-decidable-emb-binomial-type Z =
  map-decidable-emb (decidable-emb-binomial-type Z)

abstract
  is-emb-map-emb-binomial-type :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (Z : binomial-type X Y) 
    is-emb (map-decidable-emb-binomial-type Z)
  is-emb-map-emb-binomial-type Z =
    is-emb-map-decidable-emb (decidable-emb-binomial-type Z)

Proposition 17.5.6

binomial-type-Level' :
  (l : Level) {l1 l2 : Level} (A : UU l1) (B : UU l2)  UU (lsuc l  l1  l2)
binomial-type-Level' l A B =
  Σ ( A  Decidable-Prop l)
    ( λ P  mere-equiv B (Σ A (type-Decidable-Prop  P)))

compute-binomial-type-Level :
  (l : Level) {l1 l2 : Level} (A : UU l1) (B : UU l2) 
  binomial-type-Level (l1  l) A B  binomial-type-Level' (l1  l) A B
compute-binomial-type-Level l {l1} {l2} A B =
  ( ( ( equiv-Σ
        ( λ P  mere-equiv B (Σ A (type-Decidable-Prop  P)))
        ( equiv-Fib-Decidable-Prop l A)
        ( λ e 
          equiv-trunc-Prop
            ( equiv-postcomp-equiv
              ( inv-equiv (equiv-total-fib (pr1 (pr2 e)))) B))) ∘e
      ( inv-associative-Σ
        ( UU (l1  l))
        ( λ X  X ↪d A)
        ( λ X  mere-equiv B (pr1 X)))) ∘e
    ( equiv-tot  X  commutative-prod))) ∘e
  ( associative-Σ (UU (l1  l))  X  mere-equiv B X)  X  (pr1 X) ↪d A))

binomial-type' :
  {l1 l2 : Level} (A : UU l1) (B : UU l2)  UU (lsuc (l1  l2))
binomial-type' {l1} {l2} A B = binomial-type-Level' (l1  l2) A B

compute-binomial-type :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) 
  binomial-type A B  binomial-type' A B
compute-binomial-type {l1} {l2} A B =
  compute-binomial-type-Level (l1  l2) A B

Remark 17.5.7

Note that the universe level of small-binomial-type is lower.

small-binomial-type :
  {l1 l2 : Level} (A : UU l1) (B : UU l2)  UU (l1  l2)
small-binomial-type A B =
  Σ (A  bool)  f  mere-equiv B (fib f true))

compute-small-binomial-type :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) 
  binomial-type A B  small-binomial-type A B
compute-small-binomial-type A B =
  ( equiv-Σ
    ( λ f  mere-equiv B (fib f true))
    ( equiv-postcomp A equiv-bool-Decidable-Prop)
    ( λ P 
      equiv-trunc-Prop
        ( equiv-postcomp-equiv
          ( equiv-tot  a  compute-equiv-bool-Decidable-Prop (P a)))
          ( B)))) ∘e
  ( compute-binomial-type A B)
abstract
  binomial-type-over-empty :
    {l : Level} {X : UU l}  is-contr (binomial-type X empty)
  binomial-type-over-empty {l} {X} =
    is-contr-equiv
      ( raise-empty l ↪d X)
      ( left-unit-law-Σ-is-contr
        ( is-contr-component-UU-Level-empty l)
        ( Fin-UU-Fin l zero-ℕ))
      ( is-contr-equiv
        ( empty ↪d X)
        ( equiv-precomp-decidable-emb-equiv (compute-raise-empty l) X)
        ( is-contr-equiv
          ( is-decidable-emb ex-falso)
          ( left-unit-law-Σ-is-contr (universal-property-empty' X) ex-falso)
          ( is-proof-irrelevant-is-prop
            ( is-prop-is-decidable-emb ex-falso)
            ( is-decidable-emb-ex-falso))))

abstract
  binomial-type-empty-under :
    {l : Level} {X : UU l} 
    type-trunc-Prop X  is-empty (binomial-type empty X)
  binomial-type-empty-under H Y =
    apply-universal-property-trunc-Prop H empty-Prop
      ( λ x 
        apply-universal-property-trunc-Prop (pr2 (pr1 Y)) empty-Prop
          ( λ e  map-decidable-emb (pr2 Y) (map-equiv e x)))

abstract
  recursion-binomial-type' :
    {l1 l2 : Level} (A : UU l1) (B : UU l2) 
    binomial-type' (Maybe A) (Maybe B) 
    (binomial-type' A B + binomial-type' A (Maybe B))
  recursion-binomial-type' A B =
    ( ( ( left-distributive-Σ-coprod
          ( A  Decidable-Prop _)
          ( λ P  mere-equiv B (Σ A _))
          ( λ P  mere-equiv (Maybe B) (Σ A _))) ∘e
        ( equiv-tot
          ( λ P 
            ( ( equiv-coprod
                ( ( ( equiv-iff
                      ( mere-equiv-Prop (Maybe B) (Maybe (Σ A _)))
                      ( mere-equiv-Prop B (Σ A _))
                      ( map-trunc-Prop (equiv-equiv-Maybe))
                      ( map-trunc-Prop
                        ( λ e  equiv-coprod e id-equiv))) ∘e
                    ( equiv-trunc-Prop
                      ( equiv-postcomp-equiv
                        ( equiv-coprod
                          ( id-equiv)
                          ( equiv-is-contr is-contr-raise-unit is-contr-unit))
                        ( Maybe B)))) ∘e
                  ( left-unit-law-Σ-is-contr
                    ( is-contr-total-true-Prop)
                    ( pair (raise-unit-Prop _) raise-star)))
                ( ( equiv-trunc-Prop
                    ( equiv-postcomp-equiv
                      ( right-unit-law-coprod-is-empty
                        ( Σ A _)
                        ( raise-empty _)
                        ( is-empty-raise-empty))
                      ( Maybe B))) ∘e
                  ( left-unit-law-Σ-is-contr
                    ( is-contr-total-false-Prop)
                    ( pair (raise-empty-Prop _) map-inv-raise)))) ∘e
              ( right-distributive-Σ-coprod
                ( Σ (Prop _) type-Prop)
                ( Σ (Prop _) (¬  type-Prop))
                ( ind-coprod _
                  ( λ Q 
                    mere-equiv (Maybe B) ((Σ A _) + (type-Prop (pr1 Q))))
                  ( λ Q 
                    mere-equiv
                      ( Maybe B)
                      ( (Σ A _) + (type-Prop (pr1 Q))))))) ∘e
            ( equiv-Σ
              ( ind-coprod _
                ( λ Q 
                  mere-equiv
                    ( Maybe B)
                    ( ( Σ A  a  type-Decidable-Prop (P a))) +
                      ( type-Prop (pr1 Q))))
                ( λ Q 
                  mere-equiv
                    ( Maybe B)
                    ( ( Σ A  a  type-Decidable-Prop (P a))) +
                      ( type-Prop (pr1 Q)))))
              ( split-Decidable-Prop)
              ( ind-Σ
                ( λ Q 
                  ind-Σ
                    ( λ H 
                      ind-coprod _ ( λ q  id-equiv)  q  id-equiv)))))))) ∘e
      ( associative-Σ
        ( A  Decidable-Prop _)
        ( λ a  Decidable-Prop _)
        ( λ t 
          mere-equiv
            ( Maybe B)
            ( ( Σ A  a  type-Decidable-Prop (pr1 t a))) +
              ( type-Decidable-Prop (pr2 t)))))) ∘e
    ( equiv-Σ
      ( λ p 
        mere-equiv
          ( Maybe B)
          ( ( Σ A  a  type-Decidable-Prop (pr1 p a))) +
            ( type-Decidable-Prop (pr2 p))))
      ( equiv-universal-property-Maybe)
      ( λ u 
        equiv-trunc-Prop
          ( equiv-postcomp-equiv
            ( ( equiv-coprod
                ( id-equiv)
                ( left-unit-law-Σ  y  type-Decidable-Prop (u (inr y))))) ∘e
              ( right-distributive-Σ-coprod A unit
                ( λ x  type-Decidable-Prop (u x))))
            ( Maybe B))))

abstract
  binomial-type-Maybe :
    {l1 l2 : Level} (A : UU l1) (B : UU l2) 
    binomial-type (Maybe A) (Maybe B) 
    (binomial-type A B + binomial-type A (Maybe B))
  binomial-type-Maybe A B =
    ( inv-equiv
      ( equiv-coprod
        ( compute-binomial-type A B)
        ( compute-binomial-type A (Maybe B))) ∘e
      ( recursion-binomial-type' A B)) ∘e
    ( compute-binomial-type (Maybe A) (Maybe B))

Theorem 17.5.9

equiv-small-binomial-type :
  {l1 l2 l3 l4 : Level} {A : UU l1} {A' : UU l2} {B : UU l3} {B' : UU l4} 
  (A  A')  (B  B')  small-binomial-type A' B'  small-binomial-type A B
equiv-small-binomial-type {l1} {l2} {l3} {l4} {A} {A'} {B} {B'} e f =
  equiv-Σ
    ( λ P  mere-equiv B (fib P true))
    ( equiv-precomp e bool)
    ( λ P 
      equiv-trunc-Prop
        ( ( equiv-postcomp-equiv
            ( inv-equiv
              ( ( right-unit-law-Σ-is-contr
                  ( λ u 
                    is-contr-map-is-equiv (is-equiv-map-equiv e) (pr1 u))) ∘e
                ( equiv-compute-fib-comp P (map-equiv e) true))) B) ∘e
          ( equiv-precomp-equiv f (fib P true))))

equiv-binomial-type :
  {l1 l2 l3 l4 : Level} {A : UU l1} {A' : UU l2} {B : UU l3} {B' : UU l4} 
  (A  A')  (B  B')  binomial-type A' B'  binomial-type A B
equiv-binomial-type e f =
  ( ( inv-equiv (compute-small-binomial-type _ _)) ∘e
    ( equiv-small-binomial-type e f)) ∘e
  ( compute-small-binomial-type _ _)

binomial-type-Fin :
  (n m : )  binomial-type (Fin n) (Fin m)  Fin (binomial-coefficient-ℕ n m)
binomial-type-Fin zero-ℕ zero-ℕ =
  equiv-is-contr binomial-type-over-empty is-contr-Fin-one-ℕ
binomial-type-Fin zero-ℕ (succ-ℕ m) =
  equiv-is-empty (binomial-type-empty-under (unit-trunc-Prop (inr star))) id
binomial-type-Fin (succ-ℕ n) zero-ℕ =
  equiv-is-contr binomial-type-over-empty is-contr-Fin-one-ℕ
binomial-type-Fin (succ-ℕ n) (succ-ℕ m) =
  ( ( inv-equiv
      ( Fin-add-ℕ
        ( binomial-coefficient-ℕ n m)
        ( binomial-coefficient-ℕ n (succ-ℕ m)))) ∘e
    ( equiv-coprod
      ( binomial-type-Fin n m)
      ( binomial-type-Fin n (succ-ℕ m)))) ∘e
  ( binomial-type-Maybe (Fin n) (Fin m))

has-cardinality-binomial-type :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (n m : ) 
  has-cardinality n A  has-cardinality m B 
  has-cardinality (binomial-coefficient-ℕ n m) (binomial-type A B)
has-cardinality-binomial-type {A = A} {B} n m H K =
  apply-universal-property-trunc-Prop H
    ( has-cardinality-Prop (binomial-coefficient-ℕ n m) (binomial-type A B))
    ( λ e 
      apply-universal-property-trunc-Prop K
        ( has-cardinality-Prop (binomial-coefficient-ℕ n m) (binomial-type A B))
        ( λ f 
          unit-trunc-Prop
            ( inv-equiv
              ( binomial-type-Fin n m ∘e equiv-binomial-type e f))))

binomial-type-UU-Fin :
  {l1 l2 : Level} (n m : )  UU-Fin l1 n  UU-Fin l2 m 
  UU-Fin (lsuc l1  lsuc l2) (binomial-coefficient-ℕ n m)
pr1 (binomial-type-UU-Fin n m A B) =
  binomial-type (type-UU-Fin n A) (type-UU-Fin m B)
pr2 (binomial-type-UU-Fin n m A B) =
  has-cardinality-binomial-type n m
    ( has-cardinality-type-UU-Fin n A)
    ( has-cardinality-type-UU-Fin m B)

has-finite-cardinality-binomial-type :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  has-finite-cardinality A  has-finite-cardinality B 
  has-finite-cardinality (binomial-type A B)
pr1 (has-finite-cardinality-binomial-type (pair n H) (pair m K)) =
  binomial-coefficient-ℕ n m
pr2 (has-finite-cardinality-binomial-type (pair n H) (pair m K)) =
  has-cardinality-binomial-type n m H K

abstract
  is-finite-binomial-type :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} 
    is-finite A  is-finite B  is-finite (binomial-type A B)
  is-finite-binomial-type H K =
    is-finite-has-finite-cardinality
      ( has-finite-cardinality-binomial-type
        ( has-finite-cardinality-is-finite H)
        ( has-finite-cardinality-is-finite K))

binomial-type-𝔽 : {l1 l2 : Level}  𝔽 l1  𝔽 l2  𝔽 (l1  l2)
pr1 (binomial-type-𝔽 A B) = small-binomial-type (type-𝔽 A) (type-𝔽 B)
pr2 (binomial-type-𝔽 A B) =
  is-finite-equiv
    ( compute-small-binomial-type (type-𝔽 A) (type-𝔽 B))
    ( is-finite-binomial-type (is-finite-type-𝔽 A) (is-finite-type-𝔽 B))