This is a repository of my worked solutions when trying to understand more mathematics.
I have also included some agda code here. This repository will also store agda code for proofs since I am trying to learn how to write cubical agda.
Agda installation https://agda.readthedocs.io/en/latest/getting-started/installation.html
HoTT game installation https://thehottgameguide.readthedocs.io/en/latest/getting-started/about-hott-game.html#installing-agda-and-the-cubical-agda-library
Interactive agda - https://sites.google.com/view/lorenzoclemente/teaching/logic-for-computer-scientists-summer-semester-2018-2019
- comments
- given by -- syntax
- natural number definition
- successor function
- equality
- symbol N
- need simpler tactic
- helper / lemma
- if x ≡ y then f x ≡ f y
- underscores
- function type arrows
- pattern matching
- Set
- implict arguments
- dependent types
- reflexivity
- congruences
- induction