Construct `compute-glue-cogap` from appropriate infrastructure
fredrik-bakke opened this issue · 0 comments
fredrik-bakke commented
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.