title: Differences between Coq and Agda
body: <p>What are each of these programs designed for and what does each offer other the other? Also, are both systems consistent, and moreover, are they based on some foundational mathematical theory?</p>
  
  <p>Two things I care about:</p>
  
  <ol>
  <li>Easy to install</li>
  <li>Easy to learn</li>
  </ol>
  
  <p>I've search and what I've read seems very polarized, I would like to know their differences from the most objective (humanly) possible perspective.</p>