Commit 2022-03-14 18:58 c1c61d44

View on Github →

feat(data/W/constructions): add constructions of W types (#12292) Here I write the naturals and lists as W-types and show that the definitions are equivalent. Any other interesting examples I should add?

Estimated changes

Modified src/data/W/basic.lean

Created src/data/W/constructions.lean

added def W_type.equiv_list

added def W_type.equiv_nat

added theorem W_type.left_inv_list

added theorem W_type.left_inv_nat

added inductive W_type.list_α

added def W_type.list_α_equiv_punit_sum

added def W_type.list_β

added inductive W_type.nat_α

added def W_type.nat_α_equiv_punit_sum_punit

added def W_type.nat_β

added def W_type.of_list

added def W_type.of_nat

added theorem W_type.right_inv_list

added theorem W_type.right_inv_nat

added def W_type.to_list

added def W_type.to_nat