By reading "The little typer" to fully understand the dependent type. Will file questions we met in issue and answering it if we understand it.