fact: Definition local_indpaths_beta {X} `{IsLocal f X} {i} (h k : lgen_codomain f i -> X) (p : h o f i == k o f i) s : local_indpaths p (f i s) = p s := (fst (snd (ooextendable_islocal i 2) h k) p).2 s.
imports: HoTT.Basics HoTT.Types Extensions ReflectiveSubuniverse Accessible