Issue2790-b.agda:7,1-21
Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
  Reason: WithKEnabled
when checking the definition of uip
Issue2790-b.agda:7,1-21
Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
  Reason: WithKEnabled
when checking the definition of uip
Issue2790-b.agda:1,1-42
Cannot set OPTIONS pragma --cubical and --with-K with safe flag.
