# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574498582 -32400
# Node ID fb6237e9a98b5e528bf37717f2bfc212003ecdf0
# Parent  5275a0163b1dee12648a21484f520355e29bd599
bad direction on fin-<

diff -r 5275a0163b1d -r fb6237e9a98b agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sat Nov 23 14:39:12 2019 +0900
+++ b/agda/finiteSet.agda	Sat Nov 23 17:43:02 2019 +0900
@@ -388,30 +388,25 @@
     elm<n : toℕ (FiniteSet.F←Q fa elm ) < n
 
 fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (Fin-< n<m fa) {n}
-fin-< {A} {n} {m} n<m fa = record {
-       F←Q = F←Q
-     ; Q←F = Q←F
-     ; finiso← = finiso←
-     ; finiso→ = finiso→
-   } where
-       F←Q : Fin-< n<m fa → Fin n
-       F←Q f = fromℕ≤ ( Fin-<.elm<n f )
-       Q←F : Fin n → Fin-< n<m fa
-       Q←F f = record { elm = FiniteSet.Q←F fa (fromℕ≤ f<m); elm<n = elm<n } where 
-             f<m : toℕ f < m
-             f<m = Data.Nat.Properties.<-trans (toℕ<n f ) n<m
-             elm<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ f<m))) < n
-             elm<n = subst (λ k → k < n ) (cong ( λ k → toℕ k ) (sym (FiniteSet.finiso← fa _ )))
-                 (subst (λ k → k < n ) (sym (toℕ-fromℕ≤ f<m)) (toℕ<n f) )
-       finiso← :  (f : Fin n) → F←Q (Q←F f) ≡ f
-       finiso← f = lemma where
-           lemma : fromℕ≤ (subst (λ k → suc k ≤ n)
-                 (cong toℕ (sym (FiniteSet.finiso← fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n f) n<m)))))
-                 (subst (λ k → suc k ≤ n) (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n f) n<m))) (toℕ<n f))) ≡ f
-           lemma  = {!!}
-       finiso→ : (q : Fin-< n<m fa) → Q←F (F←Q q) ≡ q
-       finiso→ q = {!!}
-
+fin-< {A} {zero} {m} (s≤s z≤n) fa  = record { Q←F = λ () ; F←Q = λ () ; finiso← = λ () ; finiso→ = λ ()  }
+fin-< {A} {suc n} {m} (s≤s n<m) fa = iso-fin (fin-∨1 (fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa)) iso where
+   fin- : FiniteSet (Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa)
+   fin- = fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa
+   f<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) < suc n
+   f<n = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ≤ _ )) a<sa)
+   iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa)
+   ISO.A←B iso x with fromℕ≤ (Fin-<.elm<n x )
+   ISO.A←B iso x | zero = case1 one
+   ISO.A←B iso x | suc f = case2 ( FiniteSet.Q←F fin- f ) 
+   ISO.B←A iso (case1 one) = record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) ; elm<n = f<n }
+   ISO.B←A iso (case2 record { elm = elm ; elm<n = elm<n }) = record { elm = elm ; elm<n = Data.Nat.Properties.<-trans elm<n a<sa }
+   ISO.iso← iso (case1 one) with fromℕ≤ f<n
+   ISO.iso← iso (case1 one) | zero = refl
+   ISO.iso← iso (case1 one) | suc t = {!!}
+   ISO.iso← iso (case2 x) = {!!}
+   ISO.iso→ iso x with fromℕ≤ (Fin-<.elm<n x )
+   ISO.iso→ iso x | zero = {!!}
+   ISO.iso→ iso x | suc f = {!!}
 
 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
 fin-× {A} {B} {a} {b} fa fb with FiniteSet→Fin fa