Mercurial > hg > Members > kono > Proof > galois

changeset 23:b133ef55b395

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 08:50:17 +0900
parents ae586c068d01
children 882ee60695c5
files Symmetric.agda
diffstat 1 files changed, 15 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 02:02:17 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 08:50:17 2020 +0900
@@ -113,7 +113,7 @@
 record Pincl (i j : ℕ ) (p→i : Fin (suc (suc j)) → Fin (suc (suc j))) : Set (Level.suc Level.zero ) where
    field
      p←i     : (x : Fin (suc (suc j)) )    → (i≤x : toℕ x < i )       → Fin (suc (suc j))
-     piso←i  : ( x : Fin (suc (suc j)) ) → (i≤x : toℕ (p→i x) < i ) → p←i (p→i x) i≤x   ≡ x
+     piso←i  : ( x : Fin (suc (suc j)) )   → (i≤x : toℕ (p→i x) < i ) → p←i (p→i x) i≤x   ≡ x
      piso→i  : ( x : Fin (suc (suc j)) )   → (i≤x : toℕ x < i )       → p→i ( p←i x i≤x ) ≡ x
       
 
@@ -129,13 +129,22 @@
    p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
 
    pincl : Pincl (suc (suc n)) n p→ 
-   pincl = pincl1 (suc (suc n)) {!!}  where
-     pincl1 : (i : ℕ ) → i < suc n  → Pincl i n p→ 
-     pincl1 0 _  = {!!}
-     pincl1 (suc i) i<n  = {!!}
+   pincl = pincl1 (suc (suc n)) where
+     pincl1 : (i : ℕ ) → Pincl i n p→ 
+     pincl1 0  = record { p←i = λ x () ; piso←i = λ x () ; piso→i = λ x () }
+     pincl1 (suc i) = pincl2 (fromℕ≤ a<sa ) where
+         pincl2 : (y : Fin (suc (suc n))) → Pincl (suc i) n p→
+         pincl2 zero = {!!}
+         pincl2 (suc y) = {!!}
+         
+     -- with pincl1 i 
+     -- ... | p = record { p←i = λ x i<x → p1 x i<x  ; piso←i = λ x i<x →  {!!} ; piso→i = λ x i<x → {!!} } where
+     --     j = n
+     --     p1 :  (x : Fin (suc (suc j)) )    → (i≤x : toℕ x < suc i )       → Fin (suc (suc j))
+     --     p1 x i≤x = {!!}
 
    p← : Fin (suc (suc n)) → Fin (suc (suc n))
-   p← x = Pincl.p←i pincl x {!!}
+   p← x = Pincl.p←i pincl x fin<n
    piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
    piso← x = Pincl.piso←i pincl  x fin<n
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x