Lemma diagRecursion (f : nat -> nat -> Type) (init : ∏ n, f 0 n) (ind : ∏ m n, f m (S n) -> f (S m) n): ∏ m n, f m n. Proof. intros m. induction m as [|m H]. - exact init. - intros n. apply ind. apply H. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.