Counting

Table of Contents

1 Counting

module Lib.Counting where

This file defines the notion of counting in HoTT following Rijke's introduction to homotopy type theory, §16, and shows basic counting properties.

1.1 Packages imports

The imported packages can be accessed via the following links: 

import Lib.FundamentalTheorem
import Lib.Hedberg
import Lib.SubTypes
import Lib.Data.Fin  
import Lib.Prop.Empty
import Lib.Prop.Equiv
import Lib.Prop.Fin
import Lib.Prop.Proposition

1.2 Lock

We lock has-inverse/is-equiv so that the file typechecks. 

lock has-inverse/is-equiv

1.3 Definition

A type A can be counted if there is some k : Nat such that A is equivalent to Fin k. 

count (A : U) : U =
  Σ Nat (λk. Equiv (Fin k) A)

k is also called the number of elements of A. 

number-of-elements (A : U) (c : count A) : Nat = c.1
count/Equiv (A : U) (c : count A) : Equiv (Fin (number-of-elements A c)) A = c.2

1.4 Properties

1.4.1 Canonical count

It follows from the definition that every standard finite type can be counted in a canonical way. 

count/fin-count (k : Nat) : count (Fin k) =
  (k, IdEquiv (Fin k))

1.4.2 Zero and one-counts

For instance, we can give the canonical version of counts for zero and one. 

count/zero-count : count (Fin zero) =
  count/fin-count zero

count/one-count : count (Fin one-Nat) =
  count/fin-count one-Nat

1.4.3 Closure under equivalence

Furthermore, types with counting are closed under equivalence. 

count/closed-equiv (A B : U) (e : Equiv A B) (c : count B) : count A =
  (number-of-elements B c,
   Equiv/trans (Fin (number-of-elements B c)) B A (count/Equiv B c) (Equiv/sym A B e))

count/closed-equiv' (A B : U) (e : Equiv A B) (c : count A) : count B =
  count/closed-equiv B A (Equiv/sym A B e) c

1.4.4 Empty means no elements

If (k, e) is a counting of a type A, then k = 0 iff A is Empty.

  • [←] f : is-empty A is an equivalence, thus Fin k is equivalent to Empty and a quick induction on k is enough to conclude.
count/empty-has-zero-count (A : U) (c : count A) (f : is-empty A) : Path Nat zero (number-of-elements A c) =
  let e : Equiv (Fin (number-of-elements A c)) Empty =
        Equiv/trans (Fin (number-of-elements A c)) A Empty (count/Equiv A c) (Empty/equiv A f) in
  ind-Nat (λk. (Equiv (Fin k) Empty) → Path Nat zero k)
          (λ_. refl Nat zero)
          (λn _ e'. ex-falso (Path Nat zero (suc n)) ((Equiv/map (Fin (suc n)) Empty e') (zero-Fin n)))
          (number-of-elements A c) e
  • [→] By sigma-induction on the counting, yielding (k, e) then by path induction as inv e : A \to Empty.
