fact: Definition path2_universe_1 {A B : Type} (f : A <~> B) : @path2_universe _ _ f f (fun x => 1) = 1 := equiv_path2_universe_1 f.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod