Merge pull request #465 from agda/agda-2.8.0

agda 2.8.0 compatibility (useless 'private' and some trailing whitespace cleanup at the same time.)

Author: JacquesCarette

src/Categories/Adjoint/AFT.agda

@@ -74,7 +74,7 @@ module _ {R : Functor C D} where
         X↙R = X ↙ R
         module X↙R = Category X↙R
 
-        s′ : SolutionSet X↙R 
+        s′ : SolutionSet X↙R
         s′ = record
           { D   = D′
           ; arr = arr′

src/Categories/Adjoint/Alternatives.agda

@@ -24,22 +24,22 @@ private
       module R = Functor R
 
     record FromUnit : Set (levelOfTerm L ⊔ levelOfTerm R) where
-  
+
       field
         unit : NaturalTransformation idF (R ∘F L)
-  
+
       module unit = NaturalTransformation unit
-  
+
       field
         θ       : ∀ {X Y} → C [ X , R.₀ Y ] → D [ L.₀ X , Y ]
         commute : ∀ {X Y} (g : C [ X , R.₀ Y ]) → g C.≈ R.₁ (θ g) C.∘ unit.η X
         unique  : ∀ {X Y} {f : D [ L.₀ X , Y ]} {g : C [ X , R.₀ Y ]} →
                     g C.≈ R.₁ f C.∘ unit.η X → θ g D.≈ f
-  
+
       module _ where
         open C.HomReasoning
         open MR C
-  
+
         θ-natural : ∀ {X Y Z} (f : D [ Y , Z ]) (g : C [ X , R.₀ Y ]) → θ (R.₁ f C.∘ g) D.≈ θ (R.₁ f) D.∘ L.₁ g
         θ-natural {X} {Y} f g = unique eq
           where eq : R.₁ f C.∘ g C.≈ R.₁ (θ (R.₁ f) D.∘ L.₁ g) C.∘ unit.η X
@@ -49,15 +49,15 @@ private
                   R.₁ (θ (R.₁ f)) C.∘ unit.η (R.₀ Y) C.∘ g       ≈⟨ pushʳ (unit.commute g) ⟩
                   (R.₁ (θ (R.₁ f)) C.∘ R.₁ (L.₁ g)) C.∘ unit.η X ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩
                   R.₁ (θ (R.₁ f) D.∘ L.₁ g) C.∘ unit.η X         ∎
-    
+
         θ-cong : ∀ {X Y} {f g : C [ X , R.₀ Y ]} → f C.≈ g → θ f D.≈ θ g
         θ-cong eq = unique (eq ○ commute _)
-  
+
       θ-natural′ : ∀ {X Y} (g : C [ X , R.₀ Y ]) → θ g D.≈ θ C.id D.∘ L.₁ g
       θ-natural′ g = θ-cong (introˡ R.identity) ○ θ-natural D.id g ○ D.∘-resp-≈ˡ (θ-cong R.identity)
         where open D.HomReasoning
               open MR C
-  
+
       counit : NaturalTransformation (L ∘F R) idF
       counit = ntHelper record
         { η       = λ d → θ C.id
@@ -68,13 +68,13 @@ private
         }
         where open D.HomReasoning
               module CH = C.HomReasoning
-  
+
       unique′ : ∀ {X Y} {f g : D [ L.₀ X , Y ]} (h : C [ X , R.₀ Y ]) →
                   h C.≈ R.₁ f C.∘ unit.η X →
                   h C.≈ R.₁ g C.∘ unit.η X → f D.≈ g
       unique′ _ eq₁ eq₂ = ⟺ (unique eq₁) ○ unique eq₂
         where open D.HomReasoning
-  
+
       zig : ∀ {A} → θ C.id D.∘ L.F₁ (unit.η A) D.≈ D.id
       zig {A} = unique′ (unit.η A)
                         (commute (unit.η A) ○ (C.∘-resp-≈ˡ (R.F-resp-≈ (θ-natural′ (unit.η A)))))
@@ -91,12 +91,12 @@ private
         }
 
     record FromCounit : Set (levelOfTerm L ⊔ levelOfTerm R) where
