From 179740f30f8768ec60d3a3324084ef754a2cff2c Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 22 Oct 2025 01:20:25 -0500
Subject: Add symmetric monoidal structure to Push functor

---
 Data/Fin/Preimage.agda | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Data/Fin/Preimage.agda')

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
-- 
cgit v1.2.3