1
$\begingroup$

Which is better for programming benifiting by Homotopy type theory(HoTT),Idris or Agda.compare them.

$\endgroup$
4
  • 2
    $\begingroup$ Hi Ali S; while non-basic HoTT questions would generally be welcome here if they were about the content of HoTT, programming questions are not generally considered on topic here. For such questions, you could try computer science stack exchange. $\endgroup$
    – Alec Rhea
    Apr 27, 2021 at 11:02
  • 4
    $\begingroup$ This question is very similar to your since-deleted question from yesterday. It would be preferable for you to edit that question and nominate it for reopening rather than deleting that question and asking a new, lightly edited version. At any rate, the difference now is that you have listed exactly which HoTT-related languages you'd like to be compared. I suspect this is still too broad for a MO question, and I think our HoTT experts will probably confirm this. $\endgroup$
    – Tim Campion
    Apr 27, 2021 at 11:16
  • 3
    $\begingroup$ I’m voting to close this question because it is a CS topic, not maths topic. Please use an appropriate forum instead. $\endgroup$ Apr 27, 2021 at 11:19
  • 2
    $\begingroup$ As Peter LeFanu Lumsdaine explained on the deleted question, part of what makes the question too broad is that you have not explained anything about your background or about what your goals for using such software would be. $\endgroup$
    – Tim Campion
    Apr 27, 2021 at 11:37

0