-  
+
       field
         counit : NaturalTransformation (L ∘F R) idF
-  
+
       module counit = NaturalTransformation counit
-  
+
       field
         θ       : ∀ {X Y} → D [ L.₀ X , Y ] → C [ X , R.₀ Y ]
         commute : ∀ {X Y} (g : D [ L.₀ X , Y ]) → g D.≈ counit.η Y D.∘ L.₁ (θ g)
@@ -106,7 +106,7 @@ private
       module _ where
         open D.HomReasoning
         open MR D
-  
+
         θ-natural : ∀ {X Y Z} (f : C [ X , Y ]) (g : D [ L.₀ Y , Z ]) → θ (g D.∘ L.₁ f) C.≈ R.₁ g C.∘ θ (L.₁ f)
         θ-natural {X} {Y} {Z} f g = unique eq
           where eq : g D.∘ L.₁ f D.≈ counit.η Z D.∘ L.₁ (R.₁ g C.∘ θ (L.₁ f))
@@ -115,10 +115,10 @@ private
                   (g D.∘ counit.η (L.F₀ Y)) D.∘ L.F₁ (θ (L.F₁ f)) ≈⟨ pushˡ (counit.sym-commute g) ⟩
                   counit.η Z D.∘ L.₁ (R.₁ g) D.∘ L.₁ (θ (L.₁ f))  ≈˘⟨ refl⟩∘⟨ L.homomorphism ⟩
                   counit.η Z D.∘ L.₁ (R.₁ g C.∘ θ (L.₁ f))        ∎
-    
+
         θ-cong : ∀ {X Y} {f g : D [ L.₀ X , Y ]} → f D.≈ g → θ f C.≈ θ g
         θ-cong eq = unique (eq ○ commute _)
-  
+
       θ-natural′ : ∀ {X Y} (g : D [ L.₀ X , Y ]) → θ g C.≈ R.₁ g C.∘ θ D.id
       θ-natural′ g = θ-cong (introʳ L.identity) ○ θ-natural C.id g ○ C.∘-resp-≈ʳ (θ-cong L.identity)
         where open C.HomReasoning
@@ -135,14 +135,14 @@ private
         where open C.HomReasoning
               module DH = D.HomReasoning
               open MR D
-        
+
       unique′ : ∀ {X Y} {f g : C [ X , R.₀ Y ]} (h : D [ L.₀ X , Y ]) →
                   h D.≈ counit.η Y D.∘ L.₁ f →
                   h D.≈ counit.η Y D.∘ L.₁ g →
                   f C.≈ g
       unique′ _ eq₁ eq₂ = ⟺ (unique eq₁) ○ unique eq₂
         where open C.HomReasoning
-      
+
       zag : ∀ {B} → R.F₁ (counit.η B) C.∘ θ D.id C.≈ C.id
       zag {B} = unique′ (counit.η B)
                         (⟺ (cancelʳ (⟺ (commute D.id))) ○ pushˡ (counit.sym-commute (counit.η B)) ○ D.∘-resp-≈ʳ (⟺ L.homomorphism))
@@ -162,6 +162,6 @@ module _ {L : Functor C D} {R : Functor D C} where
 
   fromUnit : FromUnit L R → L ⊣ R
   fromUnit = FromUnit.L⊣R
-  
+
   fromCounit : FromCounit L R → L ⊣ R
   fromCounit = FromCounit.L⊣R

src/Categories/Adjoint/Construction/CoEilenbergMoore.agda

@@ -78,4 +78,4 @@ Forgetful⊣Cofree = record
   }
  ; zig = λ {A} → Comodule.identity A
  ; zag = λ {B} → Comonad.identityˡ M
