Theorems · Inductive type · category theory

CategoryTheory.IsCofiltered

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop

A category IsCofiltered if 1. for every pair of objects there exists another object "to the left", 2. for every pair of parallel morphisms there exists a morphism to the left so the compositions are equal, and 3. there exists some object.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

133 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category