count/zero-is-empty (A : U) (c : count A) (p : Path Nat zero (number-of-elements A c)) : is-empty A =
   ind-Σ Nat (λk. Equiv (Fin k) A)
              (λz. (Path Nat zero z.1) → is-empty A)
              (λk e p'. J Nat zero (λk' _. Equiv (Fin k') A → is-empty A) (λe'. Equiv/inv-map Empty A e') k p' e)
              c p

1.4.5 Contractible iff one element

First, assume that A has one element, that is, there is an equivalence between A and Fin 1. As Fin 1 is contractible, A is also contractible. Conversely, as A and Fin 1 are both contractible, they are equivalent and thus all countings of A have one element. 

-- count/contractible-has-one-element (A : U) (c : count A) (cA : is-contr A) : Path Nat one-Nat (number-of-elements A c) =
--   ind-Σ A (λk. Equiv (Fin k) A)
--            (λp. Path Nat one-Nat p.1)
--            (ind-Nat (λk. Equiv (Fin k) A → Path Nat one-Nat k)
--                     (λe. ex-falso (Path Nat one-Nat zero) (Equiv/inv-map (Fin zero) A e (center A cA)))
--                     (λk _ e. ind-Nat (λk'. Equiv (Fin k') A → Path Nat one-Nat k')
--                                      (λ_. refl Nat one-Nat)
--                                      (λk' r e'. ex-falso (Path Nat one-Nat k') ?)) k e) c

count/one-element-is-contr (A : U) (c : count A) (p : Path Nat one-Nat (number-of-elements A c)) : is-contr A =
  J Nat one-Nat (λk' _. Equiv (Fin k') A → is-contr A)
                (λe'. is-contr/is-contr-equiv' (Fin one-Nat) A e' Fin/fin-one-is-contr)
                (number-of-elements A c) p (count/Equiv A c)

count/contr-count (A : U) (c : is-contr A) : count A =
  ( one-Nat,
    ( is-contr/Equiv
      ( Fin one-Nat) A
      ( Fin/fin-one-is-contr) c))

1.4.6 A proposition is countable iff it is decidable

First, if a type X is countable, then it is decidable as can be shown by a quick induction on the number of elements of X. 

count/countable-is-decidable (X : U) (c : count X) : is-decidable X =
  ind-Σ Nat (λk. Equiv (Fin k) X)
             (λ_. is-decidable X)
             (ind-Nat (λk'. Equiv (Fin k') X → is-decidable X)
                      (λe'. is-decidable/Equiv' Empty X e' is-decidable/Empty)
                      (λk' _ e'. inl ((Equiv/map (Fin (suc k')) X e') (inr star)))) c

Conversely, if X is a decidable proposition, then X is countable. Indeed, by case analysis, it yields either the zero-count or the one-count. 

count/is-decidable-is-countable (X : U) (p : is-prop X) : is-decidable X → count X = split
  inl x → (one-Nat, Equiv/trans (Fin one-Nat) Unit X (Equiv/Equiv-copr-empty-type Unit) (Equiv/sym X Unit (is-prop/is-subterminal X p x)))
  inr f → (zero, Equiv/sym X Empty (Empty/equiv X f))

1.4.7 A countable type has a decidable equality

Actually, a type A equipped with a counting has decidable equality as Fin k has decidable equality. 

count/has-decidable-eq (A : U) (c : count A) : has-decidable-equality A =
  has-decidable-equality/Equiv' (Fin (number-of-elements A c)) A (count/Equiv A c) (Fin/decidable-eq (number-of-elements A c))

1.4.8 A countable type is a set

Then, Hedberg's theorem allows us to conclude that if A has a counting, then A is a set. 

count/is-set (A : U) (c : count A) : is-set A =
  hedberg A (count/has-decidable-eq A c)

1.4.9 Characterization of countings for Unit

Unit has a one count. 

count/Unit : count Unit =
  (one-Nat, Equiv/Equiv-copr-empty-type Unit)

1.4.10 Characterization of countings for coproduct and dependent pair

If A and B come equipped with a counting, then Coprod A B also comes with a counting. Indeed, if A ≅ Fin k and B ≅ Fin ℓ, then Coprod A B ≅ Coprod (Fin k) (Fin ℓ) ≅ Fin (k + ℓ). 

count/closed-Coprod (A B : U) (cA : count A) (cB : count B) : count (Coprod A B) =
  let k : Nat = number-of-elements A cA
      l : Nat = number-of-elements B cB
  in
  (plus-Nat k l, (Equiv/trans (Fin (plus-Nat k l)) (Coprod (Fin k) (Fin l)) (Coprod A B)
                 (Fin/Equiv-add-copr k l) (Coprod/closed-Equiv (Fin k) A (Fin l) B (count/Equiv A cA) (count/Equiv B cB))))

If A comes equipped with a counting and B is a type family over A, then all B x come equipped with a counting iff Σ A B comes equipped with a counting. 

count/closed-Sg/sg (A : U) (B : A → U) (H : (x : A) → count (B x)) : (k : Nat) → (e : Equiv (Fin k) A) → count (Σ A B) = split
  zero → λe.
    count/closed-equiv
      ( Σ A B)
      ( Empty)
      ( Equiv/trans
        ( Σ A B)
        ( Σ Empty (λx. B (Equiv/map Empty A e x)))
        ( Empty)
        ( Equiv/sym (Σ Empty (λx. B (Equiv/map Empty A e x))) (Σ A B) (Sg/equiv-base Empty A B e))
        ( Equiv/Equiv-Sg-empty (λx. B (Equiv/map Empty A e x))))
      ( count/zero-count)
  suc k → λe.
    let f : Fin (suc k) → A = (Equiv/map (Fin (suc k)) A e) in
      count/closed-equiv
      ( Σ A B)
      ( Coprod (Σ (Fin k) (λx. B (f (inl x)))) (B (f (inr star))))
      ( Equiv/trans
        ( Σ A B)
        ( Σ (Fin (suc k)) (λx. B (f x)))
        ( Coprod (Σ (Fin k) (λx. B (f (inl x)))) (B (f (inr star))))
        ( Equiv/sym
          ( Σ (Fin (suc k)) (λx. B (f x)))
          ( Σ A B)
          ( Sg/equiv-base (Fin (suc k)) A B e)) -- Σ A B ~ Σ (Fin k+1) (B o e)
        ( Equiv/trans
          ( Σ (Fin (suc k)) (λx. B (f x)))
          ( Coprod (Σ (Fin k) (λx. B (f (inl x)))) (Σ Unit (λx. B (f (inr x)))))
          ( Coprod (Σ (Fin k) (λx. B (f (inl x)))) (B (f (inr star))))
          ( Equiv/Sg-distr-over-coprod (Fin k) Unit (λx. B (f x)))
          ( Coprod/closed-Equiv
            ( Σ (Fin k) (λx. B (f (inl x))))
            ( Σ (Fin k) (λx. B (f (inl x))))
            ( Σ Unit (λx. B (f (inr x))))
            ( B (f (inr star)))
            ( Equiv/refl (Σ (Fin k) (λx. B (f (inl x)))))
            ( Equiv/Sg-unit (λx. B (f (inr x))))))) -- Σ Unit (B o e o inr) ~ B(e(inr(star)))
    ( count/closed-Coprod
      ( Σ (Fin k) (λx. B (f (inl x))))
      ( B (f (inr star)))
      ( count/closed-Sg/sg
        ( Fin k)
        ( λx. B (f (inl x)))
        ( λx. H (f (inl x))) k
        ( Equiv/refl (Fin k)))
        ( H (f (inr star))))

count/closed-Σ (A : U) (B : A → U) (cA : count A) (H : (x : A) → count (B x)) : count (Σ A B) =
  count/closed-Sg/sg A B H (number-of-elements A cA) (count/Equiv A cA)

We can show the converse, that is: if A comes with a counting and Σ A B comes with a counting, then B x comes with a counting for all x. To do so, remember that (B x) is equiv to (Fib pr1 x). But (Fib pr1 x) is (Σ (Σ A B) (λu. x = pr1 u)). By assumption, Σ A B is countable. Moreover, A is countable by assumption thus it has a decidable equality: the equality is also countable. 

count/closed-fam (A : U) (B : A → U) (cA : count A) (cT : count (Σ A B)) (x : A) : count (B x) =
  count/closed-equiv' (Fib (Σ A B) A (λu. u.1) x) (B x) (Equiv/fib-space-Equiv A B x)
    (count/closed-Σ (Σ A B) (λy. Path A x y.1) cT
      (λy. count/is-decidable-is-countable
        (Path A x y.1)
        (count/is-set A cA x y.1)
        (count/has-decidable-eq A cA x y.1)))

We can also show that if Σ A B comes with a counting, as well as B x comes with a counting for all x, then A comes with a counting whenever B has a section f : (x : A) → B x. 

count/closed-base-sg-map (A : U) (B : A → U) (b : (x : A) → B x) (x : A) : Σ A B = (x, b x)

-- count/closed-base-sg-equiv (A : U) (B : A → U) (b : (x : A) → B x) : Equiv A (Σ (Σ A B) (Fib A (Σ A B) (count/closed-base-sg-map A B b))) =
--   equiv-total-fib/Equiv A (Σ A B) (count/closed-base-sg-map A B b)

-- count/closed-base-sg (A : U) (B : A → U) (b : (x : A) → B x) (cT : count (Σ A B)) (cF : (x : A) → count B x) : count A =
--   count/closed-equiv A
--     ( Σ (Σ A B) (Fib A (Σ A B) (count/closed-base-sg-map A B b)))
--     ( count/closed-Sg
--       ( Σ A B)
--       ( Fib A (Σ A B) (count/closed-base-sg-map A B b)) cT
--       ( λt. count/closed-equiv
--             ( Fib A (Σ A B) (count/closed-base-sg-map A B b))
--             ( Σ A (λx. Path A t.1 x))
--             ( Equiv/trans
--               ( Fib A (Σ A B) (count/closed-base-sg-map A B b))  
--               ( Σ A (λx. Σ (Path A t.1 x) (λp. Path (B x) (tr A t.1 x p B t.2) (b x))))
--               ( Σ A (λx. Path A t.1 x))
--               ( Equiv/Sg-fam A
--                 ( λx. Path (Σ A B) t (x, b x))
--                 ( λx. Σ (Path A t.1 x) (λp. Path (B x) (tr A t.1 x p B t.2) (b x)))
--                 ( PathSg/Equiv A B t (x, b x)))
--               ( Equiv/Sg-target ? ?                      
--                 ( λx. count/is-set (B x) (cF x))))))

Remark that if P is a decidable subtype of X, then P is countable whenever X is countable. 

count/closed-decidable-subtype (X : U) (P : X → U) (c : count X) (s : is-decidable-subtype X P) (x : X) : count (P x) =
  count/closed-fam X P c
    (count/closed-Σ X P c (λy. count/is-decidable-is-countable (P y) (s.1 y) (s.2 y))) x

And so we conclude by proving the converse direction of the first statement: if Coprod A B has a counting then both A and B come equipped with a counting. We start by showing the counting of A: 

count/is-left (A B : U) : Coprod A B → U = split
  inl _ → Unit
  inr _ → Empty

count/is-left-count (A B : U) : (c : Coprod A B) → count (count/is-left A B c) = split
  inl _ → count/Unit
  inr _ → count/zero-count

count/Equiv-is-left (A B : U) : Equiv (Σ (Coprod A B) (count/is-left A B)) A =
  Equiv/trans (Σ (Coprod A B) (count/is-left A B)) (Coprod (Σ A (λ_. Unit)) (Σ B (λ_. Empty))) A
    (Equiv/Sg-distr-over-coprod A B (count/is-left A B))
    (Equiv/trans (Coprod (Σ A (λ_. Unit)) (Σ B (λ_. Empty))) (Coprod (Σ A (λ_. Unit)) Empty) A
      (Coprod/closed-Equiv (Σ A (λ_. Unit)) (Σ A (λ_. Unit)) (Σ B (λ_. Empty)) Empty (Equiv/refl (Σ A (λ_. Unit))) (Equiv/Sg-empty B))
      (Equiv/trans (Coprod (Σ A (λ_. Unit)) Empty) (Σ A (λ_. Unit)) A
        (Equiv/Equiv-copr-type-empty (Σ A (λ_. Unit)))
        (Equiv/Sg-base-unit A)))

count/closed-Coprod-left (A B : U) (c : count (Coprod A B)) : count A =
  count/closed-equiv' (Σ (Coprod A B) (count/is-left A B)) A (count/Equiv-is-left A B)
    (count/closed-Σ (Coprod A B) (count/is-left A B) c (count/is-left-count A B))

And then, we show the counting of B: 

count/is-right (A B : U) : Coprod A B → U = split
  inl _ → Empty
  inr _ → Unit

count/is-right-count (A B : U) : (c : Coprod A B) → count (count/is-right A B c) = split
  inl _ → count/zero-count
  inr _ → count/Unit  

count/Equiv-is-right (A B : U) : Equiv (Σ (Coprod A B) (count/is-right A B)) B =
  Equiv/trans (Σ (Coprod A B) (count/is-right A B)) (Coprod (A * Empty) (B * Unit)) B
    (Equiv/Sg-distr-over-coprod A B (count/is-right A B))
    (Equiv/trans (Coprod (A * Empty) (B * Unit)) (Coprod Empty (B * Unit)) B
      (Coprod/closed-Equiv (A * Empty) Empty (B * Unit) (B * Unit) (Equiv/Sg-empty A) (Equiv/refl (B * Unit)))
      (Equiv/trans (Coprod Empty (B * Unit)) (B * Unit) B
        (Equiv/Equiv-copr-empty-type (B * Unit))
        (Equiv/Sg-base-unit B)))

count/closed-Coprod-right (A B : U) (c : count (Coprod A B)) : count B =
  count/closed-equiv' (Σ (Coprod A B) (count/is-right A B)) B (count/Equiv-is-right A B)
    (count/closed-Σ (Coprod A B) (count/is-right A B) c (count/is-right-count A B))

1.4.11 Characterization of countings for product

After the characterization of dependent pair, the counting for products are a special case. 

count/closed-Prod (A B : U) (cA : count A) (cB : count B) : count (A * B) =
  count/closed-Σ A (λ_. B) cA (λ_. cB)

We can do the left and right countings the same way that we did for coproducts. 

-- count/closed-Prod-left (A B : U) (c : count (A * B)) (b : B) : count A =
--   count/closed-fam

1.5 Double counting

In this section, we show that if Fin k is equivalent to Fin l, then k = l. This is a consequence of a more general result : if Coprod X Unit and Coprod Y Unit are equivalent, then X is equivalent to Y.

1.5.1 Star value

If we have an x such that e(inl(x)) = inr star, then e(inr star) is not inr star. 

Maybe (X : U) : U = Coprod X Unit

star-value/inj-empty (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) (z : Maybe Y) (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) z)
                     (q : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) z) : Empty =
  let f : Maybe X → Maybe Y = Equiv/map (Maybe X) (Maybe Y) e in
  Coprod/Eq/eq-map X Unit (inl x) (inr star)
    (is-bi-inv/inv-map (Path (Maybe X) (inl x) (inr star)) (Path (Maybe Y) (f (inl x)) (f (inr star)))
      (ap (Maybe X) (Maybe Y) f (inl x) (inr star))
      (is-bi-inv/is-inj (Maybe X) (Maybe Y) f (Equiv/is-bi-inv (Maybe X) (Maybe Y) e) (inl x) (inr star))
      (comp (Maybe Y) (f (inl x)) z p (f (inr star)) (inv (Maybe Y) (f (inr star)) z q)))

star-value/inj (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star))
  : (y : Maybe Y) → Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) y → Y = split
  inl y → λ_. y
  inr s → λq. ind-Unit (λz. Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) (inr z) → Y)
                       (λr. ex-falso Y (star-value/inj-empty X Y e x (inr star) p r)) s q

star-value (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star)) : Y =
  star-value/inj X Y e x p (Equiv/map (Maybe X) (Maybe Y) e (inr star)) (refl (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)))

