add fixity

Categories/2-Category.agda

@@ -17,6 +17,10 @@ open import Categories.Product using (assocʳ; πˡ; πʳ)
 
 record 2-Category (o ℓ t e : Level) : Set (suc (o ⊔ ℓ ⊔ t ⊔ e)) where
   open Terminal (Categories ℓ t e) (One {ℓ} {t} {e})
+
+  infix  4 _⇒_
+  infixr 9 _∘_
+
   field
     Obj : Set o
     _⇒_ : (A B : Obj) → Category ℓ t e
@@ -25,7 +29,7 @@ record 2-Category (o ℓ t e : Level) : Set (suc (o ⊔ ℓ ⊔ t ⊔ e)) where
   _∘_ : {A B C : Obj} {L R : Category ℓ t e} → Functor L (B ⇒ C) → Functor R (A ⇒ B) → Bifunctor L R (A ⇒ C)
   _∘_ {A} {B} {C} F G = reduce-× {D₁ = B ⇒ C} {D₂ = A ⇒ B} —∘— F G
   field
-    .assoc : ∀ {A B C D : Obj} → ((—∘— ∘ idF) ∘F assocʳ (C ⇒ D) (B ⇒ C) (A ⇒ B)) ≡F idF ∘ —∘—
+    .assoc : ∀ {A B C D : Obj} → ((—∘— ∘ idF) ∘F assocʳ (C ⇒ D) (B ⇒ C) (A ⇒ B)) ≡F (idF ∘ —∘—)
     .identityˡ : {A B : Obj} → (id {B} ∘ idF {C = A ⇒ B}) ≡F πʳ {C = ⊤} {A ⇒ B}
     .identityʳ : {A B : Obj} → (idF {C = A ⇒ B} ∘ id {A}) ≡F πˡ {C = A ⇒ B} {⊤}
 

Categories/Agda.agda

@@ -61,7 +61,7 @@ Setoids c ℓ = record
   where
   infix  4 _≡′_
   open Function.Equality using (_⟨$⟩_; cong; _⟶_) renaming (_∘_ to _∘′_; id to id′)
-  open Relation.Binary using (Setoid; Rel)
+  open Relation.Binary using (Setoid; module Setoid; Rel)
 
   _≡′_ : ∀ {X Y} → Rel (X ⟶ Y) _
   _≡′_ {X} {Y} f g = ∀ {x} → Setoid._≈_ Y (f ⟨$⟩ x) (g ⟨$⟩ x)

Categories/Category.agda

@@ -14,8 +14,9 @@ postulate
   .irr : ∀ {a} {A : Set a} → .A → A
 
 record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where 
+
+  infix  4 _≡_ _⇒_
   infixr 9 _∘_
-  infix  4 _≡_
 
   field
     Obj : Set o
@@ -105,6 +106,8 @@ record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
   .id-comm : ∀ {a b} {f : a ⇒ b} → f ∘ id ≡ id ∘ f
   id-comm = trans identityʳ (sym identityˡ)
 
+infix 10  _[_,_] _[_≡_] _[_∘_]
+
 _[_,_] : ∀ {o ℓ e} → (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ
 _[_,_] = Category._⇒_
 
@@ -119,6 +122,8 @@ module Heterogeneous {o ℓ e} (C : Category o ℓ e) where
   open Category C
   open Equiv renaming (refl to refl′; sym to sym′; trans to trans′; reflexive to reflexive′)
 
+  infix 4 _∼_
+
   data _∼_ {A B} (f : A ⇒ B) : ∀ {X Y} → (X ⇒ Y) → Set (ℓ ⊔ e) where
     ≡⇒∼ : {g : A ⇒ B} → .(f ≡ g) → f ∼ g
 

Categories/Comma.agda

@@ -46,6 +46,7 @@ Comma {o₁}{ℓ₁}{e₁}
 
     infixr 9 _∘′_
     infix  4 _≡′_
+    infix 10 _,_,_ _,_[_]    
 
     record Obj : Set (o₁ ⊔ o₂ ⊔ ℓ₃) where
         constructor _,_,_

Categories/Congruence.agda

@@ -138,6 +138,8 @@ module Heterogeneous {o ℓ e} {C : Category o ℓ e} {q} (Q : Congruence C q) w
   open Equiv renaming (refl to refl′; sym to sym′; trans to trans′; reflexive to reflexive′)
   open Equiv₀ renaming (refl to refl₀; sym to sym₀; trans to trans₀; reflexive to reflexive₀)
 
+  infix 4 _∼_
+
   data _∼_ {A B} (f : A ⇒ B) {X Y} (g : X ⇒ Y) : Set (o ⊔ ℓ ⊔ e ⊔ q) where
     ≡⇒∼ : (ax : A ≡₀ X) (by : B ≡₀ Y) → .(coerce ax by f ≡ g) → f ∼ g
 
@@ -234,7 +236,7 @@ module Heterogeneous {o ℓ e} {C : Category o ℓ e} {q} (Q : Congruence C q) w
   -- floatʳ-resp-∼ : ∀ {A A′ B} (A≣A′ : A ≣ A′) {f : C [ A , B ]} → f ∼ floatʳ A≣A′ f
   -- floatʳ-resp-∼ ≣-refl = refl
 
-  infix 3 ▹_
+  infixr 4 ▹_
 
   record -⇒- : Set (o ⊔ ℓ) where
     constructor ▹_

Categories/Globe.agda

@@ -21,6 +21,8 @@ data GlobeHom : (m n : ℕ) → Set where
   σ : {m n : ℕ} (n<m : n < m) → GlobeHom n m
   τ : {m n : ℕ} (n<m : n < m) → GlobeHom n m
 
+infixl 7 _⊚_
+
 _⊚_ : ∀ {l m n} → GlobeHom m n → GlobeHom l m → GlobeHom l n
 I ⊚ y = y
 x ⊚ I = x
@@ -111,6 +113,8 @@ GlobeEquiv = record { refl = refl; sym = sym; trans = trans }
   trans both-σ both-σ = both-σ
   trans both-τ both-τ = both-τ
 
+infixl 7 _⊚′_
+
 _⊚′_ : ∀ {l m n} → GlobeHom′ m n → GlobeHom′ l m → GlobeHom′ l n
 x ⊚′ I = x
 x ⊚′ y σ′ = (x ⊚′ y) σ′
@@ -163,4 +167,4 @@ plain x ⊚ʳ plain y = plain (x ⊚ y)
 plain I ⊚ʳ ι y = ι y
 plain (σ _) ⊚ʳ ι y = (plain (stripped σ n<m)) ⊚ʳ y
 plain (τ n<m) ⊚ʳ ι y = (plain (stripped τ n<m)) ⊚ʳ y
--}
+-}