- }
+ }

src/Categories/Adjoint/Parametric.agda

@@ -117,15 +117,15 @@ record ParametricAdjoint {C D E : Category o ℓ e} (L : Functor C (Functors D E
         where
           open D.HomReasoning
           open MR D
-      
+
       adjunction-iso : ∀ {X Y} (f : X C.⇒ Y) → A.Ladjunct X (A.Radjunct X (η (R.₁ f) A))
                        D.≈ A.Ladjunct X (A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A))
       adjunction-iso {X} {Y} f = adjunction-isoˡ f ○ ⟺ (adjunction-isoʳ f)
         where open D.HomReasoning
 
       is-cowedge : ∀ {X Y} (f : X C.⇒ Y) → A.Radjunct X (η (R.₁ f) A) E.≈ A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A)
       is-cowedge {X} {Y} f = Injection.injective (Inverse⇒Injection (Hom-inverse (areAdjoint X) (RR.₀ Y A) A)) (adjunction-iso f)
-      
+
       -- the dinat needed is  DinaturalTransformation F (const E)
       -- where F = PABifunctor {A} and E is A and G = const E
       -- here we inline the definitions

src/Categories/Adjoint/RAPL.agda

@@ -45,7 +45,7 @@ module _ {o″ ℓ″ e″} {J : Category o″ ℓ″ e″} (F : Functor J D) wh
     }
     where module lim = LF.Limit lim
           open lim
-          
+
           ⊤ : CRF.Cone
           ⊤ = record
             { N    = R.F₀ apex
@@ -54,7 +54,7 @@ module _ {o″ ℓ″ e″} {J : Category o″ ℓ″ e″} (F : Functor J D) wh
               ; commute = λ f → [ R ]-resp-∘ (limit-commute f)
               }
             }
