-
Notifications
You must be signed in to change notification settings - Fork 1
/
Sn.agda
75 lines (63 loc) · 3.07 KB
/
Sn.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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
{-# OPTIONS --without-K --rewriting --overlapping-instances #-}
module Pi.Coxeter.Sn where
open import lib.Base
open import lib.Relation
open import lib.PathGroupoid
open import lib.Function
open import lib.Function2
open import lib.NType
open import lib.NType2
open import lib.types.SetQuotient public
open import lib.types.List
open import lib.types.Fin
open import lib.types.Truncation
open import lib.types.Sigma
open import Pi.Common.Extra
open import Pi.Coxeter.Coxeter
open import Pi.Common.Misc
Sn : (n : ℕ) → Type lzero
Sn n = SetQuot (_≈*_ {n})
instance
Sn-level : {n : ℕ} → is-set (Sn n)
Sn-level = SetQuot-is-set
private
list++-assoc-lemma : {n : ℕ} → (l₁ l₂ l₃ l₄ : List (Fin n)) → (l₁ ++ l₂) ++ (l₃ ++ l₄) == l₁ ++ (l₂ ++ l₃) ++ l₄
list++-assoc-lemma l₁ l₂ l₃ l₄ = (++-assoc l₁ l₂ (l₃ ++ l₄)) ∙ ap (λ e → l₁ ++ e) (! (++-assoc l₂ l₃ l₄))
idp≃ : {n : ℕ} → (l₁ l₂ : List (Fin n)) → (l₁ == l₂) → (l₁ ≈* l₂)
idp≃ l₁ l₂ p = transport (λ e → l₁ ≈* e) p idp
respects-++-lr : {n : ℕ} → (l m m' r : List (Fin (S n))) → (m ≈* m') → (l ++ (m ++ r)) ≈* (l ++ (m' ++ r))
respects-++-lr l m m' r p = respects-++ {l = l} {l' = l} idp (respects-++ p idp)
≈-inv-r : {n : ℕ} → (l : List (Fin n)) → (l ++ reverse l) ≈* nil
≈-inv-r {O} nil = idp
≈-inv-r {S n} nil = idp
≈-inv-r {S n} (x :: l) =
trans (idp≃ _ _ (list++-assoc-lemma (x :: nil) l (reverse l) (x :: nil)))
(trans (respects-++-lr (x :: nil) (l ++ reverse l) nil (x :: nil) (≈-inv-r l))
(≈-rel cancel))
≈-inv-l : {n : ℕ} → (l : List (Fin n)) → ((reverse l) ++ l) ≈* nil
≈-inv-l {O} nil = idp
≈-inv-l {S n} nil = idp
≈-inv-l {S n} (x :: l) =
trans (idp≃ _ _ (list++-assoc-lemma (reverse l) (x :: nil) (x :: nil) l))
(trans (respects-++-lr (reverse l) (x :: x :: nil) nil l (≈-rel cancel))
(≈-inv-l l))
reverse-respects-≈ : {n : ℕ} {l1 l2 : List (Fin n)} → l1 ≈* l2 → reverse l1 ≈* reverse l2
reverse-respects-≈ {O} {nil} {nil} p = p
reverse-respects-≈ {S n} (≈-rel cancel) = (≈-rel cancel)
reverse-respects-≈ {S n} (≈-rel (swap p)) = comm (≈-rel (swap p))
reverse-respects-≈ {S n} (≈-rel braid) = ≈-rel braid
reverse-respects-≈ {S n} idp = idp
reverse-respects-≈ {S n} (comm {l1 = l1} {l2 = l2} p) =
comm {l1 = reverse l1} {l2 = reverse l2} (reverse-respects-≈ p)
reverse-respects-≈ {S n} (trans {l1 = l1} {l2 = l2} {l3 = l3} p1 p2) =
let r1 = reverse-respects-≈ {l1 = l2} {l2 = l3} p2
r2 = reverse-respects-≈ {l1 = l1} {l2 = l2} p1
in trans {l1 = reverse l1} {l2 = reverse l2} {l3 = reverse l3} r2 r1
reverse-respects-≈ {S n} (respects-++ {l = l} {l' = l'} {r = r} {r' = r'} p1 p2) =
let r1 = reverse-respects-≈ p1
r2 = reverse-respects-≈ p2
s1 = reverse-++ l r
s2 = reverse-++ l' r'
in trans (idp≃ _ _ s1) (trans (respects-++ r2 r1) (idp≃ _ _ (! s2)))
::-respects-≈ : {n : ℕ} {x : Fin n} {l1 l2 : List (Fin n)} → l1 ≈* l2 → (x :: l1) ≈* (x :: l2)
::-respects-≈ {n = S n} p = respects-++ idp p