# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574577637 -32400
# Node ID 2d70f90565c63111877ecee1be4eab642f8cd168
# Parent  14cf0e1c8d91b952118bc258af91b8a972ae07e1
...

diff -r 14cf0e1c8d91 -r 2d70f90565c6 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sun Nov 24 14:52:20 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 24 15:40:37 2019 +0900
@@ -382,6 +382,38 @@
 
 open import Data.Product
 
+Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) {n}
+Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
+
+data f-1 { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
+  elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → f-1 n<m fa
+
+-- f-1-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
+--    → ( elm s ≡ elm t) → ( elm<n s ≅ elm<n t ) → elm1 e0 e0<n ≡ elm1 e1 e1<n
+-- f-1-<-cong n<m fa _ _ refl HE.refl = refl
+
+fin-<' : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (f-1 n<m fa) {n}
+fin-<' {A} {n} {m} n<m fa  = iso-fin (Fin2Finite n) iso where
+    iso : ISO (Fin n) (f-1 n<m fa)
+    ISO.A←B iso (elm1 elm x) = fromℕ≤ x
+    ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m ))) to<n where
+        x<n : toℕ x < n
+        x<n = toℕ<n x
+        to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m)))) < n
+        to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m) )) x<n )
+    ISO.iso← iso x  = lemma2 where
+        lemma2 : fromℕ≤ (subst (λ k → toℕ k < n) (sym
+          (FiniteSet.finiso← fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
+          (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
+        lemma2 = {!!}
+    ISO.iso→ iso (elm1 elm x) = lemma1 where
+        lemma : FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm 
+        lemma = {!!}
+        lemma1 : ISO.B←A iso (ISO.A←B iso (elm1 elm x)) ≡ elm1 elm x
+        lemma1 with lemma
+        ... | eq = {!!}
+
+
 record Fin-< { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) : Set where
   field 
     elm : A