Is Agda sound as a proof system?

I was browsing Agda's stdlib source code, since I was trying to get into it seriously and therefore wanted to know more. I was amazed at that Agda is way more developed than I thought and it's significantly much closer to Haskell than Coq.

However, I was quite a bit panicked when I see some code like following:

toList∘fromList : ∀ s → toList (fromList s) ≡ s
toList∘fromList s = trustMe


It seems there is an observable hole in the system, and it means Agda is not entirely built from ground up by axiomization. Then I saw this,

https://github.com/agda/agda-stdlib/blob/master/src/Data/Colist.agda

data Colist {a} (A : Set a) : Set a where
[]  : Colist A
_∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A


I took Colist is the same as List in Haskell, allowing optionally infinite length, and from Wiki https://agda.readthedocs.io/en/v2.5.3/language/coinduction.html

The type constructor ∞ can be used to prove absurdity!

Just as I suspected, optional infinity introduces absurdity. To this point, I felt I was more scared than amazed.

I understand that being practical must come with some trade off. However, Agda is more or less considered as a proof system, arguably more than a progarmming language. There are lots of papers these days are based on Agda. However, a quick code scan has shown holes in many disguises. (Sure Coq also has that, but it's considerably easy to discover: just grep axiom, admit will tell a lot, and Coq supports printing axioms for each lemma.)

Since I am trying to enter Agda, I have no idea what I should expect from it. So the title says all my question: are the system and the results based on it, sound?

• really nobody wants to answer this question? – Jason Hu Mar 22 '18 at 16:17
• is it a good idea to ask this question on cstheory, in case there can be more attention on that platform. – Jason Hu Mar 22 '18 at 16:29
• I encourage you to have some more patience. This is a small site; sometimes it can take a few days for people to see the question. You could consider setting a bounty if you want to try to gather more attention to the question, but I'd recommend just giving it a little time. – D.W. Mar 23 '18 at 0:55
• Cross-posted: cstheory.stackexchange.com/q/40439/5038, cs.stackexchange.com/q/89611/755. Please do not post the same question on multiple sites. Each community should have an honest shot at answering without anybody's time being wasted. – D.W. Mar 23 '18 at 0:55