Skip to content

Commit

Permalink
tinny chagne to trigger CI
Browse files Browse the repository at this point in the history
  • Loading branch information
marcinjangrzybowski committed Oct 25, 2023
1 parent a14f79c commit 06b977a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Cubical/Categories/Adjoint.agda
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ module AdjointUniqeUpToNatIso where
∙∙ cong (H' ⟪ _ ⟫ D⋆_)
(sym (⋆Assoc D _ _ _)
∙ cong (_D⋆ ε ⟦ _ ⟧)
( sym (F-seq H' _ _)
( sym (F-seq H' _ _)
∙∙ cong (H' ⟪_⟫) (Δ₂ (H' ⟅ _ ⟆))
∙∙ F-id H')
∙ ⋆IdL D _)
Expand Down

0 comments on commit 06b977a

Please sign in to comment.