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

Remove undefined

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-01-21 14:32:27 +01:00
parent 4c13334277
commit 316de7e4f9
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Cat/Category.agda
View file

@ -22,8 +22,6 @@ open import Cubical
syntax ∃!-syntax (λ x → B) = ∃![ x ] B syntax ∃!-syntax (λ x → B) = ∃![ x ] B
postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
record IsCategory {ℓ ℓ' : Level} record IsCategory {ℓ ℓ' : Level}
(Object : Set ℓ) (Object : Set ℓ)
(Arrow : Object → Object → Set ℓ') (Arrow : Object → Object → Set ℓ')