Category.Product: Factor out use of arrowAreSets to shorten proofs

src/Cat/Category/Product.agda

@@ -154,59 +154,40 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
   open RawCategory raw
 
+  propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y')
+            → (xy : ℂ.Arrow X Y) → isProp (ℂ [ ya ∘ xy ] ≡ xa × ℂ [ yb ∘ xy ] ≡ xb)
+  propEqs xs = propSig (ℂ.arrowsAreSets _ _) (\ _ → ℂ.arrowsAreSets _ _)
+
   isAssocitaive : IsAssociative
-  isAssocitaive {A , a0 , a1} {B , _} {C , c0 , c1} {D , d0 , d1} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i
-    = s0 i , rl i , rr i
+  isAssocitaive {A'@(A , a0 , a1)} {B , _} {C , c0 , c1} {D'@(D , d0 , d1)} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i
+    = s0 i , lemPropF propEqs s0 {proj₂ l} {proj₂ r} i
     where
     l = hh ∘ (gg ∘ ff)
     r = hh ∘ gg ∘ ff
     -- s0 : h ℂ.∘ (g ℂ.∘ f) ≡ h ℂ.∘ g ℂ.∘ f
     s0 : proj₁ l ≡ proj₁ r
     s0 = ℂ.isAssociative {f = f} {g} {h}
-    prop0 : ∀ a → isProp (ℂ [ d0 ∘ a ] ≡ a0)
-    prop0 a = ℂ.arrowsAreSets (ℂ [ d0 ∘ a ]) a0
-    rl : (λ i → (ℂ [ d0 ∘ s0 i ]) ≡ a0) [ proj₁ (proj₂ l) ≡ proj₁ (proj₂ r) ]
-    rl = lemPropF prop0 s0
-    prop1 : ∀ a → isProp ((ℂ [ d1 ∘ a ]) ≡ a1)
-    prop1 a = ℂ.arrowsAreSets _ _
-    rr : (λ i → (ℂ [ d1 ∘ s0 i ]) ≡ a1) [ proj₂ (proj₂ l) ≡ proj₂ (proj₂ r) ]
-    rr = lemPropF prop1 s0
+
 
   isIdentity : IsIdentity 𝟙
   isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity
     where
     leftIdentity : 𝟙 ∘ (f , f0 , f1) ≡ (f , f0 , f1)
-    leftIdentity i = l i , rl i , rr i
+    leftIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
       where
       L = 𝟙 ∘ (f , f0 , f1)
       R : Arrow AA BB
       R = f , f0 , f1
       l : proj₁ L ≡ proj₁ R
       l = ℂ.leftIdentity
-      prop0 : ∀ a → isProp ((ℂ [ b0 ∘ a ]) ≡ a0)
-      prop0 a = ℂ.arrowsAreSets _ _
-      rl : (λ i → (ℂ [ b0 ∘ l i ]) ≡ a0) [ proj₁ (proj₂ L) ≡ proj₁ (proj₂ R) ]
-      rl = lemPropF prop0 l
-      prop1 : ∀ a → isProp (ℂ [ b1 ∘ a ] ≡ a1)
-      prop1 _ = ℂ.arrowsAreSets _ _
-      rr : (λ i → (ℂ [ b1 ∘ l i ]) ≡ a1) [ proj₂ (proj₂ L) ≡ proj₂ (proj₂ R) ]
-      rr = lemPropF prop1 l
     rightIdentity : (f , f0 , f1) ∘ 𝟙 ≡ (f , f0 , f1)
-    rightIdentity i = l i , rl i , {!!}
+    rightIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
       where
       L = (f , f0 , f1) ∘ 𝟙
       R : Arrow AA BB
       R = (f , f0 , f1)
       l : ℂ [ f ∘ ℂ.𝟙 ] ≡ f
       l = ℂ.rightIdentity
-      prop0 : ∀ a → isProp ((ℂ [ b0 ∘ a ]) ≡ a0)
-      prop0 _ = ℂ.arrowsAreSets _ _
-      rl : (λ i → (ℂ [ b0 ∘ l i ]) ≡ a0) [ proj₁ (proj₂ L) ≡ proj₁ (proj₂ R) ]
-      rl = lemPropF prop0 l
-      prop1 : ∀ a → isProp ((ℂ [ b1 ∘ a ]) ≡ a1)
-      prop1 _ = ℂ.arrowsAreSets _ _
-      rr : (λ i → (ℂ [ b1 ∘ l i ]) ≡ a1) [ proj₂ (proj₂ L) ≡ proj₂ (proj₂ R) ]
-      rr = lemPropF prop1 l
 
   cat : IsCategory raw
   cat = record