Pi.Lehmer.Lehmer2

{-# OPTIONS --without-K --rewriting #-}

module Pi.Lehmer.Lehmer2 where

open import HoTT

Lehmer : ℕ → Type₀
Lehmer O = Fin (S O)
Lehmer (S n) = Fin (S (S n)) × Lehmer n

open import Pi.Lehmer.Lehmer renaming (Lehmer to Lehmer1)
open import Pi.Lehmer.LehmerFinEquiv
  using (LehmerInd)
  renaming (Lehmer-O-level to Lehmer1-O-level)
open import Pi.Common.Extra
open import Pi.Common.Misc

Lehmer2 = Lehmer

instance
  Lehmer-O-level : is-contr (Lehmer O)
  Lehmer-O-level =
    has-level-in ((0 , ltS) , λ { (O , ϕ) → fin= idp ; (S n , ltSR ()) })

  Lehmer-level : {n : ℕ} → is-set (Lehmer n)
  Lehmer-level {O} = contr-is-set Lehmer-O-level
  Lehmer-level {S n} = ×-level Fin-is-set (Lehmer-level {n})

Lehmer1-Lehmer2-equiv : {n : ℕ} →  Lehmer1 n ≃ Lehmer2 n
Lehmer1-Lehmer2-equiv {O} =
  Lehmer1 O ≃⟨ contr-equiv-Unit Lehmer1-O-level ⟩
  Unit ≃⟨ contr-equiv-Unit Lehmer-O-level ⁻¹ ⟩
  Lehmer2 O ≃∎
Lehmer1-Lehmer2-equiv {S n} =
  Lehmer1 (S n) ≃⟨ (LehmerInd {n}) ⁻¹ ⟩
  Fin (S (S n)) × Lehmer1 n ≃⟨ _ , (×-isemap-r (Fin (S (S n))) (snd (Lehmer1-Lehmer2-equiv {n}))) ⟩
  Fin (S (S n)) × Lehmer2 n ≃∎