blob: 01e09536ce1f3e26e6482f203882430cf5e50196 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)
open import Level using (Level; _β_)
module Morphism.Zero {o β e : Level} (π : Category o β e) where
open Category π
record IsZeroβ {A B : Obj} (z : A β B) : Set (o β β β e) where
field
constant : {C : Obj} (f g : C β A) β z β f β z β g
coconstant : {C : Obj} (f g : B β C) β f β z β g β z
|