-            
+
           K′ : CRF.Cone → CF.Cone
           K′ K = record
             { N    = L.F₀ K.N
@@ -72,9 +72,9 @@ module _ {o″ ℓ″ e″} {J : Category o″ ℓ″ e″} (F : Functor J D) wh
             where module K = CRF.Cone K
                   open D.HomReasoning
                   open MR D
-                  
+
           module K′ K = CF.Cone (K′ K)
-          
+
           ! : ∀ {K : CRF.Cone} → CRF.Cones [ K , ⊤ ]
           ! {K} = record
             { arr     = R.F₁ (rep (K′ K)) C.∘ unit.η K.N
@@ -93,7 +93,7 @@ module _ {o″ ℓ″ e″} {J : Category o″ ℓ″ e″} (F : Functor J D) wh
                           open MR C
 
           module ! {K} = CRF.Cone⇒ (! {K})
-          
+
           !-unique : ∀ {K : CRF.Cone} (f : CRF.Cones [ K , ⊤ ]) → CRF.Cones [ ! ≈ f ]
           !-unique {K} f =
             let open C.HomReasoning
@@ -104,7 +104,7 @@ module _ {o″ ℓ″ e″} {J : Category o″ ℓ″ e″} (F : Functor J D) wh
                f.arr                            ∎
             where module K = CRF.Cone K
                   module f = CRF.Cone⇒ f
-                  
+
                   f′ : CF.Cones [ K′ K , limit ]
                   f′ = record
                     { arr     = Radjunct f.arr

src/Categories/Adjoint/TwoSided/Compose.agda

@@ -29,7 +29,6 @@ _∘⊣⊢_ {C = C} {D} {E} {L} {R} {L′} {R′} L⊣⊢R L′⊣⊢R′ = with
   ; zig    = zig
   }
   where
-  private
     module C   = Category C using (_∘_; id; assoc; identityˡ; module HomReasoning)
     module D   = Category D using (id)
     module E   = Category E using (_∘_; id; _≈_; assoc; identityˡ; module HomReasoning)

src/Categories/Bicategory/Construction/LaxSlice.agda

@@ -68,12 +68,12 @@ module SliceHom (A : Obj) where
           open HomReasoning
           open Equiv
           open MR (hom X.Y A)
-          
+
   SliceHomCat : SliceObj A → SliceObj A → 1Category (o ⊔ ℓ) (ℓ ⊔ e) e
   SliceHomCat X Y = record
     { Obj = Slice⇒₁ X Y
     ; _⇒_ = Slice⇒₂
-    ; _≈_ = λ (slicearr₂ {ϕ} _) (slicearr₂ {ψ} _) → ϕ ≈ ψ 
+    ; _≈_ = λ (slicearr₂ {ϕ} _) (slicearr₂ {ψ} _) → ϕ ≈ ψ
     ; id = slice-id _
     ; _∘_ = _∘ᵥ/_
     ; assoc = hom.assoc
@@ -102,7 +102,7 @@ module SliceHom (A : Obj) where
   _⊚₀/_ {X}{Y}{Z} J K = slicearr₁ ((α⇒ ∘ᵥ J.Δ ◁ K.h) ∘ᵥ K.Δ)
     where module K = Slice⇒₁ K
           module J = Slice⇒₁ J
-  
+
   _⊚₁/_ : ∀ {X Y Z : SliceObj A} → {J J' : Slice⇒₁ Y Z} → {K K' : Slice⇒₁ X Y} → Slice⇒₂ J J' → Slice⇒₂ K K' → Slice⇒₂ (J ⊚₀/ K) (J' ⊚₀/ K')
   _⊚₁/_ {X}{Y}{Z}{J'}{J}{K'}{K} δ γ = slicearr₂ $ begin
     (α⇒ ∘ᵥ J.Δ ◁ K.h) ∘ᵥ K.Δ                                                  ≈⟨ (refl⟩∘⟨ γ.E) ⟩
@@ -122,7 +122,7 @@ module SliceHom (A : Obj) where
           module K = Slice⇒₁ K
           module K' = Slice⇒₁ K'
           module γ = Slice⇒₂ γ
-          module δ = Slice⇒₂ δ          
+          module δ = Slice⇒₂ δ
           open 1Category (hom X.Y A)
           open HomReasoning
           open MR (hom X.Y A)
@@ -142,7 +142,7 @@ module SliceHom (A : Obj) where
       where module X = SliceObj X
             module Y = SliceObj Y
             module Z = SliceObj Z
-  
+
   α⇒/ : ∀ {W X Y Z}(J : Slice⇒₁ Y Z) (K : Slice⇒₁ X Y) (L : Slice⇒₁ W X) → Slice⇒₂ ((J ⊚₀/ K) ⊚₀/ L) (J ⊚₀/ (K ⊚₀/ L))
   α⇒/ {W}{X}{Y}{Z} J K L = slicearr₂ $ begin
     (α⇒ ∘ᵥ J.Δ ◁ K.h ⊚₀ L.h) ∘ᵥ ((α⇒ ∘ᵥ K.Δ ◁ L.h) ∘ᵥ L.Δ  )                  ≈⟨ pullʳ (center⁻¹ (sym α⇒-◁-∘₁) refl) ⟩
@@ -205,7 +205,7 @@ module SliceHom (A : Obj) where
           module Y = SliceObj Y
           module J = Slice⇒₁ J
           module K = Slice⇒₁ K
-          module α = Slice⇒₂ α          
+          module α = Slice⇒₂ α
           open 1Category (hom X.Y A)
           open HomReasoning
           open MR (hom X.Y A)

src/Categories/Bicategory/Construction/Spans.agda

@@ -136,7 +136,7 @@ module _ (f : Span C D) (g : Span B C) (h : Span A B) where
             p₂ pullback-gh ∘ universal pullback-gh _ ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-gh) ⟩
             (p₁ pullback-fg ∘ p₂ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _     ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
             p₁ pullback-fg ∘ universal pullback-fg _                              ≈⟨ p₁∘universal≈h₁ pullback-fg ⟩
-            p₂ pullback-gh ∘ p₁ pullback-f⟨gh⟩ ∎ 
+            p₂ pullback-gh ∘ p₁ pullback-f⟨gh⟩ ∎
 
           lemmaˡ = begin
             p₁ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
@@ -291,7 +291,7 @@ pentagon {A} {B} {C} {D} {E} f g h i =
         p₂ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-fg) ⟩
         (p₁ pullback-gh ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _     ≈⟨ center (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
         p₁ pullback-gh ∘ (p₁ pullback-⟨gh⟩i ∘ p₂ pullback-f⟨⟨gh⟩i⟩) ∘ universal pullback-f⟨⟨gh⟩i⟩ _           ≈⟨ center⁻¹ refl (p₂∘universal≈h₂ pullback-f⟨⟨gh⟩i⟩) ⟩
-        (p₁ pullback-gh ∘ p₁ pullback-⟨gh⟩i) ∘ universal pullback-⟨gh⟩i _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩              ≈⟨ center (p₁∘universal≈h₁ pullback-⟨gh⟩i) ⟩ 
+        (p₁ pullback-gh ∘ p₁ pullback-⟨gh⟩i) ∘ universal pullback-⟨gh⟩i _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩              ≈⟨ center (p₁∘universal≈h₁ pullback-⟨gh⟩i) ⟩
         p₁ pullback-gh ∘ universal pullback-gh _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                       ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-gh) ⟩
         p₁ pullback-g⟨hi⟩ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                              ≈˘⟨ p₂∘universal≈h₂ pullback-fg ⟩
         p₂ pullback-fg ∘ universal pullback-fg _                                                              ∎

src/Categories/Bicategory/Object/Product.agda

@@ -24,9 +24,9 @@ record Product  (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
     β₁a : ∀ {Γ} f g → hom Γ A [ πa ∘₁ ⟨ f , g ⟩₁  ≅ f ]
     β₁b : ∀ {Γ} f g → hom Γ B [ πb ∘₁ ⟨ f , g ⟩₁  ≅ g ]
     β₂a : ∀ {Γ}{fa ga fb gb}(αa : hom Γ A [ fa , ga ])(αb : hom Γ B [ fb , gb ])
-        → Along β₁a _ _ , β₁a _ _ [ πa ▷ ⟨ αa , αb ⟩₂ ≈ αa ] 
+        → Along β₁a _ _ , β₁a _ _ [ πa ▷ ⟨ αa , αb ⟩₂ ≈ αa ]
     β₂b : ∀ {Γ}{fa ga fb gb}(αa : hom Γ A [ fa , ga ])(αb : hom Γ B [ fb , gb ])
-        → Along β₁b _ _ , β₁b _ _ [ πb ▷ ⟨ αa , αb ⟩₂ ≈ αb ] 
+        → Along β₁b _ _ , β₁b _ _ [ πb ▷ ⟨ αa , αb ⟩₂ ≈ αb ]
 
     η₁ : ∀ {Γ} p → hom Γ A×B [ p ≅ ⟨ πa ∘₁ p , πb ∘₁ p ⟩₁ ]
     η₂ : ∀ {Γ}{p p'}(ϕ : hom Γ A×B [ p , p' ])

src/Categories/Bicategory/Object/Terminal.agda

@@ -17,5 +17,5 @@ record IsTerminal (⊤ : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
 
     η₁ : ∀ {A} f → hom A ⊤ [ f ≅ !₁ ]
     η₂ : ∀ {A}{f g}(α : hom A ⊤ [ f , g ])
-       → Along η₁ _ , η₁ _ [ α ≈ !₂ ] 
+       → Along η₁ _ , η₁ _ [ α ≈ !₂ ]