From 06b977a52f3ee7ce123a62fb884b788a841cd4f6 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Wed, 25 Oct 2023 18:57:42 +0200 Subject: [PATCH] tinny chagne to trigger CI --- Cubical/Categories/Adjoint.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda index 5d6c102ac3..788b8d30e2 100644 --- a/Cubical/Categories/Adjoint.agda +++ b/Cubical/Categories/Adjoint.agda @@ -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 _)