-
Notifications
You must be signed in to change notification settings - Fork 1
/
Lehmer2.agda
37 lines (29 loc) · 1.14 KB
/
Lehmer2.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
{-# 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 ≃∎