@[reducible, inline]

abbrev AlgebraicTopologyI.Iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X Y : C) : Type u_2

Definition 3.2 (Isomorphism). An isomorphism in a category C, in the sense of Miller's Lectures on Algebraic Topology I: a morphism with a two-sided inverse, packaged as a structure recording both the morphism and its inverse together with the inversion equations. This is a thin wrapper around Mathlib's CategoryTheory.Iso.

@[reducible, inline]

abbrev AlgebraicTopologyI.IsIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) : Prop

The Mathlib class witnessing that a morphism f is an isomorphism in the sense of Definition 3.2, i.e. there exists a two-sided inverse. This is a thin wrapper around CategoryTheory.IsIso.

@[reducible, inline]

abbrev AlgebraicTopologyI.NatTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (F G : CategoryTheory.Functor C D) : Type (max u_1 u_4)

Definition 3.5 (Natural transformation). A natural transformation θ : F ⟶ G between two functors F, G : C ⥤ D, in the sense of Miller's Lectures on Algebraic Topology I: a family of morphisms θ_X : F X ⟶ G X satisfying the naturality squares. This is a thin wrapper around Mathlib's CategoryTheory.NatTrans.