That is, we have a homotopy α : inl(star-value e x p) = e(inr star). 

star-value-htpy/inj-empty (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star))
                               : (s : Unit) → Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) (inr s) → Empty = split
  star → (star-value/inj-empty X Y e x (inr star) p)

star-value-htpy/inj' (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star))
                     (s : Unit) (q : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) (inr s))
                        : Path (Maybe Y) (inl (star-value X Y e x p)) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) = 
  ex-falso (Path (Maybe Y) (inl (star-value X Y e x p)) (Equiv/map (Maybe X) (Maybe Y) e (inr star)))
           (star-value-htpy/inj-empty X Y e x p s q)

star-value-htpy/inj (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star))
                         : (y : Maybe Y) → Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) y
                                         → Path (Maybe Y) (inl (star-value X Y e x p)) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) = split
  inl y → λq. J (Maybe Y) (inl y) (λz _. (r : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) z) → Path (Maybe Y) (inl (star-value/inj X Y e x p z r)) z)
                (λr. Coprod/Eq/map Y Unit (inl (star-value/inj X Y e x p (inl y) r)) (inl y) (refl Y y))
                (Equiv/map (Maybe X) (Maybe Y) e (inr star)) (inv (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) (inl y) q) (refl (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)))
  inr s → star-value-htpy/inj' X Y e x p s

