fact: Definition wedge_incl_comp3 : wedge_incl_comp2 a0 = (wedge_incl_comp1 b0) @ f_a0b0 := isconn_wedge_incl.2.2.2.
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc