Mercurial > hg > Members > kono > Proof > galois

changeset 25:fab3609ac3f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Aug 2020 09:29:06 +0900
parents 882ee60695c5
children fb9dcee4ed86
files Symmetric.agda
diffstat 1 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 09:14:29 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 09:29:06 2020 +0900
@@ -94,15 +94,15 @@
    p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
    p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
 
-   pincl :  (Fin (suc (suc n)) → Fin (suc (suc n)))
-       ∧ (( p←i : Fin (suc (suc n)) → Fin (suc (suc n))) →  (x : Fin (suc (suc n)) ) → p←i (p→ x)   ≡ x )
-       ∧ (( p←i : Fin (suc (suc n)) → Fin (suc (suc n))) →  (x : Fin (suc (suc n)) ) → p→ (p←i x)   ≡ x )
+   pincl : ((x  : Fin (suc (suc n))) → Fin (suc (suc n)))
+       ∧ (( p←i : Fin (suc (suc n))  → Fin (suc (suc n))) →  (x y : Fin (suc (suc n)) ) → p→ y ≡ x  → p←i (p→ y)   ≡ y )
+       ∧ (( p←i : Fin (suc (suc n))  → Fin (suc (suc n))) →  (x : Fin (suc (suc n)) )               → p→ (p←i x)   ≡ x )
    pincl = {!!}
 
    open _∧_
    p← : Fin (suc (suc n)) → Fin (suc (suc n))
    p← = proj1 pincl
    piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
-   piso← = proj1 (proj2 pincl) p←
+   piso← x = proj1 (proj2 pincl) p← (p→ x) x refl
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
    piso→ = proj2 (proj2 pincl) p←