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

Use bot from stdlib

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2017-11-15 22:56:04 +01:00
parent b46ef652ab
commit 1d040e5391
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Category.agda
View file

@ -6,6 +6,7 @@ open import Agda.Primitive
open import Data.Unit.Base open import Data.Unit.Base
open import Data.Product open import Data.Product
open import Cubical.PathPrelude open import Cubical.PathPrelude
open import Data.Empty
postulate undefined : {ℓ : Level} → {A : Set ℓ} → A postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
@ -115,8 +116,6 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } w
iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
data ⊥ : Set where
¬_ : {ℓ : Level} → Set ℓ → Set ℓ ¬_ : {ℓ : Level} → Set ℓ → Set ℓ
¬ A = A → ⊥ ¬ A = A → ⊥