star-value-htpy (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star))
                     : Path (Maybe Y) (inl (star-value X Y e x p)) (Equiv/map (Maybe X) (Maybe Y) e (inr star)) =
  star-value-htpy/inj X Y e x p (Equiv/map (Maybe X) (Maybe Y) e (inr star)) (refl (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inr star)))

1.5.2 Equivalence map

Next, given e : X + 1 ≅ Y + 1, we construct f : X → Y such that f will be inversible. First, we define an auxiliary function. 

double-counting/map-star (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X)
                              : (s : Unit) → Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr s) → Y = split
  star → star-value X Y e x

double-counting/map' (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X)
                          : (u : Maybe Y) → Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) u → Y = split
  inl y → λ_. y
  inr s → double-counting/map-star X Y e x s

Then, we can define f using e(inl x) and refl. 

double-counting/map (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) : Y =
  double-counting/map' X Y e x (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (refl (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)))

Then, we have two identifications for f(x) : whenever e(inl x) = inl y, f(x) = y ; 

double-counting/map-inl-id (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X) (y : Y)
                           (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inl y)) : Path Y (double-counting/map X Y e x) y =
  tr (Maybe Y) (inl y) (Equiv/map (Maybe X) (Maybe Y) e (inl x))
    (inv (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inl y) p)
    (λu. (q : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) u) → Path Y (double-counting/map' X Y e x u q) y)
    (λ_. refl Y y) (refl (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)))

