fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Do not define synonym for contractible

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-20 18:15:07 +01:00
parent d2da84269f
commit edf552cb86
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Cat/Category.agda
View file

@ -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 ℂ