Merge pull request #459 from agda/indexed-products-more-implicits

JacquesCarette · web-flow · commit cce07616535e · 2025-03-03T07:39:34.000-05:00
Make inferable arguments implicit in Product.Indexed.{commute,unqiue}
diff --git a/src/Categories/Category/Complete/Properties/Construction.agda b/src/Categories/Category/Complete/Properties/Construction.agda
@@ -6,6 +6,7 @@ module Categories.Category.Complete.Properties.Construction {o ℓ e} (C : Categ
 
 open import Level
 open import Data.Product using (∃₂; _,_; -,_)
+open import Function.Base using (_$_)
 
 open import Categories.Category.Complete
 open import Categories.Diagram.Equalizer C
@@ -60,9 +61,9 @@ module _ (prods : AllProductsOf (o′ ⊔ ℓ′)) (equalizer : ∀ {A B} (f g :
         ; apex = record
           { ψ       = λ X → OP.π (lift X) C.∘ eq.arr
           ; commute = λ {X Y} f → begin
-            F₁ f C.∘ OP.π (lift X) C.∘ eq.arr ≈˘⟨ pushˡ (MP.commute ψ⇒ _) ⟩
+            F₁ f C.∘ OP.π (lift X) C.∘ eq.arr ≈˘⟨ pushˡ MP.commute ⟩
             (MP.π (-, -, f) C.∘ ψ) C.∘ eq.arr ≈˘⟨ pushʳ eq.equality ⟩
-            MP.π (-, -, f) C.∘ ϕ C.∘ eq.arr   ≈⟨ pullˡ (MP.commute ϕ⇒ _ ) ⟩
+            MP.π (-, -, f) C.∘ ϕ C.∘ eq.arr   ≈⟨ pullˡ MP.commute ⟩
             OP.π (lift Y) C.∘ eq.arr          ∎
           }
         }
@@ -74,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⇒                   ∎
 
@@ -93,19 +94,19 @@ module _ (prods : AllProductsOf (o′ ⊔ ℓ′)) (equalizer : ∀ {A B} (f g :
           { arr     = eq.equalize {h = K⇒} !-eq
           ; commute = λ {j} → begin
             (OP.π (lift j) C.∘ eq.arr) C.∘ eq.equalize !-eq ≈˘⟨ pushʳ eq.universal ⟩
-            OP.π (lift j) C.∘ K⇒                            ≈⟨ OP.commute _ _ ⟩
+            OP.π (lift j) C.∘ K⇒                            ≈⟨ OP.commute ⟩
             K.ψ j                                           ∎
           }
 
         !-unique : (f : Co.Cones F [ K , ⊤ ]) → Co.Cones F [ ! ≈ f ]
         !-unique f = ⟺ (eq.unique eq)
           where module f = Co.Cone⇒ F f
                 eq : K⇒ C.≈ eq.arr C.∘ f.arr
-                eq = OP.unique′ _ _ λ i → begin
-                  OP.π i C.∘ K⇒                 ≈⟨ OP.commute _ _ ⟩
-                  K.ψ (lower i)                 ≈˘⟨ f.commute ⟩
-                  (OP.π i C.∘ eq.arr) C.∘ f.arr ≈⟨ C.assoc ⟩
-                  OP.π i C.∘ eq.arr C.∘ f.arr   ∎
+                eq = OP.unique′ $ begin
+                  OP.π _ C.∘ K⇒                 ≈⟨ OP.commute ⟩
+                  K.ψ _                         ≈˘⟨ f.commute ⟩
+                  (OP.π _ C.∘ eq.arr) C.∘ f.arr ≈⟨ C.assoc ⟩
+                  OP.π _ C.∘ eq.arr C.∘ f.arr   ∎
 
       complete : Limit F
       complete = record
diff --git a/src/Categories/Category/Complete/Properties/SolutionSet.agda b/src/Categories/Category/Complete/Properties/SolutionSet.agda
@@ -65,9 +65,9 @@ module _ {C : Category o ℓ e} (Com : Complete (o ⊔ ℓ ⊔ o′) (o ⊔ ℓ
 
     prop : (f : W.X ⇒ W.X) → f ∘ equalizer.arr ≈ equalizer.arr
     prop f = begin
-      f ∘ equalizer.arr            ≈˘⟨ pullˡ (Warr.commute _ f) ⟩
+      f ∘ equalizer.arr            ≈˘⟨ pullˡ Warr.commute ⟩
       Warr.π f ∘ Γ ∘ equalizer.arr ≈˘⟨ refl⟩∘⟨ equalizer.equality ⟩
-      Warr.π f ∘ Δ ∘ equalizer.arr ≈⟨ cancelˡ (Warr.commute _ f) ⟩
+      Warr.π f ∘ Δ ∘ equalizer.arr ≈⟨ cancelˡ Warr.commute ⟩
       equalizer.arr                ∎
 
     ! : ∀ A → equalizer.obj ⇒ A
diff --git a/src/Categories/Object/Coproduct/Indexed.agda b/src/Categories/Object/Coproduct/Indexed.agda
@@ -18,20 +18,20 @@ record IndexedCoproductOf {i} {I : Set i} (P : I → Obj) : Set (i ⊔ o ⊔ e 
     ι : ∀ i → P i ⇒ X
     [_] : ∀ {Y} → (∀ i → P i ⇒ Y) → X ⇒ Y
 
-    commute : ∀ {Y} (f : ∀ i → P i ⇒ Y) → ∀ i → [ f ] ∘ ι i ≈ f i
-    unique : ∀ {Y} (h : X ⇒ Y) (f : ∀ i → P i ⇒ Y) → (∀ i → h ∘ ι i ≈ f i) → [ f ] ≈ h
+    commute : ∀ {Y} {f : ∀ i → P i ⇒ Y} {i} → [ f ] ∘ ι i ≈ f i
+    unique : ∀ {Y} {h : X ⇒ Y} {f : ∀ i → P i ⇒ Y} → (∀ {i} → h ∘ ι i ≈ f i) → [ f ] ≈ h
 
   η : ∀ {Y} (h : X ⇒ Y) → [ (λ i → h ∘ ι i) ] ≈ h
-  η h = unique _ _ λ _ → refl
+  η h = unique refl
 
   ∘[] : ∀ {Y Z} (f : ∀ i → P i ⇒ Y) (g : Y ⇒ Z) → g ∘ [ f ] ≈ [ (λ i → g ∘ f i) ]
-  ∘[] f g = sym (unique _ _ λ i → pullʳ (commute _ _))
+  ∘[] 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 _ _ λ i → trans (commute _ _) (sym (eq i))
+  []-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
diff --git a/src/Categories/Object/Product/Indexed.agda b/src/Categories/Object/Product/Indexed.agda
@@ -22,20 +22,20 @@ record IndexedProductOf {i} {I : Set i} (P : I → Obj) : Set (i ⊔ o ⊔ e ⊔
     π   : ∀ i → X ⇒ P i
     ⟨_⟩ : ∀ {Y} → (∀ i → Y ⇒ P i) → Y ⇒ X
 
-    commute : ∀ {Y} (f : ∀ i → Y ⇒ P i) → ∀ i → π i ∘ ⟨ f ⟩ ≈ f i
-    unique  : ∀ {Y} (h : Y ⇒ X) (f : ∀ i → Y ⇒ P i) → (∀ i → π i ∘ h ≈ f i) → ⟨ f ⟩ ≈ h
+    commute : ∀ {Y} {f : ∀ i → Y ⇒ P i} {i} → π i ∘ ⟨ f ⟩ ≈ f i
+    unique  : ∀ {Y} {h : Y ⇒ X} {f : ∀ i → Y ⇒ P i} → (∀ {i} → π i ∘ h ≈ f i) → ⟨ f ⟩ ≈ h
 
   η : ∀ {Y} (h : Y ⇒ X) → ⟨ (λ i → π i ∘ h) ⟩ ≈ h
-  η h = unique _ _ λ _ → refl
+  η h = unique refl
 
   ⟨⟩∘ : ∀ {Y Z} (f : ∀ i → Y ⇒ P i) (g : Z ⇒ Y) → ⟨ f ⟩ ∘ g ≈ ⟨ (λ i → f i ∘ g) ⟩
-  ⟨⟩∘ f g = ⟺ (unique _ _ λ i → pullˡ (commute _ _))
+  ⟨⟩∘ 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 _ _ λ i → trans (commute _ _) (⟺ (eq i))
+  ⟨⟩-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
diff --git a/src/Categories/Object/Product/Indexed/Properties.agda b/src/Categories/Object/Product/Indexed/Properties.agda
@@ -42,9 +42,8 @@ module _ {i} (Com : Complete (i ⊔ o′) (i ⊔ ℓ′) (i ⊔ e′) C) where
       { X       = L.apex
       ; π       = λ i → L.proj (lift i)
       ; ⟨_⟩     = λ f → L.rep (K f)
-      ; commute = λ f _ → Cone⇒.commute (L.rep-cone (K f))
-      ; unique  = λ f g eq → L.terminal.!-unique {A = K g} record
-        { arr     = f
-        ; commute = eq _
+      ; commute = Cone⇒.commute (L.rep-cone (K _))
+      ; unique  = λ eq → L.terminal.!-unique record
+        { commute = eq
         }
       }

Original file line number	Diff line number	Diff line change
`@@ -42,9 +42,8 @@ module _ {i} (Com : Complete (i ⊔ o′) (i ⊔ ℓ′) (i ⊔ e′) C) where`
`42`	`42`	`{ X = L.apex`
`43`	`43`	`; π = λ i → L.proj (lift i)`
`44`	`44`	`; ⟨_⟩ = λ f → L.rep (K f)`
`45`		`- ; commute = λ f _ → Cone⇒.commute (L.rep-cone (K f))`
`46`		`- ; unique = λ f g eq → L.terminal.!-unique {A = K g} record`
`47`		`- { arr = f`
`48`		`- ; commute = eq _`
	`45`	`+ ; commute = Cone⇒.commute (L.rep-cone (K _))`
	`46`	`+ ; unique = λ eq → L.terminal.!-unique record`
	`47`	`+ { commute = eq`
`49`	`48`	`}`
`50`	`49`	`}`