I'm looking to model data inputs for an artificially intelligent system, which is affected by its internal parts and has feedback loops. I'd like to model it mathematically, using category theory or homotopy type theory.

Is Agda or Idris the best choice for such modelling?

  • $\begingroup$ I suspect you're going to need to edit the question to make it clearer what you're asking. I am not clear on what it means "to have data inputs mathematically interpreted and modeled in [..]". That sounds vague to me. It also sounds too broad. What specific problem are you trying to solve? Can you give a concrete example? Asking for language recommendations sounds like a matter of opinion and hence not a good fit here. What is "best" is a matter of opinion. See cs.stackexchange.com/help/dont-ask. $\endgroup$
    – D.W.
    Commented Apr 27, 2021 at 19:35
  • $\begingroup$ I see that you've received similar feedback before. When you get feedback, that's a great opportunity to improve your question by editing it to provide further context. This makes it more likely you'll get an answer that is useful to you, and more likely that it'll meet our quality standards. $\endgroup$
    – D.W.
    Commented Apr 27, 2021 at 19:36

1 Answer 1


Agda is definitely the better choice if you're doing Homotopy Type Theory.

  1. Idris has several features that are specifically incompatible with HoTT. Specifically, you can use dependent pattern matching to prove Uniqueness of Identity Proofs (UIP), which, when combined with Univalence, allows you to prove False. There's also a type-case feature which you can use to directly prove False from univalence.
  2. Agda has some features that are specifically designed to enable HoTT. Namely, it has a --without-K option, which ensures that you can't prove UIP or the related Axiom K. There's also a whole language extension for Cubical Type Theory, which uses a special notion of equality gives computational meaning to univalence.

Relevant reading:

Introduction to Univalent Foundations in Agda

Pattern Matching without K

Proof-relevant Unification in Agda

Cubical Agda Paper

Cubical Agda documentation

Cubical Agda tutorial


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.