Skip to content

Commit

Permalink
Fix whitespace crime
Browse files Browse the repository at this point in the history
  • Loading branch information
anuyts committed Oct 21, 2024
1 parent 6941f15 commit 96f21a2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Cubical/Categories/Constructions/BinProduct.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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`" #-}

0 comments on commit 96f21a2

Please sign in to comment.