`{Univalence} {m n : trunc_index} {A : Type} (a0 : A) `{IsConnected m.+1 A} {B : Type} (b0 : B) `{IsConnected n.+1 B} (P : A -> B -> Type) {HP : forall a b, IsTrunc (m +2+ n) (P a b)} (fs : {f_a0 : forall b:B, P a0 b & { f_b0 : forall a:A, P a b0 & f_a0 b0 = f_b0 a0 }}) : forall (a : A) (b : B), P a b. Proof. destruct fs as [f_a0 [f_b0 f_a0b0]]. refine (wedge_incl_elim _ _ _ _ _ f_a0b0). Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.