From Categories Require Export KanExt.LocalFacts.Uniqueness.
From Categories Require Export KanExt.LocalFacts.HomToCones.
From Categories Require Export KanExt.LocalFacts.ConesToHom.
From Categories Require Export KanExt.LocalFacts.NatIso.
From Categories Require Export KanExt.LocalFacts.From_Iso_Cat.
