Invertegory is an intermediate structure between a category and a groupoid: every morphism has a formal inverse, but the inverse is not required to satisfy the groupoid inverse laws.

class LeanPool.Polylean.Invertegory (Obj : Sort u_1) extends LeanPool.Polylean.Category Obj : Sort (max u_1 (u_2 + 1))

A category equipped with formal inverses for all morphisms.

• hom : Obj → Obj → Sort u_2
• id (X : Obj) : X ⟶ X
• comp {X Y Z : Obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
• id_comp {X Y : Obj} (f : X ⟶ Y) : 𝟙 X ≫ f = f
• comp_id {X Y : Obj} (f : X ⟶ Y) : f ≫ 𝟙 Y = f
• comp_assoc {W X Y Z : Obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : (f ≫ g) ≫ h = f ≫ g ≫ h
• inv {X Y : Obj} : (X ⟶ Y) → (Y ⟶ X)

  Formal inverse of a morphism.

• invInv {X Y : Obj} (e : X ⟶ Y) : inv (inv e) = e

structure LeanPool.Polylean.Invertegory.Functor {C : Sort u_1} {D : Sort u_2} (ℭ : Invertegory C) (𝔇 : Invertegory D) extends ℭ.toCategory ⥤ 𝔇.toCategory : Sort (max (max (max (max 1 u_1) u_2) u_3) u_4)

A morphism of Invertegorys preserving formal inverses.

• obj : C → D
• map {X Y : C} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map_id (X : C) : self.map (𝟙 X) = 𝟙 (self.obj X)
• map_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (f ≫ g) = self.map f ≫ self.map g
• mapInv {X Y : C} {f : X ⟶ Y} : self.map (inv f) = inv (self.map f)