diff options
Diffstat (limited to 'Data/Fin/Preimage.agda')
| -rw-r--r-- | Data/Fin/Preimage.agda | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Data/Fin/Preimage.agda b/Data/Fin/Preimage.agda index f6e4373..4f7ea43 100644 --- a/Data/Fin/Preimage.agda +++ b/Data/Fin/Preimage.agda @@ -40,3 +40,9 @@ preimage-∘ (z : Fin C) → preimage (g ∘ f) ⁅ z ⁆ ≗ preimage f (preimage g ⁅ z ⁆) preimage-∘ f g S x = ≡.refl + +preimage-⊥ + : {n m : ℕ} + (f : Fin n → Fin m) + → preimage f ⊥ ≗ ⊥ +preimage-⊥ f x = ≡.refl |