# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574487552 -32400
# Node ID 5275a0163b1dee12648a21484f520355e29bd599
# Parent  0e8a0e50ed26ca9a78e486163b5a6b122ea18971
..

diff -r 0e8a0e50ed26 -r 5275a0163b1d agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sat Nov 23 12:59:45 2019 +0900
+++ b/agda/finiteSet.agda	Sat Nov 23 14:39:12 2019 +0900
@@ -382,6 +382,37 @@
 
 open import Data.Product
 
+record Fin-< { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) : Set where
+  field 
+    elm : A
+    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 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
 ... | a=f = iso-fin (fin-×-f a ) iso-1 where