and whenever e(inl x) = inr star, f(x) = star-value e x p. The proof is quite complicated as the path intervenes in star-value, thus we use some tricks to recover it properly. 

Unit/inr (A : U) : (s : Unit) → Path (Maybe A) (inr s) (inr star) = split
  star → refl (Coprod A Unit) (inr star)

Unit/copr (A : U) (x : Maybe A) (p : Path (Maybe A) x (inr star)) : (u : Maybe A) → Path (Maybe A) x u → Path (Maybe A) u (inr star) = split
  inl a → λq. ex-falso (Path (Maybe A) (inl a) (inr star)) (Coprod/Eq/eq-map A Unit (inr star) (inl a) (comp (Maybe A) (inr star) x (inv (Maybe A) x (inr star) p) (inl a) q))
  inr s → λ_. Unit/inr A s

double-counting/map-inr-id/refl (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X)
                                (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star))
                                   : Path Y (double-counting/map' X Y e x (inr star) (comp (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star) p (inr star) (refl (Maybe Y) (inr star))))
                                            (star-value X Y e x p) =
  let f : Maybe X → Maybe Y = Equiv/map (Maybe X) (Maybe Y) e in
  ap (Path (Maybe Y) (f (inl x)) (inr star)) Y (λq. (double-counting/map' X Y e x (inr star) q))
     (comp (Maybe Y) (f (inl x)) (inr star) p (inr star) (refl (Maybe Y) (inr star))) p (comp/ident-r (Maybe Y) (f (inl x)) (inr star) p)

double-counting/map-inr-id' (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X)
                            (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star))
                               : Path Y (double-counting/map' X Y e x (Equiv/map (Maybe X) (Maybe Y) e (inl x))
                                          (comp (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star) p
                                                         (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inv (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star) p)))
                                        (star-value X Y e x p) =
  let f : Maybe X → Maybe Y = Equiv/map (Maybe X) (Maybe Y) e in
  tr (Maybe Y) (inr star) (f (inl x))
    (inv (Maybe Y) (f (inl x)) (inr star) p)
    (λu. (q : Path (Maybe Y) (f (inl x)) (inr star)) → 
         (r : Path (Maybe Y) (inr star) u) → Path Y (double-counting/map' X Y e x u (comp (Maybe Y) (f (inl x)) (inr star) q u r)) (star-value X Y e x q))
    (λq r. J (Maybe Y) (inr star) (λu q'. Path Y (double-counting/map' X Y e x u (comp (Maybe Y) (f (inl x)) (inr star) q u q')) (star-value X Y e x q))
             (double-counting/map-inr-id/refl X Y e x q) (inr star) r) p (inv (Maybe Y) (f (inl x)) (inr star) p)

double-counting/map-inr-id (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X)
                           (p : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl x)) (inr star))
                              : Path Y (double-counting/map X Y e x) (star-value X Y e x p) =
  let f : Maybe X → Maybe Y = Equiv/map (Maybe X) (Maybe Y) e in
  comp Y (double-counting/map X Y e x)
         (double-counting/map' X Y e x (f (inl x)) (comp (Maybe Y) (f (inl x)) (inr star) p (f (inl x)) (inv (Maybe Y) (f (inl x)) (inr star) p)))
         (ap (Path (Maybe Y) (f (inl x)) (f (inl x))) Y (λq. double-counting/map' X Y e x (f (inl x)) q) (refl (Maybe Y) (f (inl x)))
             (comp (Maybe Y) (f (inl x)) (inr star) p (f (inl x)) (inv (Maybe Y) (f (inl x)) (inr star) p))
             (comp/inv-r' (Maybe Y) (f (inl x)) (inr star) p))
         (star-value X Y e x p) (double-counting/map-inr-id' X Y e x p)

1.5.3 Inverse map

We build the inverse map using the inverse equivalence so that the other properties follow. 

double-counting/inv-map (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) : X =
  double-counting/map Y X (Equiv/sym (Maybe X) (Maybe Y) e) y

It comes equipped with the same identifications: g(inl y) = x ; 

double-counting/inv-map-inl-id (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (x : X)
                               (p : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inl x)) : Path X (double-counting/inv-map X Y e y) x =
  double-counting/map-inl-id Y X (Equiv/sym (Maybe X) (Maybe Y) e) y x p

and g(inl y) = star-value whenever e-1(inl y) is star. 

double-counting/inv-map-inr-id (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y)
                               (p : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star))
                                  : Path X (double-counting/inv-map X Y e y) (star-value Y X (Equiv/sym (Maybe X) (Maybe Y) e) y p) =
  double-counting/map-inr-id Y X (Equiv/sym (Maybe X) (Maybe Y) e) y p

1.5.4 Decidability

To show that g is a right and left homotopy of f, we use the fact that the type (e(inl x) = star) is decidable. Hence, we have to show that this type is indeed decidable. 

double-counting/has-decidable-eq (X : U) : (x : Maybe X) → is-decidable (Path (Maybe X) x (inr star)) = split
  inl x → inr (λp. Coprod/Eq/eq-map X Unit (inl x) (inr star) p)
  inr s → inl (Coprod/Eq/map X Unit (inr s) (inr star) (Unit/all-elements-equal s star))

1.5.5 g is a right homotopy of f

We proceed by case analysis on e-1(inl y) = inr star + e-1(inl y) ≠ inr star. First, assume e-1(inl y) ≠ inr star. Remark that if e-1(inl y) ≠ inr star, then there must exists an x such that e-1(inl y) = inl x. 

double-counting/not-exception-value' (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (f : neg (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star)))
                                          : (u : Maybe X) → Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) u → X = split
  inl x → λ_. x
  inr s → λp. ex-falso X (f (comp (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr s) p (inr star) (Unit/inr X s)))

double-counting/not-exception-value (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (f : neg (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star))) : X =
  double-counting/not-exception-value' X Y e y f (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (refl (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)))

That is, we have a path e-1(inl y) = inl x by (mostly) judgmental equality. 

double-counting/convert-path'' (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (f : neg (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star)))
                               (x : X) (p : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inl x))
                                  : (q : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)))
            → Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inl (double-counting/not-exception-value' X Y e y f (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) q)) =
  tr (Maybe X) (inl x) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y))
     (inv (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inl x) p)
     (λu. (r : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) u)
           → Path (Maybe X) u (inl (double-counting/not-exception-value' X Y e y f u r)))
     (λ_. refl (Maybe X) (inl x))

double-counting/convert-path' (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (f : neg (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star)))
                                   : (u : Maybe X) → Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) u
                                                   → Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inl (double-counting/not-exception-value X Y e y f)) = split
  inl x → λp. double-counting/convert-path'' X Y e y f x p (refl (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)))
  inr s → λp. ex-falso (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inl (double-counting/not-exception-value X Y e y f)))
                       (f (comp (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr s) p (inr star) (Unit/inr X s)))

double-counting/convert-path (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (f : neg (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star)))
                                  : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inl (double-counting/not-exception-value X Y e y f)) =
  double-counting/convert-path' X Y e y f (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (refl (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)))

