From edf552cb86191732c7bb6bf1949e85cdcce6a31b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Feb 2018 18:15:07 +0100 Subject: [PATCH] Do not define synonym for contractible --- src/Cat/Category.agda | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) 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 ℂ