diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-22 01:20:25 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-22 01:20:25 -0500 |
| commit | 179740f30f8768ec60d3a3324084ef754a2cff2c (patch) | |
| tree | ef2cd5f49c2d2e567dd79c14f19d0644e5cdc887 /Data/Fin | |
| parent | e5b3cd06b1ba2504831db203a6be30c184df3274 (diff) | |
Add symmetric monoidal structure to Push functor
Diffstat (limited to 'Data/Fin')
| -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 |