# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574557694 -32400
# Node ID 08990387c9192fc1aec37c6d712cced7ce921373
# Parent  fb6237e9a98b5e528bf37717f2bfc212003ecdf0
...

diff -r fb6237e9a98b -r 08990387c919 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sat Nov 23 17:43:02 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 24 10:08:14 2019 +0900
@@ -387,26 +387,37 @@
     elm : A
     elm<n : toℕ (FiniteSet.F←Q fa elm ) < n
 
+open Fin-<
 fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (Fin-< n<m fa) {n}
 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
+   iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa)
+   c1 : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ))) ≡ n 
+   c1 = subst (λ k → toℕ k ≡ n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k ≡ n) (sym (toℕ-fromℕ≤ _ )) refl )
    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 = {!!}
+   f<n = subst ( λ k → k < suc n ) (sym c1) a<sa
+   ISO.A←B iso x with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
+   ISO.A←B iso x | tri< a ¬b ¬c = case2 record { elm = elm x ; elm<n = a }
+   ISO.A←B iso x | tri≈ ¬a b ¬c = case1 one
+   ISO.A←B iso x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
+   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 x)  = record { elm = elm x ; elm<n = Data.Nat.Properties.<-trans (elm<n x) a<sa }
+   ISO.iso← iso (case1 one) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm (ISO.B←A iso (case1 one))))) n
+   ISO.iso← iso (case1 one) | tri< a ¬b ¬c = ⊥-elim ( ¬b c1 )
+   ISO.iso← iso (case1 one) | tri≈ ¬a b ¬c = refl
+   ISO.iso← iso (case1 one) | tri> ¬a ¬b c = ⊥-elim ( ¬b c1 )
+   ISO.iso← iso (case2 x) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x))) n
+   ISO.iso← iso (case2 x) | tri< a ¬b ¬c = cong ( λ k → case2 record { elm = elm x ; elm<n = k } ) (lemma1 _ _) where
+     lemma1 : {m n : ℕ } → ( i j : m < n ) → i ≡ j
+     lemma1 {zero} {suc n} (s≤s z≤n) (s≤s z≤n) = refl
+     lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j )
+   ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) )
+   ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) )
+   ISO.iso→ iso x with ISO.A←B iso x 
+   ISO.iso→ iso x | case1 one = ?
+   ISO.iso→ iso x | case2 x1 = {!!}
 
 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