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
Imports
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
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.
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 (pair k f) (pair l g) e = is-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
Recent changes
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).