W types in idris please refer to the hott book on this topic,and https://github.com/agda/agda-stdlib/blob/master/src/Data/W.agda https://mazzo.li/epilogue/index.html%3Fp=324.html