Funext_downward_closed@{i j max i' j' max' | i <= max, j <= max, i' <= max', j' <= max', i' <= i, j' <= j} `{H : Funext_type@{i j max}} : Funext_type@{i' j' max'}. Proof. hnf in *. exact (fun A P => H A P). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Metatheory.Core.