Remove the duplicate of eq-pair

Author: arnoudvanderleer

src/category-theory/functor-curry.lagda.md

@@ -15,7 +15,7 @@ open import category-theory.precategory-of-functors
 open import category-theory.products-of-precategories
 
 open import foundation.action-on-identifications-functions
-open import foundation.cartesian-product-types
+open import foundation.equality-cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels
@@ -132,7 +132,7 @@ module CurryFunctor
           ＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
               (f , id-hom-Precategory D)
               (id-hom-Precategory C , g))
-            by ap (hom-functor-Precategory CD E F) (identity-product
+            by ap (hom-functor-Precategory CD E F) (eq-pair
               (left-unit-law-comp-hom-Precategory C f
                 ∙ inv (right-unit-law-comp-hom-Precategory C f))
               (right-unit-law-comp-hom-Precategory D g

src/foundation/cartesian-product-types.lagda.md

@@ -31,24 +31,6 @@ tr-product :
 tr-product B C refl u = refl
 ```
 
-### Identities of products
-
-```agda
-identity-product :
-  {l1 l2 : Level}
-  {A : UU l1} {B : UU l2}
-  {a a' : A} {b b' : B}
-  → a ＝ a' → b ＝ b' → (a , b) ＝ (a' , b')
-identity-product refl refl = refl
-
-identity-product' :
-  {l1 l2 : Level}
-  {A : UU l1} {B : UU l2}
-  {ab ab' : A × B}
-  → pr1 ab ＝ pr1 ab' → pr2 ab ＝ pr2 ab' → ab ＝ ab'
-identity-product' refl refl = refl
-```
-
 ### Subuniverses closed under cartesian product types
 
 ```agda