fact: Definition local_indpaths {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).1.
imports: HoTT.Basics HoTT.Types Extensions ReflectiveSubuniverse Accessible