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

Remove unused function

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-21 14:05:10 +01:00
parent 7398210a2b
commit a82095604d
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Cat/Categories/Sets.agda
View file

@ -24,9 +24,6 @@ module _ (ℓ : Level) where
𝟙 SetsRaw = Function.id 𝟙 SetsRaw = Function.id
_∘_ SetsRaw = Function._∘′_ _∘_ SetsRaw = Function._∘′_
setIsSet : (A : Set ℓ) → isSet A
setIsSet A x y p q = {!ua!}
SetsIsCategory : IsCategory SetsRaw SetsIsCategory : IsCategory SetsRaw
assoc SetsIsCategory = refl assoc SetsIsCategory = refl
proj₁ (ident SetsIsCategory) = funExt λ _ → refl proj₁ (ident SetsIsCategory) = funExt λ _ → refl