[WIP] Arrows are sets in special product category

src/Cat/Category/Product.agda

@@ -160,27 +160,31 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         l = ℂ.rightIdentity
 
     arrowsAreSets : ArrowsAreSets
-    arrowsAreSets {X , x0 , x1} {Y , y0 , y1} (f , f0 , f1) (g , g0 , g1) p q = {!!}
+    arrowsAreSets {X , x0 , x1} {Y , y0 , y1} (f , f0 , f1) (g , g0 , g1) p q = pq
       where
-      prop : ∀ {X Y} (x y : ℂ.Arrow X Y) → isProp (x ≡ y)
-      prop = ℂ.arrowsAreSets
+      -- prop : ∀ {X Y} (x y : ℂ.Arrow X Y) → isProp (x ≡ y)
+      -- prop = ℂ.arrowsAreSets
       a0 a1 : f ≡ g
       a0 i = proj₁ (p i)
       a1 i = proj₁ (q i)
       a : a0 ≡ a1
       a = ℂ.arrowsAreSets _ _ a0 a1
-      res : p ≡ q
-      res i j = a i j , {!b i j!} , {!!}
-        where
-        -- b0 b1 : (λ j → (ℂ [ y0 ∘ a i j ]) ≡ x0) [ f0 ≡ g0 ]
-        -- b0 = lemPropF (λ x → prop (ℂ [ y0 ∘ x ]) x0) (a i)
-        -- b1 = lemPropF (λ x → prop (ℂ [ y0 ∘ x ]) x0) (a i)
-        b0 : (λ j → (ℂ [ y0 ∘ a0 j ]) ≡ x0) [ f0 ≡ g0 ]
-        b0 = lemPropF (λ x → prop (ℂ [ y0 ∘ x ]) x0) a0
-        b1 : (λ j → (ℂ [ y0 ∘ a1 j ]) ≡ x0) [ f0 ≡ g0 ]
-        b1 = lemPropF (λ x → prop (ℂ [ y0 ∘ x ]) x0) a1
-        -- b : b0 ≡ b1
-        -- b = {!!}
+      module _ (i : I) where
+        r : f ≡ g
+        r = a i
+        module _ (j : I) where
+          prop0 : isProp (ℂ [ y0 ∘ r j ] ≡ x0)
+          prop0 = ℂ.arrowsAreSets _ _
+          prop1 : isProp (ℂ [ y1 ∘ r j ] ≡ x1)
+          prop1 = ℂ.arrowsAreSets _ _
+          prop : isProp (ℂ [ y0 ∘ r j ] ≡ x0 × ℂ [ y1 ∘ r j ] ≡ x1)
+          prop = propSig prop0 (λ _ → prop1)
+          helper : (b0 b1 : (ℂ [ y0 ∘ r j ]) ≡ x0 × (ℂ [ y1 ∘ r j ]) ≡ x1) → b0 ≡ b1
+          helper _ _ = lemPropF (λ _ → prop) p
+          b : (ℂ [ y0 ∘ r j ]) ≡ x0 × (ℂ [ y1 ∘ r j ]) ≡ x1
+          b = {!!}
+      pq : p ≡ q
+      pq i j = a i j , b i j
 
     open Univalence isIdentity