<html><body><div style="color:#000; background-color:#fff; font-family:times new roman, new york, times, serif;font-size:12pt"><div><div><font face="'times new roman', 'new york', times, serif">The following definition looks reasonable to me,</font></div><div><font face="'times new roman', 'new york', times, serif">the type of the hole is reported as </font><span style="font-family: 'times new roman', 'new york', times, serif; ">ℕ </span><span style="font-family: 'times new roman', 'new york', times, serif; ">→ Set,</span></div><div><span style="font-family: 'times new roman', 'new york', times, serif; ">and refine/give accepts what I've written there,</span></div><div><span style="font-family: 'times new roman', 'new york', times, serif; ">but then typechecking the file fails, saying</span></div><div><span><font face="'times new roman', 'new york', times, serif">t true !=< ℕ of type Set</font><br></span></div><div><span><font
face="'times new roman', 'new york', times, serif"><br></font></span></div><div><span style="font-family: 'times new roman', 'new york', times, serif; ">module test where</span><br></div><div><font face="'times new roman', 'new york', times, serif">open import Data.Nat</font></div><div><font face="'times new roman', 'new york', times, serif">open import Data.Bool</font></div><div><font face="'times new roman', 'new york', times, serif">open import Data.Product</font></div><div><font face="'times new roman', 'new york', times, serif">open import Data.Vec</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">t : Bool → Set</font></div><div><font face="'times new roman', 'new york', times, serif">t true = ℕ</font></div><div><font face="'times new roman', 'new york', times, serif">t false = Σ (t true) {!Vec Bool!}</font></div><div><font face="'times new
roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">Why isn't this definition accepted?</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">Brandon</font></div></div></div></body></html>