search

pufferffish / agda-symmetries

MIT License
5 stars 1 forks source link

Useful lemmas #71

Closed pufferffish closed 8 months ago

pufferffish commented 8 months ago
  1. Tree on emptySig is Free #27
  2. Any type on emptyEqSig is Free #28
  3. Free objects on same set are isomorphic in #29
  4. Define empty and sum of signature #26