Skip to content

Fin.ArithmeticViaEquivalence

Arithmetic via equivalence
--------------------------

MartΓ­n HΓΆtzel EscardΓ³

Originally 10 July 2014, modified 10 Oct 2017, 22 March 2018, 25 Nov 2019.

This is a literate proof in univalent mathematics, in Agda
notation. Although the concepts of univalent mathematics are used, the
univalence axiom is not needed.

We have that 3+3+3+3+3 = 5+5+5, or 5Γ—3 = 3Γ—5, and more generally

  mΓ—n = nΓ—m.

This can of course be proved by induction. A more appealing pictorial
proof is

  ooo
  ooo         ooooo
  ooo    =    ooooo
  ooo         ooooo
  ooo

where "o" is a pebble. We just rotate the grid of pebbles, or swap
the coordinates, and doing this doesn't change the number of pebbles.

How can this proof be formally rendered, as faithfully as possible to
the intuition?

We first define an interpretation function Fin : β„• β†’ 𝓀₀ of numbers as
sets (in the universe 𝓀₀) by

 (1) Fin   0  = 𝟘,          where 𝟘 is the empty set,
 (2) Fin(n+1) = Fin n + πŸ™,  where πŸ™ is the singleton set,

Then Fin is a semiring homomorphism:

 (3) Fin(m + n) ≃ Fin m + Fin n, where "+" in the rhs is disjoint union,
 (4) Fin 1 ≃ πŸ™,
 (5) Fin(m Γ— n) ≃ Fin m Γ— Fin n, where "Γ—" in the rhs is cartesian product,

It is also left-cancellable:

 (6) Fin m ≃ Fin n β†’ m = n.

Two boxes with the same number of pebbles are counted by same number.

