Circle.Integers-SymmetricInduction

Tom de Jong
Reboot: 22 January 2021
Earlier version: 18 September 2020

We show that the type of integers enjoys the symmetric induction principle, as
used in constructing the circle as the type of ℤ-torsors. The symmetric
induction principle appears as Theorem 3.13 in "Construction of the circle in
UniMath" by Bezem, Buchholtz, Grayson and Shulman
(doi:10.1016/j.jpaa.2021.106687).

\begin{code}

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

open import Naturals.UniversalProperty

open import Circle.Integers
open import Circle.Integers-Properties

open import MLTT.Spartan
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Subsingletons

module Circle.Integers-SymmetricInduction where

ℤ-symmetric-induction : {𝓤 : Universe}
                      → funext 𝓤₀ 𝓤
                      → (A : ℤ → 𝓤 ̇ )
                        (f : (z : ℤ) → A z ≃ A (succ-ℤ z))
                      → (Σ h ꞉ Π A , ((z : ℤ) → h (succ-ℤ z) ＝ ⌜ f z ⌝ (h z)))
                      ≃ A 𝟎
ℤ-symmetric-induction {𝓤} fe A f =
 (Σ h ꞉ Π A , Q₁ h)                                               ≃⟨ I    ⟩
 (Σ h ꞉ (Π (A ∘ ⌜𝟎⌝) × Π (A ∘ inr)) , Q₁ (g₁ h))                  ≃⟨ II   ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , Σ hᵣ ꞉ Π (A ∘ inr) , Q₁ (g₁ (hₒ , hᵣ)))    ≃⟨ III  ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , Σ hᵣ ꞉ (Π (A ∘ pos) × Π (A ∘ neg)),
                         Q₂ hₒ (g₂ hᵣ))                           ≃⟨ IV   ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , Σ hₚ ꞉ Π (A ∘ pos) ,
                       Σ hₙ ꞉ Π (A ∘ neg) , Q₂ hₒ (g₂ (hₚ , hₙ))) ≃⟨ V    ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , Σ hₚ ꞉ Π (A ∘ pos) ,
                       Σ hₙ ꞉ Π (A ∘ neg) , Qₚ (hₒ ⋆) hₚ
                                          × Qₙ' (hₒ ⋆) hₙ)        ≃⟨ VI   ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , ((Σ hₚ ꞉ Π (A ∘ pos) , Qₚ (hₒ ⋆) hₚ)
                     ×  (Σ hₙ ꞉ Π (A ∘ neg) , Qₙ' (hₒ ⋆) hₙ)))    ≃⟨ VII  ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , 𝟙 × (Σ hₙ ꞉ Π (A ∘ neg) , Qₙ' (hₒ ⋆) hₙ))  ≃⟨ VIII ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , Σ hₙ ꞉ Π (A ∘ neg) , Qₙ' (hₒ ⋆) hₙ)        ≃⟨ IX   ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , Σ hₙ ꞉ Π (A ∘ neg) , Qₙ (hₒ ⋆) hₙ)         ≃⟨ X    ⟩
 (Σ hₒ ꞉ Π (A ∘ ⌜𝟎⌝) , 𝟙)                                         ≃⟨ XI   ⟩
 Π (A ∘ ⌜𝟎⌝)                                                      ≃⟨ XII  ⟩
 A 𝟎 ■
  where
   ⌜𝟎⌝ : 𝟙 {𝓤₀} → ℤ
   ⌜𝟎⌝ _ = 𝟎
   Q₁ : Π A → 𝓤 ̇
   Q₁ h = (z : ℤ) → h (succ-ℤ z) ＝ ⌜ f z ⌝ (h z)
   g₁ : Π (A ∘ ⌜𝟎⌝) × Π (A ∘ inr) → Π A
   g₁ = ⌜ Π×+ fe ⌝
   Q₂ : Π (A ∘ ⌜𝟎⌝) → Π (A ∘ inr) → 𝓤 ̇
   Q₂ hₒ hᵣ = Q₁ (g₁ (hₒ , hᵣ))
   g₂ : Π (A ∘ pos) × Π (A ∘ neg) → Π (A ∘ inr)
   g₂ = ⌜ Π×+ fe ⌝
   Qₚ : A 𝟎 → Π (A ∘ pos) → 𝓤 ̇
   Qₚ aₒ hₚ = (hₚ 0 ＝ ⌜ f 𝟎 ⌝ aₒ)
            × ((n : ℕ) → hₚ (succ n) ＝ ⌜ f (pos n) ⌝ (hₚ n))
   Qₙ' : A 𝟎 → Π (A ∘ neg) → 𝓤 ̇
   Qₙ' a₀ hₙ = (a₀ ＝ ⌜ f (neg 0) ⌝ (hₙ 0))
             × ((n : ℕ) → hₙ n ＝ ⌜ f (neg (succ n)) ⌝ (hₙ (succ n)))
   Qₙ : A 𝟎 → Π (A ∘ neg) → 𝓤 ̇
   Qₙ aₒ hₙ = (hₙ 0 ＝ ⌜ (f (neg 0)) ⌝⁻¹ aₒ)
            × ((n : ℕ) → hₙ (succ n) ＝ ⌜ (f (neg (succ n))) ⌝⁻¹ (hₙ n))
   I    = ≃-sym (Σ-change-of-variable Q₁ g₁ (⌜⌝-is-equiv (Π×+ fe)))
   II   = Σ-assoc
   III  = Σ-cong
          (λ hₒ → ≃-sym (Σ-change-of-variable (Q₂ hₒ) g₂ (⌜⌝-is-equiv (Π×+ fe))))
   IV   = Σ-cong (λ _ → Σ-assoc)
   V    = Σ-cong λ hₒ → Σ-cong (λ hₚ → Σ-cong (λ hₙ → γ hₒ hₚ hₙ))
    where
     γ : (hₒ : Π (A ∘ ⌜𝟎⌝))  (hₚ : Π (A ∘ pos)) (hₙ : Π (A ∘ neg))
       → Q₂ hₒ (g₂ (hₚ , hₙ)) ≃ Qₚ (hₒ ⋆) hₚ × Qₙ' (hₒ ⋆) hₙ
     γ hₒ hₚ hₙ = qinveq φ (ψ , η , ε)
      where
       φ : Q₂ hₒ (g₂ (hₚ , hₙ)) → Qₚ (hₒ ⋆) hₚ × Qₙ' (hₒ ⋆) hₙ
       φ q = ((q 𝟎 , q ∘ pos) , (q (neg 0) , q ∘ neg ∘ succ))
       ψ : (Qₚ (hₒ ⋆) hₚ × Qₙ' (hₒ ⋆) hₙ) → Q₂ hₒ (g₂ (hₚ , hₙ))
       ψ ((qₒ , qₚ) , (qₒ' , qₙ')) = c
        where
         c : Q₂ hₒ (g₂ (hₚ , hₙ))
         c 𝟎              = qₒ
         c (pos n)        = qₚ n
         c (neg zero)     = qₒ'
         c (neg (succ n)) = qₙ' n
       ε : φ ∘ ψ ∼ id
       ε q = refl
       η : ψ ∘ φ ∼ id
       η q = dfunext fe c
        where
         c : (z : ℤ) → (ψ (φ q)) z ＝ q (z)
         c 𝟎              = refl
         c (pos n)        = refl
         c (neg zero)     = refl
         c (neg (succ n)) = refl
   VI   = Σ-cong γ
    where
     γ : (hₒ : Π (A ∘ ⌜𝟎⌝))
       → (Σ hₚ ꞉ Π (A ∘ pos) , Σ hₙ ꞉ Π (A ∘ neg) , Qₚ (hₒ ⋆) hₚ × Qₙ' (hₒ ⋆) hₙ)
       ≃ (  (Σ hₚ ꞉ Π (A ∘ pos) , Qₚ (hₒ ⋆) hₚ)
          × (Σ hₙ ꞉ Π (A ∘ neg) , Qₙ' (hₒ ⋆) hₙ))
     γ hₒ = Σ-interchange
   VII  = Σ-cong (λ hₒ → ×-cong (singleton-≃-𝟙 {𝓤} {𝓤₀} (γ hₒ)) (≃-refl _))
    where
     γ : (hₒ : Π (A ∘ ⌜𝟎⌝))
       → is-singleton ((Σ hₚ ꞉ Π (A ∘ pos) , Qₚ  (hₒ ⋆) hₚ))
     γ hₒ = (ℕ-is-nno-dep fe (A ∘ pos) a₀ s)
      where
       a₀ : A (pos 0)
       a₀ = ⌜ (f 𝟎) ⌝ (hₒ ⋆)
       s : (n : ℕ) → A (pos n) → A (pos (succ n))
       s n = ⌜ f (pos n) ⌝
   VIII = Σ-cong (λ hₒ → 𝟙-lneutral)
   IX   = Σ-cong (λ hₒ → Σ-cong (λ hₙ → γ hₒ hₙ))
    where
     γ : (hₒ : Π (A ∘ ⌜𝟎⌝)) (hₙ : Π (A ∘ neg))
       → Qₙ' (hₒ ⋆) hₙ ≃ Qₙ (hₒ ⋆) hₙ
     γ hₒ hₙ = ×-cong γ₀ (Π-cong fe fe γₙ)
      where
       f₀ = ⌜ f (neg 0) ⌝
       f₀⁻¹ = ⌜ (f (neg 0)) ⌝⁻¹
       e₀ : is-equiv f₀
       e₀ = ⌜⌝-is-equiv (f (neg 0))
       γ₀ : (hₒ ⋆ ＝ f₀ (hₙ 0))
          ≃ (hₙ 0 ＝ f₀⁻¹ (hₒ ⋆))
       γ₀ = (hₒ ⋆ ＝ f₀ (hₙ 0))             ≃⟨ I₀   ⟩
            (f₀ (hₙ 0) ＝ hₒ ⋆)             ≃⟨ II₀  ⟩
            (f₀ (hₙ 0) ＝ f₀ (f₀⁻¹ (hₒ ⋆))) ≃⟨ III₀ ⟩
            (hₙ 0 ＝ f₀⁻¹ (hₒ ⋆)) ■
        where
         I₀   = ＝-flip
         II₀  = ＝-cong-r (f₀ (hₙ 0)) (hₒ ⋆)
                 ((inverses-are-sections f₀ e₀ (hₒ ⋆)) ⁻¹)
         III₀ = embedding-criterion-converse f₀
                 (equivs-are-embeddings f₀ e₀)
                 (hₙ 0) (f₀⁻¹ (hₒ ⋆))
       fₙ : (n : ℕ) → A (neg (succ n)) → A (neg n)
       fₙ n = ⌜ f (neg (succ n)) ⌝
       eₙ : (n : ℕ) → is-equiv (fₙ n)
       eₙ n = ⌜⌝-is-equiv (f (neg (succ n)))
       fₙ⁻¹ : (n : ℕ) → A (neg n) → A (neg (succ n))
       fₙ⁻¹ n = ⌜ (f (neg (succ n))) ⌝⁻¹
       γₙ : (n : ℕ)
          → (hₙ n ＝ fₙ n (hₙ (succ n)))
          ≃ (hₙ (succ n) ＝ fₙ⁻¹ n (hₙ n))
       γₙ n = (hₙ n ＝ fₙ n (hₙ (succ n)))                 ≃⟨ Iₙ ⟩
              (fₙ n (hₙ (succ n)) ＝ hₙ n)                 ≃⟨ IIₙ ⟩
              (fₙ n (hₙ (succ n)) ＝ fₙ n (fₙ⁻¹ n (hₙ n))) ≃⟨ IIIₙ ⟩
              (hₙ (succ n) ＝ fₙ⁻¹ n (hₙ n))               ■
        where
         Iₙ   = ＝-flip
         IIₙ  = ＝-cong-r (fₙ n (hₙ (succ n))) (hₙ n)
                 ((inverses-are-sections (fₙ n) (eₙ n) (hₙ n)) ⁻¹)
         IIIₙ = embedding-criterion-converse (fₙ n)
                 (equivs-are-embeddings (fₙ n) (eₙ n))
                 (hₙ (succ n)) (fₙ⁻¹ n (hₙ n))
   X    = Σ-cong (λ hₒ → singleton-≃-𝟙 {𝓤} {𝓤₀} (γ hₒ))
    where
     γ : (hₒ : Π (A ∘ ⌜𝟎⌝))
       → is-singleton ((Σ hₙ ꞉ Π (A ∘ neg) , Qₙ  (hₒ ⋆) hₙ))
     γ hₒ = (ℕ-is-nno-dep fe (A ∘ neg) a₀ s)
      where
       a₀ : A (neg 0)
       a₀ = ⌜ (f (neg 0)) ⌝⁻¹ (hₒ ⋆)
       s : (n : ℕ) → A (neg n) → A (neg (succ n))
       s n = ⌜ (f (neg (succ n))) ⌝⁻¹
   XI   = 𝟙-rneutral
   XII  = ≃-sym (𝟙→ fe)

\end{code}