--- a/Symmetric.agda	Tue Aug 18 15:58:15 2020 +0900
+++ b/Symmetric.agda	Tue Aug 18 22:50:41 2020 +0900
@@ -119,20 +119,40 @@
        x<sn = <-trans a (s≤s m<n)
    p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
    p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
+
    p← : Fin (suc (suc n)) → Fin (suc (suc n))
-   p← x with <-cmp (toℕ x) (suc (suc n))
+   p← x with <-cmp (toℕ x) (suc n)
    p← x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn))  where
        x<sn : toℕ x < suc n
-       x<sn = <-trans a ?
+       x<sn = a
    p← x | tri≈ ¬a b ¬c = fromℕ≤ (s≤s (s≤s m<n))
-   p← x | tri> ¬a ¬b c = ⊥-elim ( nat-<> c fin<n )
+   p← x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c  fin<n )
+
    piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
    piso← x with <-cmp (toℕ x) m
    piso← x | tri< a ¬b ¬c = {!!}
-   piso← x | tri≈ ¬a b ¬c = {!!} where
-       lem4 : toℕ (fromℕ≤ (s≤s a<sa)) ≡ m → fromℕ≤ {!!} ≡ x 
-       lem4 = {!!}
+   piso← x | tri≈ ¬a refl ¬c = begin
+          p← ( fromℕ≤ a<sa )
+       ≡⟨ {!!}  ⟩
+          fromℕ≤ (s≤s (s≤s m<n))
+       ≡⟨ {!!}  ⟩
+          x
+       ∎  where
+            open ≡-Reasoning
+            lem4 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ {suc n} a<sa  → p← x ≡ fromℕ≤ (s≤s (s≤s m<n))
+            lem4 {x} refl with <-cmp (toℕ x) (suc n)
+            lem4  refl | tri< a ¬b ¬c = {!!}
+            lem4  refl | tri≈ ¬a b ¬c = {!!}
+            lem4  refl | tri> ¬a ¬b c = {!!}
    piso← x | tri> ¬a ¬b c = {!!}
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-   piso→ = {!!}
+   piso→ x with <-cmp (toℕ x) (suc n)
+   piso→ x | tri< a ¬b ¬c = {!!}
+   piso→ x | tri≈ ¬a b ¬c = begin
+          {!!} -- fromℕ≤ (s≤s (s≤s m<n))
+       ≡⟨ {!!}  ⟩
+          x
+       ∎  where
+            open ≡-Reasoning
+   piso→ x | tri> ¬a ¬b c = {!!}