diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 27f271e..50f21cd 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -65,14 +65,11 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
     Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
 
-  unique = isContr
-
   IsInitial : Object → Set (ℓa ⊔ ℓb)
-  IsInitial I = {X : Object} → unique (Arrow I X)
+  IsInitial I = {X : Object} → isContr (Arrow I X)
 
   IsTerminal : Object → Set (ℓa ⊔ ℓb)
-  -- ∃![ ? ] ?
-  IsTerminal T = {X : Object} → unique (Arrow X T)
+  IsTerminal T = {X : Object} → isContr (Arrow X T)
 
   Initial : Set (ℓa ⊔ ℓb)
   Initial = Σ (Object) IsInitial
@@ -80,7 +77,6 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   Terminal : Set (ℓa ⊔ ℓb)
   Terminal = Σ (Object) IsTerminal
 
-
 -- Univalence is indexed by a raw category as well as an identity proof.
 module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