We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent a82cb33 commit 87678c8Copy full SHA for 87678c8
Cubical/Categories/Dagger/Instances/BinProduct.agda
@@ -66,7 +66,6 @@ module _ (C : DagCat ℓ ℓ') (D : DagCat ℓ'' ℓ''') where
66
†Rinj c = †Const c ,†F †Id
67
68
open areInv
69
-
70
†CatIso× : ∀ {x y z w} → †CatIso C x y → †CatIso D z w → †CatIso (C ×D D) (x , z) (y , w)
71
†CatIso× (f , fiso) (g , giso) .fst = f , g
72
†CatIso× (f , fiso) (g , giso) .snd .sec = ≡-× (fiso .sec) (giso .sec)
0 commit comments