Implicits in cong and unique-prime

Author: Taneb

src/Categories/Category/Complete/Properties/Construction.agda

@@ -75,17 +75,17 @@ module _ (prods : AllProductsOf (o′ ⊔ ℓ′)) (equalizer : ∀ {A B} (f g :
         K⇒ : K.N C.⇒ src
         K⇒ = OP.⟨ (λ j → K.ψ (lower j)) ⟩
 
-        Keq : (i : ∃₂ J._⇒_) → ϕ⇒ i C.∘ K⇒ C.≈ ψ⇒ i C.∘ K⇒
-        Keq i@(A , B , f) = begin
-          ϕ⇒ i C.∘ K⇒    ≈⟨ OP.commute ⟩
-          K.ψ B          ≈˘⟨ K.commute _ ⟩
-          F₁ f C.∘ K.ψ A ≈˘⟨ pullʳ OP.commute ⟩
-          ψ⇒ i C.∘ K⇒    ∎
+        Keq : {i : ∃₂ J._⇒_} → ϕ⇒ i C.∘ K⇒ C.≈ ψ⇒ i C.∘ K⇒
+        Keq = begin
+          _ C.∘ K⇒       ≈⟨ OP.commute ⟩
+          K.ψ _          ≈˘⟨ K.commute _ ⟩
+          F₁ _ C.∘ K.ψ _ ≈˘⟨ pullʳ OP.commute ⟩
+          _ C.∘ K⇒       ∎
 
         !-eq : ϕ C.∘ K⇒ C.≈ ψ C.∘ K⇒
         !-eq = begin
           ϕ C.∘ K⇒                   ≈⟨ MP.⟨⟩∘ _ _ ⟩
-          MP.⟨ (λ i → ϕ⇒ i C.∘ K⇒) ⟩ ≈⟨ MP.⟨⟩-cong _ _ Keq ⟩
+          MP.⟨ (λ i → ϕ⇒ i C.∘ K⇒) ⟩ ≈⟨ MP.⟨⟩-cong Keq ⟩
           MP.⟨ (λ i → ψ⇒ i C.∘ K⇒) ⟩ ≈˘⟨ MP.⟨⟩∘ _ _ ⟩
           ψ C.∘ K⇒                   ∎
 
@@ -102,7 +102,7 @@ module _ (prods : AllProductsOf (o′ ⊔ ℓ′)) (equalizer : ∀ {A B} (f g :
         !-unique f = ⟺ (eq.unique eq)
           where module f = Co.Cone⇒ F f
                 eq : K⇒ C.≈ eq.arr C.∘ f.arr
-                eq = OP.unique′ _ _ $ begin
+                eq = OP.unique′ $ begin
                   OP.π _ C.∘ K⇒                 ≈⟨ OP.commute ⟩
                   K.ψ _                         ≈˘⟨ f.commute ⟩
                   (OP.π _ C.∘ eq.arr) C.∘ f.arr ≈⟨ C.assoc ⟩

src/Categories/Object/Coproduct/Indexed.agda

@@ -27,11 +27,11 @@ record IndexedCoproductOf {i} {I : Set i} (P : I → Obj) : Set (i ⊔ o ⊔ e 
   ∘[] : ∀ {Y Z} (f : ∀ i → P i ⇒ Y) (g : Y ⇒ Z) → g ∘ [ f ] ≈ [ (λ i → g ∘ f i) ]
   ∘[] f g = sym (unique (pullʳ commute))
 
-  []-cong : ∀ {Y} (f g : ∀ i → P i ⇒ Y) → (∀ i → f i ≈ g i) → [ f ] ≈ [ g ]
-  []-cong f g eq = unique (trans commute (sym (eq _)))
+  []-cong : ∀ {Y} {f g : ∀ i → P i ⇒ Y} → (∀ {i} → f i ≈ g i) → [ f ] ≈ [ g ]
+  []-cong eq = unique (trans commute (sym eq))
 
-  unique′ : ∀ {Y} (h h′ : X ⇒ Y) → (∀ {i} → h′ ∘ ι i ≈ h ∘ ι i) → h′ ≈ h
-  unique′ h h′ f = trans (sym (unique f)) (η _)
+  unique′ : ∀ {Y} {h h′ : X ⇒ Y} → (∀ {i} → h′ ∘ ι i ≈ h ∘ ι i) → h′ ≈ h
+  unique′ f = trans (sym (unique f)) (η _)
 
 AllCoproductsOf : ∀ i → Set (o ⊔ ℓ ⊔ e ⊔ suc i)
 AllCoproductsOf i = ∀ {I : Set i} (P : I → Obj) → IndexedCoproductOf P

src/Categories/Object/Product/Indexed.agda

@@ -31,11 +31,11 @@ record IndexedProductOf {i} {I : Set i} (P : I → Obj) : Set (i ⊔ o ⊔ e ⊔
   ⟨⟩∘ : ∀ {Y Z} (f : ∀ i → Y ⇒ P i) (g : Z ⇒ Y) → ⟨ f ⟩ ∘ g ≈ ⟨ (λ i → f i ∘ g) ⟩
   ⟨⟩∘ f g = ⟺ (unique (pullˡ commute))
 
-  ⟨⟩-cong : ∀ {Y} (f g : ∀ i → Y ⇒ P i) → (eq : ∀ i → f i ≈ g i) → ⟨ f ⟩ ≈ ⟨ g ⟩
-  ⟨⟩-cong f g eq = unique (trans commute (⟺ (eq _)))
+  ⟨⟩-cong : ∀ {Y} {f g : ∀ i → Y ⇒ P i} → (eq : ∀ {i} → f i ≈ g i) → ⟨ f ⟩ ≈ ⟨ g ⟩
+  ⟨⟩-cong eq = unique (trans commute (⟺ eq))
 
-  unique′ : ∀ {Y} (h h′ : Y ⇒ X) → (∀ {i} → π i ∘ h′ ≈ π i ∘ h) → h′ ≈ h
-  unique′ h h′ f = trans (⟺ (unique f)) (η _)
+  unique′ : ∀ {Y} {h h′ : Y ⇒ X} → (∀ {i} → π i ∘ h′ ≈ π i ∘ h) → h′ ≈ h
+  unique′ f = trans (⟺ (unique f)) (η _)
 
 AllProductsOf : ∀ i → Set (o ⊔ ℓ ⊔ e ⊔ suc i)
 AllProductsOf i = ∀ {I : Set i} (P : I → Obj) → IndexedProductOf P