123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140JointMono : {ΞΉ : Level} (I : Set ΞΉ) (B : I β Obj) β ((i : I) β A β B i) β Set (o β β β e β ΞΉ)JointMono {A} I B f = β {C} β (gβ gβ : C β A) β ((i : I) β f i β gβ β f i β gβ) β gβ β gβJointEpi {B} I A f = β {C} β (gβ gβ : B β C) β ((i : I) β gβ β f i β gβ β f i) β gβ β gβ