double-counting/convert-path-Y (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (p : neg (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star)))
                                  : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl (double-counting/not-exception-value X Y e y p))) (inl y) =
  let f : (Maybe X) → Maybe Y = Equiv/map (Maybe X) (Maybe Y) e
      g : Maybe Y → Maybe X = Equiv/inv-map (Maybe X) (Maybe Y) e
      x : X = double-counting/not-exception-value X Y e y p
  in
  comp (Maybe Y) (f (inl x)) (f (g (inl y)))
       (ap (Maybe X) (Maybe Y) f (inl x) (g (inl y)) (inv (Maybe X) (g (inl y)) (inl x) (double-counting/convert-path X Y e y p)))
       (inl y) (Equiv/inv-right-htpy (Maybe X) (Maybe Y) e (inl y))

Then, f(g(y)) = f(e-1(y)) = e(e-1(y)) = y. We can thus show the right homotopy in this case: 

double-counting/right-htpy-inr (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (f : neg (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star)))
                                    : Path Y (double-counting/map X Y e (double-counting/inv-map X Y e y)) y =  
  let x : X = (double-counting/not-exception-value X Y e y f) in
  comp Y (double-counting/map X Y e (double-counting/inv-map X Y e y))
         (double-counting/map X Y e x)
         (ap X Y (double-counting/map X Y e) (double-counting/inv-map X Y e y) x
                 (double-counting/inv-map-inl-id X Y e y x (double-counting/convert-path X Y e y f)))
         y (double-counting/map-inl-id X Y e x y (double-counting/convert-path-Y X Y e y f))

And in the other case: 

