Setoids in AgdaSetoid is a record type in Agda, and it appears everywhere from Relation.Binary.EqReasoning to Algebra. But, why do we need such a type ? After reading “setoids in type theory”, I thought that setoids are used for mathematical constructions like subset, quotients in the intensional type theory and the Calculus of Inductive Construction. Since some of functional data structure could be represented
