-
Notifications
You must be signed in to change notification settings - Fork 1
/
Lehmer2FinEquiv.agda
30 lines (23 loc) · 1.06 KB
/
Lehmer2FinEquiv.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
{-# OPTIONS --rewriting --without-K --exact-split --overlapping-instances #-}
module Pi.Lehmer.Lehmer2FinEquiv where
open import HoTT hiding (_≤_; _<_; ≤-has-all-paths ; ltS ; ltSR)
import lib.types.Nat as N
open import Pi.Common.Misc
open import Pi.Lehmer.FinExcept
open import Pi.Lehmer.Lehmer2
open import Pi.Coxeter.InvTransform
open import Pi.UFin.BAut
open import Pi.Common.Extra
open import Pi.Lehmer.FinExcept
Fin≃Lehmer-aux : {n : ℕ} -> Aut (Fin (S n)) ≃ Lehmer n
Fin≃Lehmer-aux {O} =
Aut (Fin (S O)) ≃⟨ contr-equiv-Unit (Aut-level {{Fin1-level}}) ⟩
Unit ≃⟨ contr-equiv-Unit Fin1-level ⁻¹ ⟩
Lehmer O ≃∎
Fin≃Lehmer-aux {S m} =
Fin (S (S m)) ≃ Fin (S (S m)) ≃⟨ i ⟩
Σ (Fin (S (S m))) (λ k → FinExcept fzero ≃ FinExcept k) ≃⟨ Σ-cong-equiv-snd ii ⟩
Fin (S (S m)) × (Fin (S m) ≃ Fin (S m)) ≃⟨ _ , ×-isemap-r (Fin (S (S m))) (snd (Fin≃Lehmer-aux {m})) ⟩
Fin (S (S m)) × Lehmer m ≃∎
Fin≃Lehmer : {n : ℕ} -> Aut (Fin (S n)) ≃ Lehmer n
Fin≃Lehmer = Fin≃Lehmer-aux ∘e inv-transform-equiv