fix line lengths (#44)

maxsnew · Jul 22, 2023 · eb0ce0a · eb0ce0a
1 parent 20158c2
commit eb0ce0a
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 14 deletions.
diff --git a/Cubical/Categories/Constructions/Free/Category/Quiver.agda b/Cubical/Categories/Constructions/Free/Category/Quiver.agda
@@ -57,7 +57,8 @@ module _ (Q : Quiver ℓg ℓg') where
 
   -- A displayed interpretation
   open Categoryᴰ
-  record Interpᴰ (𝓓 : Categoryᴰ FreeCat ℓd ℓd') : Type ((ℓ-max (ℓ-max ℓg ℓg') (ℓ-max ℓd ℓd'))) where
+  record Interpᴰ (𝓓 : Categoryᴰ FreeCat ℓd ℓd')
+    : Type ((ℓ-max (ℓ-max ℓg ℓg') (ℓ-max ℓd ℓd'))) where
     field
       I-ob : (c : Q .ob) → ob[_] 𝓓 c
       I-hom : ∀ e → 𝓓 [ ↑ e ][ I-ob (Q .dom e) , I-ob (Q .cod e) ]
@@ -69,14 +70,16 @@ module _ (Q : Quiver ℓg ℓg') where
     private
       module 𝓓 = Categoryᴰ 𝓓
 
-    elimF : ∀ {c c'} (f : FreeCat [ c , c' ]) → 𝓓 [ f ][ ı .I-ob c , ı .I-ob c' ]
+    elimF : ∀ {c c'} (f : FreeCat [ c , c' ])
+          → 𝓓 [ f ][ ı .I-ob c , ı .I-ob c' ]
     elimF (↑ e) = ı .I-hom e
     elimF idₑ = 𝓓 .idᴰ
     elimF (f ⋆ₑ g) = elimF f 𝓓.⋆ᴰ elimF g
     elimF (⋆ₑIdL f i) = 𝓓 .⋆IdLᴰ (elimF f) i
     elimF (⋆ₑIdR f i) = 𝓓 .⋆IdRᴰ (elimF f) i
     elimF (⋆ₑAssoc f f₁ f₂ i) = 𝓓 .⋆Assocᴰ (elimF f) (elimF f₁) (elimF f₂) i
-    elimF (isSetExp f g p q i j) = isOfHLevel→isOfHLevelDep 2 (λ x → 𝓓 .isSetHomᴰ)
+    elimF (isSetExp f g p q i j) =
+      isOfHLevel→isOfHLevelDep 2 (λ x → 𝓓 .isSetHomᴰ)
       (elimF f)
       (elimF g)
       (cong elimF p)
@@ -103,10 +106,11 @@ module _ (Q : Quiver ℓg ℓg') where
   rec ı = Iso.fun (SectionToWkIsoFunctor _ _) (elim ı)
 
   module _ {ℓc ℓc'} {𝓒 : Category ℓc ℓc'} (F G : Functor FreeCat 𝓒)
-           (agree-on-gen : Interpᴰ (Preorderᴰ→Catᴰ
-                                   (SecPath (weaken FreeCat 𝓒)
-                                            (Iso.inv (SectionToWkIsoFunctor _ _) F)
-                                            (Iso.inv (SectionToWkIsoFunctor _ _) G))))
+           (agree-on-gen :
+             Interpᴰ (Preorderᴰ→Catᴰ
+                     (SecPath (weaken FreeCat 𝓒)
+                     (Iso.inv (SectionToWkIsoFunctor _ _) F)
+                     (Iso.inv (SectionToWkIsoFunctor _ _) G))))
          where
     FreeCatFunctor≡ : F ≡ G
     FreeCatFunctor≡ = isoInvInjective (SectionToWkIsoFunctor _ _) F G

diff --git a/Cubical/Categories/Displayed/Section.agda b/Cubical/Categories/Displayed/Section.agda
@@ -37,7 +37,8 @@ module _ {C : Category ℓC ℓC'} (D : Categoryᴰ C ℓD ℓD') where
   open Section
   Section≡ : {F G : Section}
            → (h : ∀ c → F .F-ob c ≡ G .F-ob c)
-           → (∀ {c c'} (f : C [ c , c' ]) → PathP (λ i → D [ f ][ h c i , h c' i ]) (F .F-hom f) (G .F-hom f))
+           → (∀ {c c'} (f : C [ c , c' ])
+           → PathP (λ i → D [ f ][ h c i , h c' i ]) (F .F-hom f) (G .F-hom f))
            → F ≡ G
   Section≡ hOb hHom i .F-ob c = hOb c i
   Section≡ hOb hHom i .F-hom f = hHom f i
@@ -47,10 +48,11 @@ module _ {C : Category ℓC ℓC'} (D : Categoryᴰ C ℓD ℓD') where
     (G .F-id)
     i
   Section≡ {F = F}{G = G} hOb hHom i .F-seq f g =
-    isProp→PathP (λ j → D .isSetHomᴰ (hHom (f ⋆⟨ C ⟩ g) j) (hHom f j D.⋆ᴰ hHom g j))
-    (F .F-seq f g)
-    (G .F-seq f g)
-    i
+    isProp→PathP
+      (λ j → D .isSetHomᴰ (hHom (f ⋆⟨ C ⟩ g) j) (hHom f j D.⋆ᴰ hHom g j))
+      (F .F-seq f g)
+      (G .F-seq f g)
+      i
 
   SectionToFunctor : Section → Functor C (∫C D)
   SectionToFunctor F .F-ob x = x , F .F-ob x
@@ -88,14 +90,16 @@ open Preorder.Section
 module _ (C : Category ℓC ℓC') (P : Preorderᴰ C ℓD ℓD') where
   open Iso
   open Preorderᴰ
-  PreorderSectionIsoCatSection : Iso (Preorder.Section P) (Section (Preorderᴰ→Catᴰ P))
+  PreorderSectionIsoCatSection
+    : Iso (Preorder.Section P) (Section (Preorderᴰ→Catᴰ P))
   PreorderSectionIsoCatSection .fun F .F-ob = F .F-ob
   PreorderSectionIsoCatSection .fun F .F-hom = F .F-hom
   PreorderSectionIsoCatSection .fun F .F-id = P .isPropHomᴰ _ _
   PreorderSectionIsoCatSection .fun F .F-seq f g = P .isPropHomᴰ _ _
   PreorderSectionIsoCatSection .inv F .F-ob = F .F-ob
   PreorderSectionIsoCatSection .inv F .F-hom = F .F-hom
-  PreorderSectionIsoCatSection .rightInv b = Section≡ _ (λ c → refl) (λ f → refl)
+  PreorderSectionIsoCatSection .rightInv b =
+    Section≡ _ (λ c → refl) (λ f → refl)
   PreorderSectionIsoCatSection .leftInv a = refl
 
 module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where