We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 251aa71 commit ee66405Copy full SHA for ee66405
Cubical/Categories/Dagger/Instances/BinProduct.agda
@@ -70,4 +70,4 @@ module _ (C : DagCat ℓ ℓ') (D : DagCat ℓ'' ℓ''') where
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)
73
- †CatIso× (f , fiso) (g , giso) .snd .ret = ≡-× (fiso .ret) (giso .ret)
+ †CatIso× (f , fiso) (g , giso) .snd .ret = ≡-× (fiso .ret) (giso .ret)
0 commit comments