# Double counting

```agda
module univalent-combinatorics.double-counting where
```

<details><summary>Imports</summary>

```agda
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
```

</details>

## Idea

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.

```agda
abstract
  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 (k , f) (l , g) e =
    is-equivalence-injective-Fin (inv-equiv g ∘e e ∘e f)

abstract
  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
```