double-counting/right-htpy/star-value (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) (p : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star))
                                           : Path (Maybe Y) (Equiv/map (Maybe X) (Maybe Y) e (inl (double-counting/inv-map X Y e y))) (inr star) =
  let f : (Maybe X) → Maybe Y = Equiv/map (Maybe X) (Maybe Y) e
      g : Maybe Y → Maybe X = Equiv/inv-map (Maybe X) (Maybe Y) e
      h : Y → X = double-counting/inv-map X Y e
  in comp-n (Maybe Y) three-Nat
            (f (inl (h y))) (f (inl (star-value Y X (Equiv/sym (Maybe X) (Maybe Y) e) y p)))
            (ap X (Maybe Y) (λz. f (inl z)) (h y) (star-value Y X (Equiv/sym (Maybe X) (Maybe Y) e) y p)
                  (double-counting/inv-map-inr-id X Y e y p))
            (f (g (inr star))) (ap (Maybe X) (Maybe Y) (λz. f z) (inl (star-value Y X (Equiv/sym (Maybe X) (Maybe Y) e) y p)) (g (inr star))
                                   (star-value-htpy Y X (Equiv/sym (Maybe X) (Maybe Y) e) y p))
            (inr star) (Equiv/inv-right-htpy (Maybe X) (Maybe Y) e (inr star))

