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

Proove that IsCategory is a mere proposition!

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-20 18:01:26 +01:00
parent 159bffa6ae
commit a4f8a37e36
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Cat/Category.agda
View file

@ -165,7 +165,7 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
P y eq = ∀ (b' : Univ y) → U eq b' P y eq = ∀ (b' : Univ y) → U eq b'
helper : ∀ (b' : Univ X.ident) helper : ∀ (b' : Univ X.ident)
→ (λ _ → Univ X.ident) [ X.univalent ≡ b' ] → (λ _ → Univ X.ident) [ X.univalent ≡ b' ]
helper univ = {!!} helper univ = propUnivalent x X.univalent univ
foo = pathJ P helper Y.ident ident foo = pathJ P helper Y.ident ident
eqUni : U ident Y.univalent eqUni : U ident Y.univalent
eqUni = foo Y.univalent eqUni = foo Y.univalent