fact: Definition local_rec {X} `{IsLocal f X} {i} (g : lgen_domain f i -> X) : lgen_codomain f i -> X := (fst (ooextendable_islocal i 1%nat) g).1.
imports: HoTT.Basics HoTT.Types Extensions ReflectiveSubuniverse Accessible