Need help in Agda programming

only need to do this part: 2 Internal Verification The file [login to view URL] defines an internally verified data type for sorted lists. A value of type sorted-list l u is a list which is guaranteed (statically, by type checking) to be in sorted order, and with all data between lower bound l and upper bound u. 1. Fill in the definition of sorted-list-to-L so that you get out a simple list of the data in the input sorted-list [10 points]. 2. Fill in the code for relax-lb and relax-ub, so that you get back a list with the same data as the input list, but with the lower bound, or upper bound, respectively, relaxed as indicated by the type. [10 points each] 3. Define a function for appending sorted lists. You get 5 points just for the type of the function, and 10 more points for the code. 4. Define a function for inserting a piece of data into a sorted list (in the correct position to preserve being sorted). [15 points] 5. Fill in the definition of insert-sort so that it returns a sorted version of the input list, by calling your function for inserting a piece of data into a sorted list. [5 points (just because we are over 60 points with this one)] You can test your code with concrete data; see [login to view URL] (though this cannot be loaded until you fill or comment out the code with holes in [login to view URL]).