Double counting

Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.

Created on 2022-02-11.
Last modified on 2023-03-13.

module univalent-combinatorics.double-counting where
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.universe-levels

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


Given two countings of the same type, we obtain the same number of its elements. Likewise, given two countings of equivalent types, we obtain the same number of their elements.

  double-counting-equiv :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (count-A : count A)
    (count-B : count B) (e : A  B) 
    Id (number-of-elements-count count-A) (number-of-elements-count count-B)
  double-counting-equiv (pair k f) (pair l g) e =
    is-injective-Fin ((inv-equiv g ∘e e) ∘e f)

  double-counting :
    {l : Level} {A : UU l} (count-A count-A' : count A) 
    Id (number-of-elements-count count-A) (number-of-elements-count count-A')
  double-counting count-A count-A' =
    double-counting-equiv count-A count-A' id-equiv

Recent changes