Cosmetics

This commit is contained in:
Frederik Hanghøj Iversen 2018-02-21 12:59:31 +01:00
parent edf552cb86
commit ed40824edc

View file

@ -65,17 +65,17 @@ 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₁
IsInitial : Object Set (a b)
IsInitial I = {X : Object} isContr (Arrow I X)
IsInitial : Object Set (a b)
IsInitial I = {X : Object} isContr (Arrow I X)
IsTerminal : Object Set (a b)
IsTerminal T = {X : Object} isContr (Arrow X T)
Initial : Set (a b)
Initial = Σ (Object) IsInitial
Initial : Set (a b)
Initial = Σ Object IsInitial
Terminal : Set (a b)
Terminal = Σ (Object) IsTerminal
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