Skipping elements in standard finite types
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-03-14.
Last modified on 2024-04-11.
module univalent-combinatorics.skipping-element-standard-finite-types where
Imports
open import elementary-number-theory.natural-numbers open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equality-coproduct-types open import foundation.identity-types open import foundation.injective-maps open import foundation.sets open import foundation.unit-type open import univalent-combinatorics.standard-finite-types
skip-Fin : (k : ℕ) → Fin (succ-ℕ k) → Fin k → Fin (succ-ℕ k) skip-Fin (succ-ℕ k) (inl x) (inl y) = inl (skip-Fin k x y) skip-Fin (succ-ℕ k) (inl x) (inr y) = inr star skip-Fin (succ-ℕ k) (inr x) y = inl y abstract is-injective-skip-Fin : (k : ℕ) (x : Fin (succ-ℕ k)) → is-injective (skip-Fin k x) is-injective-skip-Fin (succ-ℕ k) (inl x) {inl y} {inl z} p = ap ( inl) ( is-injective-skip-Fin k x ( is-injective-is-emb (is-emb-inl (Fin (succ-ℕ k)) unit) p)) is-injective-skip-Fin (succ-ℕ k) (inl x) {inr star} {inr star} p = refl is-injective-skip-Fin (succ-ℕ k) (inr star) {y} {z} p = is-injective-is-emb (is-emb-inl (Fin (succ-ℕ k)) unit) p abstract is-emb-skip-Fin : (k : ℕ) (x : Fin (succ-ℕ k)) → is-emb (skip-Fin k x) is-emb-skip-Fin k x = is-emb-is-injective ( is-set-Fin (succ-ℕ k)) ( is-injective-skip-Fin k x) emb-skip-Fin : (k : ℕ) (x : Fin (succ-ℕ k)) → Fin k ↪ Fin (succ-ℕ k) pr1 (emb-skip-Fin k x) = skip-Fin k x pr2 (emb-skip-Fin k x) = is-emb-skip-Fin k x
Recent changes
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).