We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 3376274 commit b91f273Copy full SHA for b91f273
Cubical/Categories/NaturalTransformation/Base.agda
@@ -116,7 +116,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
116
-- vertical sequencing
117
seqTrans : {F G H : Functor C D} (α : NatTrans F G) (β : NatTrans G H) → NatTrans F H
118
seqTrans α β .N-ob x = (α .N-ob x) ⋆ᴰ (β .N-ob x)
119
- seqTrans α β .N-hom f = compSq D (α .N-hom f) (β .N-hom f)
+ seqTrans α β .N-hom f = compSq D (α .N-hom f) (β .N-hom f)
120
121
compTrans : {F G H : Functor C D} (β : NatTrans G H) (α : NatTrans F G) → NatTrans F H
122
compTrans β α = seqTrans α β
0 commit comments