We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 21a8e37 commit d318ebfCopy full SHA for d318ebf
Cubical/Categories/Category/Path.agda
@@ -84,7 +84,7 @@ module _ {C C' : Category ℓ ℓ'} where
84
private
85
cp = ≡→CategoryPath b
86
b' = CategoryPath.mk≡ cp
87
-
+
88
CategoryPathIsoRightInv : mk≡ (≡→CategoryPath b) ≡ b
89
CategoryPathIsoRightInv i j .ob = b j .ob
90
CategoryPathIsoRightInv i j .Hom[_,_] = b j .Hom[_,_]
0 commit comments