But instead of proving (3)-(5) after defining addition and
multiplication, we prove that

 (3') For every m,n:β„• there is k:β„• with Fin k ≃ Fin m + Fin n.
 (5') For every m,n:β„• there is k:β„• with Fin k ≃ Fin m Γ— Fin n.

We then define addition and multiplication on β„• from (3') and (5'),
from which (3) and (5) follow tautologically.

This relies on type arithmetic. To prove (3'), we use the trivial
bijections, or *equivalences* in the terminology of univalent
mathematics,

 X ≃ X + 𝟘,
 (X + Y) + πŸ™ ≃ X + (Y + πŸ™),

mimicking the definition of addition on β„• in Peano arithmetic (but
with the equations written backwards).

To prove (4), we use the equivalence

 𝟘 + πŸ™ ≃ πŸ™

To prove (5'), we use the equivalences

 𝟘 ≃ X Γ— 𝟘,
 X Γ— Y + X ≃ X Γ— (Y + πŸ™),

mimicking the definition of multiplication on β„• in Peano arithmetic
(again backwards).

To prove the cancellation property (6), we use the cancellation
property

 X + πŸ™ ≃ Y + πŸ™ β†’ X ≃ Y,

mimicking the cancellation property of the successor function on β„•.
(This is the only combinatorial argument here.)

Now, relying on the equivalence

 X Γ— Y ≃ Y Γ— X,

which corresponds to the rotation of the grid of pebbles, we can prove
m Γ— n = n Γ— m as follows:

 Fin(m Γ— n) ≃ Fin m Γ— Fin n   by (5)
            ≃ Fin n Γ— Fin m   by  X Γ— Y ≃ Y Γ— X,
            ≃ Fin(n Γ— m)      by (5),

and so

 m Γ— n ≃ n Γ— m                by (6).

Similarly we can prove, of course,

 m + n ≃ n + m

using (3) and the equivalence

 X + Y ≃ Y + X.

Among all these constructions, we use induction on β„• only in

  * the definition (1-2) of the function Fin : β„• β†’ 𝓀₀,

  * the existence (3')-(5') of addition and multiplication, and

  * the left-cancellability (6) of Fin.

With this, induction is not needed to prove that addition and
multiplication are commutative.

Side-remark, to be explored in a future version. From the equivalence

 (5) Fin(m Γ— n) ≃ Fin m Γ— Fin n

we get two maps

     f : Fin(m Γ— n) β†’ Fin m,
     g : Fin(m Γ— n) β†’ Fin n,

which we didn't define explicitly or combinatorially.

21st March 2018 remark: After doing this, I found this article by Tim
Gowers:

    Why is multiplication commutative?
    https://www.dpmms.cam.ac.uk/~wtg10/commutative.html

which says very much the same as above (implemented below in univalent
foundations in Agda notation).


{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan hiding (_^_)

module Fin.ArithmeticViaEquivalence where

open import Fin.Bishop
open import Fin.Properties
open import Fin.Topology
open import Fin.Type
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.PropTrunc
open import UF.Subsingletons


The 1st definition by induction is that of the function Fin defined in
the module Fin imported above, namely

  Fin   0  = 𝟘,
  Fin(n+1) = Fin n + πŸ™.

From a natural number n, get a finite set Fin n with n elements. This
can be considered as an interpretation function, which defines the
meaning of numbers as types.

2nd definition by induction. Existence of addition:


+construction : (m n : β„•) β†’ Ξ£ k κž‰ β„• , Fin k ≃ Fin m + Fin n
+construction m zero = m , 𝟘-rneutral
+construction m (succ n) = g
  where
    IH : Ξ£ k κž‰ β„• , Fin k ≃ Fin m + Fin n
    IH = +construction m n
    k : β„•
    k = pr₁ IH
    Ο† : Fin k ≃ Fin m + Fin n
    Ο† = prβ‚‚ IH

    Ο†' =  Fin k + πŸ™           β‰ƒβŸ¨ Ap+ πŸ™ Ο† ⟩
         (Fin m + Fin n) + πŸ™  β‰ƒβŸ¨ +assoc ⟩
         (Fin m + Fin n + πŸ™)  β– 

    g : Ξ£ k' κž‰ β„• , Fin k' ≃ Fin m + Fin (succ n)
    g = succ k , Ο†'


The construction gives an addition function by projection:


_+'_ : β„• β†’ β„• β†’ β„•
m +' n = pr₁(+construction m n)

infixl 20 _+'_


The construction also shows that its satisfies the usual
characterizing equations from Peano arithmetic:


+base : {m : β„•} β†’ m +' zero ＝ m
+base = refl

+step : {m n : β„•} β†’ m +' (succ n) ＝ succ(m +' n)
+step = refl


Tautologically, we get that Fin : β„• β†’ 𝓀₀ is an
addition-homomorphism:


Fin+homo : (m n : β„•) β†’ Fin(m +' n) ≃ Fin m + Fin n
Fin+homo m n = prβ‚‚(+construction m n)


The 3rd and last use of induction is for the left-cancellability of
Fin : β„• β†’ 𝓀₀, which is in the module Fin.

With this, no further induction is needed to prove commutativity of
addition:


+'-comm : (m n : β„•) β†’ m +' n ＝ n +' m
+'-comm m n = Fin-lc (m +' n) (n +' m)
 (Fin (m +' n)   β‰ƒβŸ¨ Fin+homo m n ⟩
  Fin m + Fin n  β‰ƒβŸ¨ +comm ⟩
  Fin n + Fin m  β‰ƒβŸ¨ ≃-sym (Fin+homo n m) ⟩
  Fin (n +' m)   β– )


Exercise. Associativity without induction.

We now repeat this story for multiplication:


Γ—construction : (m n : β„•) β†’ Ξ£ k κž‰ β„• , Fin k ≃ Fin m Γ— Fin n
Γ—construction m zero = zero , Γ—πŸ˜
Γ—construction m (succ n) = g
  where
    IH : Ξ£ k κž‰ β„• , Fin k ≃ Fin m Γ— Fin n
    IH = Γ—construction m n
    k : β„•
    k = pr₁ IH
    Ο† : Fin k ≃ Fin m Γ— Fin n
    Ο† = prβ‚‚ IH

    Ο†' = Fin (k +' m)          β‰ƒβŸ¨ Fin+homo k m ⟩
         Fin k + Fin m         β‰ƒβŸ¨ Ap+ (Fin m) Ο† ⟩
         Fin m Γ— Fin n + Fin m β‰ƒβŸ¨ πŸ™distr ⟩
         Fin m Γ— (Fin n + πŸ™)   β– 

    g : Ξ£ k' κž‰ β„• , Fin k' ≃ Fin m Γ— Fin (succ n)
    g = (k +' m) , Ο†'

_Γ—'_ : β„• β†’ β„• β†’ β„•
m Γ—' n = pr₁(Γ—construction m n)

infixl 22 _Γ—'_

Γ—base : {m : β„•} β†’ m Γ—' zero ＝ zero
Γ—base = refl

Γ—step : {m n : β„•} β†’ m Γ—' (succ n) ＝ m Γ—' n +' m
Γ—step = refl

FinΓ—homo : (m n : β„•) β†’ Fin(m Γ—' n) ≃ Fin m Γ— Fin n
FinΓ—homo m n = prβ‚‚(Γ—construction m n)

Γ—'-comm : (m n : β„•) β†’ m Γ—' n ＝ n Γ—' m
Γ—'-comm m n = Fin-lc (m Γ—' n) (n Γ—' m)
 (Fin (m Γ—' n)   β‰ƒβŸ¨ FinΓ—homo m n ⟩
  Fin m Γ— Fin n  β‰ƒβŸ¨ Γ—comm ⟩
  Fin n Γ— Fin m  β‰ƒβŸ¨ ≃-sym (FinΓ—homo n m) ⟩
  Fin (n Γ—' m)   β– )


Exercise. Associativity without induction.

Added 30th August 2018: Exponentiation. Requires one more induction
and function extensionality.


open import UF.FunExt

module exponentiation-and-factorial (fe : FunExt) where

 feβ‚€ : funext 𝓀₀ 𝓀₀
 feβ‚€ = fe 𝓀₀ 𝓀₀

 β†’construction : (m n : β„•) β†’ Ξ£ k κž‰ β„• , Fin k ≃ (Fin m β†’ Fin n)
 β†’construction zero n = succ zero ,
                        (𝟘 + πŸ™        β‰ƒβŸ¨ 𝟘-lneutral ⟩
                         πŸ™            β‰ƒβŸ¨ πŸ˜β†’ feβ‚€ ⟩
                        (𝟘 β†’ Fin n)   β– )
 β†’construction (succ m) n = g
  where
   IH : Ξ£ k κž‰ β„• , Fin k ≃ (Fin m β†’ Fin n)
   IH = β†’construction m n
   k : β„•
   k = pr₁ IH
   Ο† : Fin k ≃ (Fin m β†’ Fin n)
   Ο† = prβ‚‚ IH

   Ο†' = Fin (k Γ—' n)                   β‰ƒβŸ¨ FinΓ—homo k n ⟩
        Fin k Γ— Fin n                  β‰ƒβŸ¨ Γ—-cong Ο† (πŸ™β†’ feβ‚€) ⟩
       (Fin m β†’ Fin n) Γ— (πŸ™ β†’ Fin n)   β‰ƒβŸ¨ ≃-sym (+β†’ feβ‚€) ⟩
       (Fin m + πŸ™ β†’ Fin n)             β– 

   g : Ξ£ k' κž‰ β„• , Fin k' ≃ (Fin (succ m) β†’ Fin n)
   g = k Γ—' n , Ο†'

 _^_ : β„• β†’ β„• β†’ β„•
 n ^ m = pr₁(β†’construction m n)

 infixl 23 _^_

 ^base : {n : β„•} β†’ n ^ zero ＝ succ zero
 ^base = refl

 ^step : {m n : β„•} β†’ n ^ (succ m) ＝ (n ^ m) Γ—' n
 ^step = refl

 Fin^homo : (m n : β„•) β†’ Fin(n ^ m) ≃ (Fin m β†’ Fin n)
 Fin^homo m n = prβ‚‚(β†’construction m n)


 Then, without the need for induction, we get the exponential laws:


 ^+homo : (k m n : β„•) β†’ k ^ (m +' n) ＝ (k ^ m) Γ—' (k ^ n)
 ^+homo k m n = Fin-lc (k ^ (m +' n)) (k ^ m Γ—' k ^ n)
  (Fin (k ^ (m +' n))                β‰ƒβŸ¨ Fin^homo (m +' n) k ⟩
  (Fin (m +' n) β†’ Fin k)             β‰ƒβŸ¨ β†’cong feβ‚€ feβ‚€ (Fin+homo m n) (≃-refl (Fin k)) ⟩
  (Fin m + Fin n β†’ Fin k)            β‰ƒβŸ¨ +β†’ feβ‚€  ⟩
  (Fin m β†’ Fin k) Γ— (Fin n β†’ Fin k)  β‰ƒβŸ¨ Γ—-cong (≃-sym (Fin^homo m k)) (≃-sym (Fin^homo n k)) ⟩
   Fin (k ^ m) Γ— Fin (k ^ n)         β‰ƒβŸ¨ ≃-sym (FinΓ—homo (k ^ m) (k ^ n)) ⟩
   Fin (k ^ m Γ—' k ^ n)              β– )

 iterated^ : (k m n : β„•) β†’ k ^ (m Γ—' n) ＝ (k ^ n) ^ m
 iterated^ k m n = Fin-lc (k ^ (m Γ—' n)) (k ^ n ^ m)
    (Fin (k ^ (m Γ—' n))        β‰ƒβŸ¨ Fin^homo (m Γ—' n) k ⟩
    (Fin (m Γ—' n) β†’ Fin k)     β‰ƒβŸ¨ β†’cong feβ‚€ feβ‚€ (FinΓ—homo m n) (≃-refl (Fin k)) ⟩
    (Fin m Γ— Fin n β†’ Fin k)    β‰ƒβŸ¨ curry-uncurry fe ⟩
    (Fin m β†’ (Fin n β†’ Fin k))  β‰ƒβŸ¨ β†’cong feβ‚€ feβ‚€ (≃-refl (Fin m)) (≃-sym (Fin^homo n k)) ⟩
    (Fin m β†’ Fin (k ^ n))      β‰ƒβŸ¨ ≃-sym (Fin^homo m (k ^ n)) ⟩
     Fin (k ^ n ^ m)           β– )


Added 25t November 2019: Numerical factorial from the type theoretical
factorial, which also uses function extensionality (which is not
actually necessary - see the comments in the module
Factorial.Law).


 open import Factorial.Law fe public

 !construction : (n : β„•) β†’ Ξ£ k κž‰ β„• , Fin k ≃ Aut (Fin n)
 !construction zero = 1 ,
                      (Fin 1          β‰ƒβŸ¨ ≃-refl (Fin 1) ⟩
                       𝟘 + πŸ™          β‰ƒβŸ¨ 𝟘-lneutral ⟩
                       πŸ™              β‰ƒβŸ¨ factorial-base ⟩
                       Aut (Fin zero) β– )
 !construction (succ n) = g
  where
   IH : Ξ£ k κž‰ β„• , Fin k ≃ Aut(Fin n)
   IH = !construction n
   k : β„•
   k = pr₁ IH
   Ο† : Fin k ≃ Aut(Fin n)
   Ο† = prβ‚‚ IH

   Ο†' = Fin (succ n Γ—' k)         β‰ƒβŸ¨ FinΓ—homo (succ n) k ⟩
        Fin (succ n) Γ— Fin k      β‰ƒβŸ¨ Γ—-cong (≃-refl (Fin (succ n))) Ο† ⟩
        (Fin n + πŸ™) Γ— Aut (Fin n) β‰ƒβŸ¨ discrete-factorial (Fin n) Fin-is-discrete ⟩
        Aut (Fin n + πŸ™)           β– 

   g : Ξ£ k' κž‰ β„• , Fin k' ≃ Aut (Fin (succ n))
   g = succ n Γ—' k , Ο†'


Geometric definition of the factorial function:


 _! : β„• β†’ β„•
 n ! = pr₁ (!construction n)

 infix 100 _!


The following are theorems rather than definitions:


 !-base : 0 ! ＝ 1
 !-base = refl

 !-step : (n : β„•) β†’ (n +' 1)! ＝ (n +' 1) Γ—' n !
 !-step n = refl


Added 8th December 2019. Some corollaries.

Recall that a type X is finite if there is n : β„• with X ≃ Fin n.


module _ (pt : propositional-truncations-exist)
         (fe : FunExt)
         {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         where

 open PropositionalTruncation pt
 open finiteness pt
 open exponentiation-and-factorial fe
 open import UF.Equiv-FunExt

 Aut-finite : is-finite X β†’ is-finite (Aut X)
 Aut-finite (n , Ξ±) = n ! , Ξ³
  where
   Ξ΄ : X ≃ Fin n β†’ Aut X ≃ Fin (n !)
   Ξ΄ d = Aut X       β‰ƒβŸ¨ ≃-cong fe d d ⟩
         Aut (Fin n) β‰ƒβŸ¨ ≃-sym (prβ‚‚ (!construction n)) ⟩
         Fin (n !)   β– 
   Ξ³ : βˆ₯ Aut X ≃ Fin (n !) βˆ₯
   Ξ³ = βˆ₯βˆ₯-functor Ξ΄ Ξ±

 module _ {π“₯ : Universe} {Y : π“₯ Μ‡ } where

  +finite : is-finite X β†’ is-finite Y β†’ is-finite (X + Y)
  Γ—finite : is-finite X β†’ is-finite Y β†’ is-finite (X Γ— Y)
  β†’finite : is-finite X β†’ is-finite Y β†’ is-finite (X β†’ Y)

  +finite (m , Ξ±) (n , Ξ²) = m +' n , Ξ³
   where
    Ξ΄ : X ≃ Fin m β†’ Y ≃ Fin n β†’ X + Y ≃ Fin (m +' n)
    Ξ΄ d e = X + Y         β‰ƒβŸ¨ +-cong d e ⟩
            Fin m + Fin n β‰ƒβŸ¨ ≃-sym (prβ‚‚ (+construction m n)) ⟩
            Fin (m +' n)  β– 
    Ξ³ : βˆ₯ X + Y ≃ Fin (m +' n) βˆ₯
    Ξ³ = βˆ₯βˆ₯-functorβ‚‚ Ξ΄ Ξ± Ξ²

  Γ—finite (m , Ξ±) (n , Ξ²) = m Γ—' n , Ξ³
   where
    Ξ΄ : X ≃ Fin m β†’ Y ≃ Fin n β†’ X Γ— Y ≃ Fin (m Γ—' n)
    Ξ΄ d e = X Γ— Y         β‰ƒβŸ¨ Γ—-cong d e ⟩
            Fin m Γ— Fin n β‰ƒβŸ¨ ≃-sym (prβ‚‚ (Γ—construction m n)) ⟩
            Fin (m Γ—' n)  β– 
    Ξ³ : βˆ₯ X Γ— Y ≃ Fin (m Γ—' n) βˆ₯
    Ξ³ = βˆ₯βˆ₯-functorβ‚‚ Ξ΄ Ξ± Ξ²

  β†’finite (m , Ξ±) (n , Ξ²) = n ^ m , Ξ³
   where
    Ξ΄ : X ≃ Fin m β†’ Y ≃ Fin n β†’ (X β†’ Y) ≃ Fin (n ^ m)
    Ξ΄ d e = (X β†’ Y)         β‰ƒβŸ¨ β†’cong (fe 𝓀₀ 𝓀₀) (fe 𝓀 π“₯) d e ⟩
            (Fin m β†’ Fin n) β‰ƒβŸ¨ ≃-sym (prβ‚‚ (β†’construction m n)) ⟩
            Fin (n ^ m)     β– 
    Ξ³ : βˆ₯ (X β†’ Y) ≃ Fin (n ^ m) βˆ₯
    Ξ³ = βˆ₯βˆ₯-functorβ‚‚ Ξ΄ Ξ± Ξ²


We have accounted for the type constructors +, Γ—, β†’, and ≃ (and hence
＝ if we assume univalence). The last two types to account for in our
spartan MLTT are Ξ  and Ξ£.


open import UF.PropIndexedPiSigma

Ξ£-construction : (n : β„•) (a : Fin n β†’ β„•)
               β†’ Ξ£ k κž‰ β„• , Fin k ≃ (Ξ£ i κž‰ Fin n , Fin (a i))
Ξ£-construction 0 a = 0 , (Fin 0                    β‰ƒβŸ¨by-definition⟩
                         𝟘                        β‰ƒβŸ¨ ≃-sym (empty-indexed-sum-is-𝟘 id) ⟩
                         (Ξ£ i κž‰ 𝟘 , Fin (a i)) β– )
Ξ£-construction (succ n) a = g
 where
  IH : Ξ£ k κž‰ β„• , Fin k ≃ (Ξ£ i κž‰ Fin n , Fin (a (suc i)))
  IH = Ξ£-construction n (Ξ» i β†’ a (suc i))
  k : β„•
  k = pr₁ IH
  Ο† : Fin k ≃ (Ξ£ i κž‰ Fin n , Fin (a (suc i)))
  Ο† = prβ‚‚ IH
  Ο†' = Fin (a 𝟎 +' k)                                                      β‰ƒβŸ¨ i ⟩
       Fin (a 𝟎) + Fin k                                                   β‰ƒβŸ¨ ii ⟩
       Fin k + Fin (a 𝟎)                                                   β‰ƒβŸ¨ iii ⟩
       (Ξ£ i κž‰ Fin n , Fin (a (suc i))) + (Ξ£ i κž‰ πŸ™ , Fin (a (inr i))) β‰ƒβŸ¨ iv ⟩
      (Ξ£ i κž‰ Fin n + πŸ™ , Fin (a i))                                     β– 
   where
    i   = prβ‚‚ (+construction (a 𝟎) k)
    ii  = +comm
    iii = +-cong Ο† (≃-sym (prop-indexed-sum ⋆ πŸ™-is-prop))
    iv  = Ξ£+-split (Fin n) πŸ™ (Ξ» i β†’ Fin (a i))

  g : Ξ£ k' κž‰ β„• , Fin k' ≃ (Ξ£ i κž‰ Fin (succ n) , Fin (a i))
  g = a 𝟎 +' k , Ο†'


The numerical sum:


βˆ‘ : {n : β„•} β†’ (Fin n β†’ β„•) β†’ β„•
βˆ‘ {n} a = pr₁ (Ξ£-construction n a)

βˆ‘-property : {n : β„•} (a : Fin n β†’ β„•) β†’ Fin (βˆ‘ a) ≃ (Ξ£ i κž‰ Fin n , Fin (a i))
βˆ‘-property {n} a = prβ‚‚ (Ξ£-construction n a)


Which is characterized by its usual inductive definition:


βˆ‘-base : (a : Fin 0 β†’ β„•)
       β†’ βˆ‘ a ＝ 0
βˆ‘-base a = refl

βˆ‘-step : {n : β„•} (a : Fin (succ n) β†’ β„•)
       β†’ βˆ‘ a ＝ a 𝟎 +' βˆ‘ (a ∘ suc)
βˆ‘-step {n} a = refl


For Ξ  we need function extensionality:


module _ (fe : funext 𝓀₀ 𝓀₀) where

 Ξ -construction : (n : β„•) (a : Fin n β†’ β„•)
                β†’ Ξ£ k κž‰ β„• , Fin k ≃ (Ξ  i κž‰ Fin n , Fin (a i))
 Ξ -construction 0 a = 1 , (Fin 1                     β‰ƒβŸ¨ i ⟩
                          𝟘 + πŸ™                     β‰ƒβŸ¨ ii ⟩
                          πŸ™                         β‰ƒβŸ¨ iii ⟩
                          (Ξ  i κž‰ 𝟘 , Fin (a i))     β‰ƒβŸ¨ iv ⟩
                          (Ξ  i κž‰ Fin 0 , Fin (a i)) β– )
  where
   i   = ≃-refl _
   ii  = 𝟘-lneutral
   iii = ≃-sym (empty-indexed-product-is-πŸ™ fe id)
   iv  = ≃-refl _

 Ξ -construction (succ n) a = g
  where
   IH : Ξ£ k κž‰ β„• , Fin k ≃ (Ξ  i κž‰ Fin n , Fin (a (suc i)))
   IH = Ξ -construction n (Ξ» i β†’ a (suc i))
   k : β„•
   k = pr₁ IH
   Ο† : Fin k ≃ (Ξ  i κž‰ Fin n , Fin (a (suc i)))
   Ο† = prβ‚‚ IH
   Ο†' = Fin (a 𝟎 Γ—' k)                                                      β‰ƒβŸ¨ i ⟩
        Fin (a 𝟎) Γ— Fin k                                                   β‰ƒβŸ¨ ii ⟩
        Fin k Γ— Fin (a 𝟎)                                                   β‰ƒβŸ¨ iii ⟩
        (Ξ  i κž‰ Fin n , Fin (a (suc i))) Γ— (Ξ  i κž‰ πŸ™ , Fin (a (inr i))) β‰ƒβŸ¨ iv ⟩
        (Ξ  i κž‰ Fin n + πŸ™ , Fin (a i))                                    β– 
    where
     i   = prβ‚‚ (Γ—construction (a 𝟎) k)
     ii  = Γ—comm
     iii = Γ—-cong Ο† (≃-sym (prop-indexed-product ⋆ fe πŸ™-is-prop))
     iv  = Ξ Γ—+ fe

   g : Ξ£ k' κž‰ β„• , Fin k' ≃ (Ξ  i κž‰ Fin (succ n) , Fin (a i))
   g = a 𝟎 Γ—' k , Ο†'

 ∏ : {n : β„•} β†’ (Fin n β†’ β„•) β†’ β„•
 ∏ {n} a = pr₁ (Ξ -construction n a)

 ∏-property : {n : β„•} (a : Fin n β†’ β„•) β†’ Fin (∏ a) ≃ (Ξ  i κž‰ Fin n , Fin (a i))
 ∏-property {n} a = prβ‚‚ (Ξ -construction n a)

 ∏-base : (a : Fin 0 β†’ β„•)
        β†’ ∏ a ＝ 1
 ∏-base a = refl

 ∏-step : {n : β„•} (a : Fin (succ n) β†’ β„•)
        β†’ ∏ a ＝ a 𝟎 Γ—' ∏ (a ∘ suc)
 ∏-step {n} a = refl


In order to avoid the use of the commutativity of + and Γ— to get the
natural inductive constructions of βˆ‘ and ∏, it would have been better
to have defined Fin(succ n) = πŸ™ + Fin n. In retrospect, this
definition seems more natural in general.

TODO: Corollary. If X is a type and A is an X-indexed family of types,
and if X is finite and A x is finite for every x : X, then the types Ξ£ A
and Ξ  A are finite.