diff --git a/Cubical.Data.Fin.Recursive.Base.html b/Cubical.Data.Fin.Recursive.Base.html index 4af1a72ccc..1e61418fec 100644 --- a/Cubical.Data.Fin.Recursive.Base.html +++ b/Cubical.Data.Fin.Recursive.Base.html @@ -33,4 +33,8 @@ → (fn : Fin k) → P fn elim {k = suc k} P fz fs zero = fz elim {k = suc k} P fz fs (suc x) = fs x (elim P fz fs x) + +toℕ : Fin k → ℕ +toℕ {suc k} zero = zero +toℕ {suc k} (suc n) = suc (toℕ n) \ No newline at end of file diff --git a/Cubical.Data.Fin.Recursive.Properties.html b/Cubical.Data.Fin.Recursive.Properties.html index 9d0c937736..ec90de524a 100644 --- a/Cubical.Data.Fin.Recursive.Properties.html +++ b/Cubical.Data.Fin.Recursive.Properties.html @@ -180,89 +180,93 @@ toFin zero = zero toFin (suc n) = suc (toFin n) -inject<#toFin : ∀(i : Fin n) → inject< (≤-refl (suc n)) i # toFin n -inject<#toFin {suc n} zero = _ -inject<#toFin {suc n} (suc i) = inject<#toFin {n} i - -inject≤#⊕ : ∀(i : Fin m) (j : Fin n) → inject≤ (k≤k+n m) i # (m ⊕ j) -inject≤#⊕ {suc m} {suc n} zero j = _ -inject≤#⊕ {suc m} {suc n} (suc i) j = inject≤#⊕ i j - -split : (m : ℕ) → Fin (m + n) → Fin m ⊎ Fin n -split zero j = inr j -split (suc m) zero = inl zero -split (suc m) (suc i) with split m i -... | inl k = inl (suc k) -... | inr j = inr j - -pigeonhole - : m < n - → (f : Fin n → Fin m) - → Σ[ i ∈ Fin n ] Σ[ j ∈ Fin n ] (i # j) × (f i ≡ f j) -pigeonhole {zero} {suc n} m<n f = Empty.rec (f zero) -pigeonhole {suc m} {suc n} m<n f with any? (λ i → discreteFin (f zero) (f (suc i))) -... | yes (j , p) = zero , suc j , _ , p -... | no ¬p = let i , j , ap , p = pigeonhole {m} {n} m<n g - in suc i , suc j , ap - , punchOut-inj {i = f zero} (apart i) (apart j) p - where - apart : (i : Fin n) → f zero # f (suc i) - apart i = ≢→# {suc m} {f zero} (¬p ∘ _,_ i) - - g : Fin n → Fin m - g i = punchOut (f zero) (f (suc i)) (apart i) - -Fin-inj₀ : m < n → ¬ Fin n ≡ Fin m -Fin-inj₀ m<n P with pigeonhole m<n (transport P) -... | i , j , i#j , p = #→≢ i#j i≡j - where - i≡j : i ≡ j - i≡j = transport (λ k → transport⁻Transport P i k ≡ transport⁻Transport P j k) - (cong (transport⁻ P) p) - -Fin-inj : (m n : ℕ) → Fin m ≡ Fin n → m ≡ n -Fin-inj m n P with m ≟ n -... | eq p = p -... | lt m<n = Empty.rec (Fin-inj₀ m<n (sym P)) -... | gt n<m = Empty.rec (Fin-inj₀ n<m P) - -module Isos where - open Iso - - up : Fin m → Fin (m + n) - up {m} = inject≤ (k≤k+n m) - - resplit-identᵣ₀ : ∀ m (i : Fin n) → Sum.⊎Path.Cover (split m (m ⊕ i)) (inr i) - resplit-identᵣ₀ zero i = lift refl - resplit-identᵣ₀ (suc m) i with split m (m ⊕ i) | resplit-identᵣ₀ m i - ... | inr j | p = p - - resplit-identᵣ : ∀ m (i : Fin n) → split m (m ⊕ i) ≡ inr i - resplit-identᵣ m i = Sum.⊎Path.decode _ _ (resplit-identᵣ₀ m i) - - resplit-identₗ₀ : ∀ m (i : Fin m) → Sum.⊎Path.Cover (split {n} m (up i)) (inl i) - resplit-identₗ₀ (suc m) zero = lift refl - resplit-identₗ₀ {n} (suc m) (suc i) - with split {n} m (up i) | resplit-identₗ₀ {n} m i - ... | inl j | lift p = lift (cong suc p) - - resplit-identₗ : ∀ m (i : Fin m) → split {n} m (up i) ≡ inl i - resplit-identₗ m i = Sum.⊎Path.decode _ _ (resplit-identₗ₀ m i) - - desplit-ident : ∀ m → (i : Fin (m + n)) → Sum.rec up (m ⊕_) (split m i) ≡ i - desplit-ident zero i = refl - desplit-ident (suc m) zero = refl - desplit-ident (suc m) (suc i) with split m i | desplit-ident m i - ... | inl j | p = cong suc p - ... | inr j | p = cong suc p - - sumIso : Iso (Fin m ⊎ Fin n) (Fin (m + n)) - sumIso {m} .fun = Sum.rec up (m ⊕_) - sumIso {m} .inv i = split m i - sumIso {m} .rightInv i = desplit-ident m i - sumIso {m} .leftInv (inr j) = resplit-identᵣ m j - sumIso {m} .leftInv (inl i) = resplit-identₗ m i - -sum≡ : Fin m ⊎ Fin n ≡ Fin (m + n) -sum≡ = isoToPath Isos.sumIso +toFin< : (m : ℕ) → m < n → Fin n +toFin< {suc n} zero 0<sn = zero +toFin< {suc n} (suc m) m<n = suc (toFin< m m<n) + +inject<#toFin : ∀(i : Fin n) → inject< (≤-refl (suc n)) i # toFin n +inject<#toFin {suc n} zero = _ +inject<#toFin {suc n} (suc i) = inject<#toFin {n} i + +inject≤#⊕ : ∀(i : Fin m) (j : Fin n) → inject≤ (k≤k+n m) i # (m ⊕ j) +inject≤#⊕ {suc m} {suc n} zero j = _ +inject≤#⊕ {suc m} {suc n} (suc i) j = inject≤#⊕ i j + +split : (m : ℕ) → Fin (m + n) → Fin m ⊎ Fin n +split zero j = inr j +split (suc m) zero = inl zero +split (suc m) (suc i) with split m i +... | inl k = inl (suc k) +... | inr j = inr j + +pigeonhole + : m < n + → (f : Fin n → Fin m) + → Σ[ i ∈ Fin n ] Σ[ j ∈ Fin n ] (i # j) × (f i ≡ f j) +pigeonhole {zero} {suc n} m<n f = Empty.rec (f zero) +pigeonhole {suc m} {suc n} m<n f with any? (λ i → discreteFin (f zero) (f (suc i))) +... | yes (j , p) = zero , suc j , _ , p +... | no ¬p = let i , j , ap , p = pigeonhole {m} {n} m<n g + in suc i , suc j , ap + , punchOut-inj {i = f zero} (apart i) (apart j) p + where + apart : (i : Fin n) → f zero # f (suc i) + apart i = ≢→# {suc m} {f zero} (¬p ∘ _,_ i) + + g : Fin n → Fin m + g i = punchOut (f zero) (f (suc i)) (apart i) + +Fin-inj₀ : m < n → ¬ Fin n ≡ Fin m +Fin-inj₀ m<n P with pigeonhole m<n (transport P) +... | i , j , i#j , p = #→≢ i#j i≡j + where + i≡j : i ≡ j + i≡j = transport (λ k → transport⁻Transport P i k ≡ transport⁻Transport P j k) + (cong (transport⁻ P) p) + +Fin-inj : (m n : ℕ) → Fin m ≡ Fin n → m ≡ n +Fin-inj m n P with m ≟ n +... | eq p = p +... | lt m<n = Empty.rec (Fin-inj₀ m<n (sym P)) +... | gt n<m = Empty.rec (Fin-inj₀ n<m P) + +module Isos where + open Iso + + up : Fin m → Fin (m + n) + up {m} = inject≤ (k≤k+n m) + + resplit-identᵣ₀ : ∀ m (i : Fin n) → Sum.⊎Path.Cover (split m (m ⊕ i)) (inr i) + resplit-identᵣ₀ zero i = lift refl + resplit-identᵣ₀ (suc m) i with split m (m ⊕ i) | resplit-identᵣ₀ m i + ... | inr j | p = p + + resplit-identᵣ : ∀ m (i : Fin n) → split m (m ⊕ i) ≡ inr i + resplit-identᵣ m i = Sum.⊎Path.decode _ _ (resplit-identᵣ₀ m i) + + resplit-identₗ₀ : ∀ m (i : Fin m) → Sum.⊎Path.Cover (split {n} m (up i)) (inl i) + resplit-identₗ₀ (suc m) zero = lift refl + resplit-identₗ₀ {n} (suc m) (suc i) + with split {n} m (up i) | resplit-identₗ₀ {n} m i + ... | inl j | lift p = lift (cong suc p) + + resplit-identₗ : ∀ m (i : Fin m) → split {n} m (up i) ≡ inl i + resplit-identₗ m i = Sum.⊎Path.decode _ _ (resplit-identₗ₀ m i) + + desplit-ident : ∀ m → (i : Fin (m + n)) → Sum.rec up (m ⊕_) (split m i) ≡ i + desplit-ident zero i = refl + desplit-ident (suc m) zero = refl + desplit-ident (suc m) (suc i) with split m i | desplit-ident m i + ... | inl j | p = cong suc p + ... | inr j | p = cong suc p + + sumIso : Iso (Fin m ⊎ Fin n) (Fin (m + n)) + sumIso {m} .fun = Sum.rec up (m ⊕_) + sumIso {m} .inv i = split m i + sumIso {m} .rightInv i = desplit-ident m i + sumIso {m} .leftInv (inr j) = resplit-identᵣ m j + sumIso {m} .leftInv (inl i) = resplit-identₗ m i + +sum≡ : Fin m ⊎ Fin n ≡ Fin (m + n) +sum≡ = isoToPath Isos.sumIso \ No newline at end of file