Fix unique existential

src/Cat/Categories/Cat.agda

@@ -126,7 +126,17 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
       isUniq = isUniqL , isUniqR
 
     isProduct : ∃![ x ] (F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂)
-    isProduct = x , isUniq
+    isProduct = x , isUniq , uq
+      where
+      module _ {y : Functor X object} (eq : F[ proj₁ ∘ y ] ≡ x₁ × F[ proj₂ ∘ y ] ≡ x₂) where
+        omapEq : Functor.omap x ≡ Functor.omap y
+        omapEq = {!!}
+        -- fmapEq : (λ i → {!{A B : ?} → Arrow A B → 𝔻 [ ? A , ? B ]!}) [ Functor.fmap x ≡ Functor.fmap y ]
+        -- fmapEq = {!!}
+        rawEq : Functor.raw x ≡ Functor.raw y
+        rawEq = {!!}
+        uq : x ≡ y
+        uq = Functor≡ rawEq
 
 module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
   private

src/Cat/Categories/Sets.agda

@@ -328,7 +328,19 @@ module _ {ℓ : Level} where
 
         isProduct : IsProduct 𝓢 _ _ rawProduct
         IsProduct.ump isProduct {X = hX} f g
-          = (f &&& g) , ump hX f g
+          = f &&& g , ump hX f g , λ eq → funExt (umpUniq eq)
+          where
+          open Σ hX renaming (proj₁ to X) using ()
+          module _ {y : X → A × B} (eq : proj₁ Function.∘′ y ≡ f × proj₂ Function.∘′ y ≡ g) (x : X) where
+            p1 : proj₁ ((f &&& g) x) ≡ proj₁ (y x)
+            p1 = begin
+              proj₁ ((f &&& g) x) ≡⟨⟩
+              f x ≡⟨ (λ i → sym (proj₁ eq) i x) ⟩
+              proj₁ (y x) ∎
+            p2 : proj₂ ((f &&& g) x) ≡ proj₂ (y x)
+            p2 = λ i → sym (proj₂ eq) i x
+            umpUniq : (f &&& g) x ≡ y x
+            umpUniq i = p1 i , p2 i
 
       product : Product 𝓢 hA hB
       Product.raw       product = rawProduct

src/Cat/Prelude.agda

@@ -52,7 +52,7 @@ module _ (ℓ : Level) where
 ∃! = ∃!≈ _≡_
 
 ∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
-∃!-syntax = ∃
+∃!-syntax = ∃!
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B