line lenghts

maxsnew · Sep 20, 2024 · 92e12d5 · 92e12d5
1 parent d031d10
commit 92e12d5
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/Cubical/Categories/Displayed/Limits/BinProduct.agda b/Cubical/Categories/Displayed/Limits/BinProduct.agda
@@ -264,7 +264,8 @@ module _ {C : Category ℓC ℓC'}{c c' : C .ob}
             q₁'' = fᴰ* .snd
               (R.reind (C .⋆IdR h) (hᴰ' Cᴰ.⋆ᴰ ϕ[π₁x]∧ψ[π₂x].π₁) , q₁''')
             q₁' : fᴰ* .fst .fst Cᴰ.≡[ _ ] hᴰ' Cᴰ.⋆ᴰ ϕ[π₁x]∧ψ[π₂x].π₁
-            q₁' = R.≡out (R.≡in (congP (λ _ → fst) q₁'') ∙ sym (R.reind-filler _ _))
+            q₁' =
+              R.≡out (R.≡in (congP (λ _ → fst) q₁'') ∙ sym (R.reind-filler _ _))
             q₁ : fᴰ* .fst .fst Cᴰ.⋆ᴰ Cᴰ.idᴰ ≡ hᴰ' Cᴰ.⋆ᴰ ϕ[π₁x]∧ψ[π₂x].π₁
             q₁ = R.rectify (R.≡out (R.⋆IdR _ ∙ R.≡in q₁'))
 
@@ -281,7 +282,8 @@ module _ {C : Category ℓC ℓC'}{c c' : C .ob}
             q₂'' = gᴰ* .snd
               (R.reind (C .⋆IdR h) (hᴰ' Cᴰ.⋆ᴰ ϕ[π₁x]∧ψ[π₂x].π₂) , q₂''')
             q₂' : gᴰ* .fst .fst Cᴰ.≡[ _ ] hᴰ' Cᴰ.⋆ᴰ ϕ[π₁x]∧ψ[π₂x].π₂
-            q₂' = R.≡out (R.≡in (congP (λ _ → fst) q₂'') ∙ sym (R.reind-filler _ _))
+            q₂' =
+              R.≡out (R.≡in (congP (λ _ → fst) q₂'') ∙ sym (R.reind-filler _ _))
             q₂ : gᴰ* .fst .fst Cᴰ.⋆ᴰ Cᴰ.idᴰ ≡ hᴰ' Cᴰ.⋆ᴰ ϕ[π₁x]∧ψ[π₂x].π₂
             q₂ = R.rectify (R.≡out (R.⋆IdR _ ∙ R.≡in q₂'))