Add new type-synonym

This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 10:35:42 +01:00
parent a87d404aad
commit cc1ddaac9f

View file

@ -49,6 +49,9 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
IsIdentity id = {A B : Object} {f : Arrow A B}
f id f × id f f
ArrowsAreSets : Set (a b)
ArrowsAreSets = {A B : Object} isSet (Arrow A B)
IsInverseOf : {A B} (Arrow A B) (Arrow B A) Set b
IsInverseOf = λ f g g f 𝟙 × f g 𝟙
@ -100,7 +103,7 @@ record IsCategory {a b : Level} ( : RawCategory a b) : Set (lsuc
field
assoc : IsAssociative
ident : IsIdentity 𝟙
arrowIsSet : {A B : Object} isSet (Arrow A B)
arrowIsSet : ArrowsAreSets
univalent : Univalent ident
-- `IsCategory` is a mere proposition.
@ -162,8 +165,13 @@ module _ {a b : Level} {C : RawCategory a b} where
ident : (λ _ IsIdentity 𝟙) [ X.ident Y.ident ]
ident = propIsIdentity x X.ident Y.ident
done : x y
U : {a : IsIdentity 𝟙} (λ _ IsIdentity 𝟙) [ X.ident a ] (b : Univalent a) Set _
U eqwal bbb = (λ i Univalent (eqwal i)) [ X.univalent bbb ]
U : {a : IsIdentity 𝟙}
(λ _ IsIdentity 𝟙) [ X.ident a ]
(b : Univalent a)
Set _
U eqwal bbb =
(λ i Univalent (eqwal i))
[ X.univalent bbb ]
P : (y : IsIdentity 𝟙)
(λ _ IsIdentity 𝟙) [ X.ident y ] Set _
P y eq = (b' : Univalent y) U eq b'