From 96f21a2adca8bd54a45f9d9f9a82271007fa236a Mon Sep 17 00:00:00 2001 From: Andreas Nuyts Date: Mon, 21 Oct 2024 15:22:37 +0200 Subject: [PATCH] Fix whitespace crime --- Cubical/Categories/Constructions/BinProduct.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Categories/Constructions/BinProduct.agda b/Cubical/Categories/Constructions/BinProduct.agda index d2e424c74..1b9c87aa6 100644 --- a/Cubical/Categories/Constructions/BinProduct.agda +++ b/Cubical/Categories/Constructions/BinProduct.agda @@ -109,7 +109,7 @@ module _ (C : Category ℓC ℓC') CatIso× f g .snd .inv = f .snd .inv , g .snd .inv CatIso× f g .snd .sec i = f .snd .sec i , g .snd .sec i CatIso× f g .snd .ret i = f .snd .ret i , g .snd .ret i - + Sym : {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} → Functor (C ×C D) (D ×C C) Sym {C = C}{D = D} = Snd C D ,F Fst C D {-# WARNING_ON_USAGE Sym "DEPRECATED: Use `×C-sym` instead of `Sym`" #-}