wedge_incl_comp2 a0 = (wedge_incl_comp1 b0) @ f_a0b0 := isconn_wedge_incl.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.