Find the right infrastructure to make the construction of compute-glue-cogap just an application of a more general construction. The current construction is very almost coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family, but an apd-constant-type-family has snuck its way into the proof.
Find the right infrastructure to make the construction of
compute-glue-cogapjust an application of a more general construction. The current construction is very almostcoherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family, but anapd-constant-type-familyhas snuck its way into the proof.