Categories/Morphism/Indexed.agda

@@ -108,7 +108,7 @@ f ◽ g = record { _⟨$⟩_ = λ x → (f ‼ x) ∘ (g ‼ x)
                ; cong = λ x≈y → ∘-resp-∼ (cong₁ f x≈y) (cong₁ g x≈y) }
 
 .assoc-◽⋉ : ∀ {X Ys Zs Ws} {f : Zs ∗⇒∗ Ws} {g : Ys ∗⇒∗ Zs} {h : X ⇒∗ Ys}
-          → X ⇨∗ Ws [ _⋉_ {Ys = Ys} {Ws} (_◽_ {Ys} {Zs} {Ws} f g) h ≈ _⋉_ {Ys = Zs} {Ws} f (_⋉_ {Ys = Ys} {Zs} g h) ]
+          → (X ⇨∗ Ws) [ _⋉_ {Ys = Ys} {Ws} (_◽_ {Ys} {Zs} {Ws} f g) h ≈ _⋉_ {Ys = Zs} {Ws} f (_⋉_ {Ys = Ys} {Zs} g h) ]
 assoc-◽⋉ {Ys = Ys} {Zs} {Ws} {f = f} {g} {h} {i} {j} i≈j with Ys ! j | cong₀ Ys i≈j | Zs ! j | cong₀ Zs i≈j | Ws ! j | cong₀ Ws i≈j | f ‼ j | cong₁ f i≈j | g ‼ j | cong₁ g i≈j | h ‼ j | cong₁ h i≈j
 assoc-◽⋉ {f = f} {g} {h} {i} i≈j | ._ | ≣-refl | ._ | ≣-refl | ._ | ≣-refl | fj | ≡⇒∼ fi≡fj | gj | ≡⇒∼ gi≡gj | hj | ≡⇒∼ hi≡hj = 
   ≡⇒∼ (begin
@@ -120,4 +120,4 @@ assoc-◽⋉ {f = f} {g} {h} {i} i≈j | ._ | ≣-refl | ._ | ≣-refl | ._ | 
   ∎)
   where 
   open Heterogeneous C hiding (≡⇒∼)
-  open HomReasoning
+  open HomReasoning

Categories/NaturalTransformation.agda

@@ -5,6 +5,8 @@ open import Categories.Category
 open import Categories.Functor hiding (equiv) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)
 open import Categories.NaturalTransformation.Core public
 
+infixr 9 _∘ˡ_ _∘ʳ_
+
 _∘ˡ_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
      → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
      → {F G : Functor C D} 
@@ -181,4 +183,4 @@ interchange {C₀ = C₀} {C₁} {C₂} {F₀} {F₁} {F₅} {F₂} {F₃} {F₄
                {F F′ : Functor C D} {G G′ : Functor D E}
                {f h : NaturalTransformation G G′} {g i : NaturalTransformation F F′}
            → f ≡ h → g ≡ i → f ∘₀ g ≡ h ∘₀ i
-∘₀-resp-≡ {E = E} {G′ = G′} f≡h g≡i = Category.∘-resp-≡ E (Functor.F-resp-≡ G′ g≡i) f≡h
+∘₀-resp-≡ {E = E} {G′ = G′} f≡h g≡i = Category.∘-resp-≡ E (Functor.F-resp-≡ G′ g≡i) f≡h

Categories/NaturalTransformation/Core.agda

@@ -52,6 +52,8 @@ id {C = C} {D} {F} = record
     where 
     open D.HomReasoning
 
+infixr 9 _∘₁_ _∘₀_
+
 -- "Vertical composition"
 _∘₁_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁}
         {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁}
@@ -157,4 +159,4 @@ setoid {F = F} {G} = record
   { Carrier = NaturalTransformation F G
   ; _≈_ = _≡_
   ; isEquivalence = equiv {F = F}
-  }
+  }

Categories/Object/BinaryProducts.agda

@@ -17,6 +17,8 @@ open Product C
 open ProductMorphisms C
 
 record BinaryProducts : Set (o ⊔ ℓ ⊔ e) where
+
+  infixr 2 _×_
   infix 10 _⁂_
 
   field

Categories/Object/Exponentiating.agda

@@ -30,6 +30,8 @@ record Exponentiating Σ : Set (o ⊔ ℓ ⊔ e) where
         exponential : ∀{A} → Exponential A Σ
     module Σ↑ (X : Obj) = Exponential (exponential {X})
 
+    infixr 6 Σ↑_ Σ²_
+
     Σ↑_ : Obj → Obj
     Σ↑_ X = Σ↑.B^A X
 

Categories/Object/Product.agda

@@ -16,6 +16,9 @@ open GlueSquares C
 
 -- Borrowed from Dan Doel's definition of products
 record Product (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
+
+  infix 10 ⟨_,_⟩
+
   field
     A×B : Obj
     π₁ : A×B ⇒ A
@@ -176,4 +179,4 @@ Mobile p A₁≅A₂ B₁≅B₂ = record
   where
   module p = Product p
   open Product renaming (⟨_,_⟩ to _⟨_,_⟩)
-  open _≅_
+  open _≅_

Categories/Object/Product/Morphisms.agda

@@ -14,6 +14,8 @@ open HomReasoning
 open import Function using (flip)
 open import Level
 
+infix 10 [_]⟨_,_⟩ [_⇒_]_⁂_
+
 [[_]] : ∀{A B} → Product A B → Obj
 [[ p ]] = Product.A×B p
 

Categories/Square.agda

@@ -398,14 +398,9 @@ record NormReasoning {o ℓ e} (C : Category o ℓ e) (o′ ℓ′ : _) : Set (s
   open C
 
   infix  4 _IsRelatedTo_
-  infix  2 _∎
-  infixr 2 _≈⟨_⟩_
-  infixr 2 _↓⟨_⟩_
-  infixr 2 _↑⟨_⟩_
-  infixr 2 _↓≡⟨_⟩_
-  infixr 2 _↑≡⟨_⟩_
-  infixr 2 _↕_
   infix  1 begin_
+  infixr 2 _≈⟨_⟩_ _↓⟨_⟩_ _↑⟨_⟩_ _↓≡⟨_⟩_ _↑≡⟨_⟩_ _↕_
+  infix  3 _∎ 
 
   data _IsRelatedTo_ {X Y} (f g : _#⇒_ X Y) : Set e where
     relTo : (f∼g : norm f ≡ norm g) → f IsRelatedTo g

Categories/Support/EqReasoning.agda

@@ -8,15 +8,11 @@ module SetoidReasoning {s₁ s₂} (S : Setoid s₁ s₂) where
   open Setoid S
 
   infix  4 _IsRelatedTo_
-  infix  2 _∎
-  infixr 2 _≈⟨_⟩_
-  infixr 2 _↓⟨_⟩_
-  infixr 2 _↑⟨_⟩_
-  infixr 2 _↓≣⟨_⟩_
-  infixr 2 _↑≣⟨_⟩_
-  infixr 2 _↕_
   infix  1 begin_
-
+  infixr 2 _≈⟨_⟩_ _↓⟨_⟩_ _↑⟨_⟩_ _↓≣⟨_⟩_ _↑≣⟨_⟩_ _↕_
+  infix  3 _∎
+
+
   -- This seemingly unnecessary type is used to make it possible to
   -- infer arguments even if the underlying equality evaluates.
 

Categories/Support/IProduct.agda

@@ -74,7 +74,7 @@ zip′ : ∀ {a b c p q r}
       (_∙_ : A → B → C) →
       (∀ {x y} → P x → Q y → R (x ∙ y)) →
       Σ′ A P → Σ′ B Q → Σ′ C R
-zip′ _∙_ _∘_ (a , p) (b , q) = (a ∙ b , p ∘ q)
+zip′ _∙_ _∘_ (a , p) (b , q) = (a ∙ b) , (p ∘ q)
 
 _-×′-_ : ∀ {a b i j} {A : Set a} {B : Set b} →
         (A → B → Set i) → (A → B → Set j) → (A → B → Set _)
@@ -98,4 +98,4 @@ uncurry f (x , y) = f x y
 uncurry′ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
            (A → B → C) → (A × B → C)
 uncurry′ = uncurry
--}
+-}