double-counting/right-htpy/inl (X Y : U) (eq : Equiv (Maybe X) (Maybe Y)) (y : Y) (p : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) eq (inl y)) (inr star))
                                    : Path (Maybe Y) (inl ((double-counting/map X Y eq) (double-counting/inv-map X Y eq y))) (inl y) =
  let e  : (Maybe X) → Maybe Y = Equiv/map (Maybe X) (Maybe Y) eq
      e' : Maybe Y → Maybe X = Equiv/inv-map (Maybe X) (Maybe Y) eq
      f : X → Y = double-counting/map X Y eq
      g : Y → X = double-counting/inv-map X Y eq
      q : Path (Maybe Y) (e (inl (g y))) (inr star) = double-counting/right-htpy/star-value X Y eq y p
  in comp-n (Maybe Y) four-Nat (inl (f (g y))) (inl (star-value X Y eq (g y) q))
      (ap Y (Maybe Y) (λz. inl z) (f (g y)) (star-value X Y eq (g y) q) (double-counting/map-inr-id X Y eq (g y) q))
      (e (inr star)) (star-value-htpy X Y eq (g y) q)
      (e (e' (inl y))) (ap (Maybe X) (Maybe Y) e (inr star) (e' (inl y)) (inv (Maybe X) (e' (inl y)) (inr star) p))
      (inl y) (Equiv/inv-right-htpy (Maybe X) (Maybe Y) eq (inl y))

double-counting/right-htpy-inl (X Y : U) (eq : Equiv (Maybe X) (Maybe Y)) (y : Y) (p : Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) eq (inl y)) (inr star))
                                    : Path Y ((double-counting/map X Y eq) (double-counting/inv-map X Y eq y)) y =
  Coprod/inl-inj Y Unit ((double-counting/map X Y eq) (double-counting/inv-map X Y eq y)) y (double-counting/right-htpy/inl X Y eq y p)

Thus, we have the result for the right homotopy. 

double-counting/right-htpy-dec (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y)
                                    : is-decidable (Path (Maybe X) (Equiv/inv-map (Maybe X) (Maybe Y) e (inl y)) (inr star))
                                      → Path Y ((double-counting/map X Y e) (double-counting/inv-map X Y e y)) y = split
  inl p → double-counting/right-htpy-inl X Y e y p
  inr f → double-counting/right-htpy-inr X Y e y f  

double-counting/right-htpy (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (y : Y) : Path Y ((double-counting/map X Y e) (double-counting/inv-map X Y e y)) y =
  double-counting/right-htpy-dec X Y e y
    ( double-counting/has-decidable-eq X
        ( Equiv/inv-map
          ( Maybe X)
          ( Maybe Y) e
          ( inl y)))

1.5.6 g is a left homotopy of f

As double-counting/inv-map is double-counting/map with a symmetric equivalence, we can use the right homotopy to show the left homotopy. 

double-counting/left-htpy' (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X)
                                : Path X (double-counting/inv-map X Y e (double-counting/map X Y (Equiv/sym (Maybe Y) (Maybe X) (Equiv/sym (Maybe X) (Maybe Y) e)) x)) x =
  double-counting/right-htpy Y X
    ( Equiv/sym (Maybe X) (Maybe Y) e) x

double-counting/left-htpy (X Y : U) (e : Equiv (Maybe X) (Maybe Y)) (x : X)
                               : Path X ((double-counting/inv-map X Y e) (double-counting/map X Y e x)) x =
  comp X
    ( (double-counting/inv-map X Y e) (double-counting/map X Y e x))
    ( (double-counting/inv-map X Y e) (double-counting/map X Y (Equiv/sym (Maybe Y) (Maybe X) (Equiv/sym (Maybe X) (Maybe Y) e)) x))
    ( ap
      ( Equiv (Maybe X) (Maybe Y)) X
      ( λe'. double-counting/inv-map X Y e ( double-counting/map X Y e' x)) e
      ( Equiv/sym (Maybe Y) (Maybe X) (Equiv/sym (Maybe X) (Maybe Y) e))
      ( Equiv/sym/sym' (Maybe X) (Maybe Y) e)) x
    ( double-counting/left-htpy' X Y e x)

1.5.7 X ≅ Y

We can conclude: f and g are inverses to each other, thus they are equivalences. Hence, X is equivalent to Y. 

double-counting/is-equiv (X Y : U) (e : Equiv (Maybe X) (Maybe Y))
                              : is-equiv X Y (double-counting/map X Y e) =
  has-inverse/is-equiv X Y
    ( double-counting/map X Y e)
    ( double-counting/inv-map X Y e,
      ( double-counting/right-htpy X Y e,
        double-counting/left-htpy X Y e))

double-counting/Equiv (X Y : U) (e : Equiv (Maybe X) (Maybe Y))
                           : Equiv X Y =
  ( double-counting/map X Y e,
    double-counting/is-equiv X Y e)

1.6 Fin k ≅ Fin l implies k = l

Fin/is-inj/z : (l : Nat) → Equiv (Fin zero) (Fin l) → Path Nat zero l = split
  zero → λ_. refl Nat zero
  suc l → λe. ex-falso
                ( Path Nat zero (suc l))
                ( Equiv/inv-map
                  ( Fin zero)
                  ( Fin (suc l)) e
                  ( zero-Fin l))

Fin/is-inj/s (k : Nat) (IH : (l : Nat) → Equiv (Fin k) (Fin l) → Path Nat k l) : (l : Nat) → Equiv (Fin (suc k)) (Fin l) → Path Nat (suc k) l = split
  zero → λe.  ex-falso
                ( Path Nat (suc k) zero)
                ( Equiv/map
                  ( Fin (suc k))
                  ( Fin zero) e
                  ( zero-Fin k))
  suc l → λe. ap Nat Nat
              ( λn. suc n) k l
              ( IH l
                ( double-counting/Equiv
                  ( Fin k)
                  ( Fin l) e))

Fin/is-inj : (k l : Nat) → Equiv (Fin k) (Fin l) → Path Nat k l = split
  zero → Fin/is-inj/z
  suc k → Fin/is-inj/s k
            ( Fin/is-inj k)

1.7 Equivalent types have the same counting

Using the previous theorem, we can show that equivalent types that have count have the same number of elements. 

double-counting/sg (A B : U) (k : Nat) (eK : Equiv (Fin k) A) (l : Nat) (eL : Equiv (Fin l) B) (e : Equiv A B)
                        : Path Nat k l =
  Fin/is-inj k l
    ( Equiv/trans (Fin k) A (Fin l) eK
      ( Equiv/trans A B (Fin l) e
        ( Equiv/sym (Fin l) B eL)))

double-counting (A B : U) (count-A : count A) (count-B : count B) (e : Equiv A B)
                     : Path Nat (number-of-elements A count-A) (number-of-elements B count-B) =
  double-counting/sg A B
    ( number-of-elements A count-A)
    ( count/Equiv A count-A)
    ( number-of-elements B count-B)
    ( count/Equiv B count-B) e

1.8 Two countings of the same type have the same number of elements

double-counting' (A : U) (c c' : count A)
                    : Path Nat (number-of-elements A c) (number-of-elements A c') =
  double-counting A A c c'
    ( Equiv/refl A)

1.9 Closure under Π-types

Counting is closed under Π-types. 

Fin/closed-Pi : (k : Nat) (B : Fin k → U) (cB : (x : Fin k) → count (B x)) → count ((x : Fin k) → B x) = split
  zero → λB _.
    count/contr-count
    ( (x : Empty) → B x)
    ( Empty/universal-dependent-property
      ( Empty) B
      ( Equiv/refl Empty))
  suc k → λB cB.
    count/closed-equiv
      ( (x : Fin (suc k)) → B x)
      ( ((x : Fin k) → B (inl x)) * (B (inr star)))
      ( Equiv/trans
        ( (x : Fin (suc k)) → B x)
        ( ((x : Fin k) → B (inl x)) * ((u : Unit) → B (inr u)))
        ( ((x : Fin k) → B (inl x)) * (B (inr star)))
        ( Coprod/dependent-universal-property
          ( Fin k) Unit B)
        ( Equiv/prod'
          ( (x : Fin k) → B (inl x))
          ( (u : Unit) → B (inr u))
          ( B (inr star))
          ( Equiv/pi-Unit
            ( λu. B (inr u)))))
      ( count/closed-Prod
        ( (x : Fin k) → B (inl x))
        ( B (inr star))
        ( Fin/closed-Pi k
          ( λx. B (inl x))
          ( λx. cB (inl x)))
        ( cB (inr star)))          

count/closed-Pi (A : U) (B : A → U) (cA : count A) (cB : (x : A) → count (B x)) : count ((x : A) → B x) =
  let k : Nat = number-of-elements A cA
      e : Equiv (Fin k) A = count/Equiv A cA 
  in
  count/closed-equiv
    ( (x : A) → B x)
    ( (x : Fin k) → B (Equiv/map (Fin k) A e x))
    ( Equiv/dependent
      ( Fin k) A B e)
    ( Fin/closed-Pi k
      ( λx. B (Equiv/map (Fin k) A e x))
      ( λx. cB (Equiv/map (Fin k) A e x)))

1.10 Unlock

unlock has-inverse/is-equiv

Author: Johann Rosain

Created: 2024-07-23 Tue 13:52

Validate