From facd1167e0c8455e2f790a5fa6df8ebe1fb4eef6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 27 Mar 2018 14:18:13 +0200
Subject: [PATCH] Fix unique existential

---
 src/Cat/Categories/Cat.agda  | 12 +++++++++++-
 src/Cat/Categories/Sets.agda | 14 +++++++++++++-
 src/Cat/Prelude.agda         |  2 +-
 3 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 8843914..3021268 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/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
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 05c64b3..f4c59fd 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/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
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index f561330..036d2c7 100644
--- a/src/Cat/Prelude.agda
+++ b/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