{X} `{IsLocal f X} {i} {h k : lgen_codomain f i -> X} (p : h o f i == k o f i) : h == k := (fst (snd (ooextendable_islocal i 2) h k) p).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.