Induction principle for smash product

agda / cubical

An experimental library for Cubical Agda

Other

441 stars 134 forks source link

Closed aljungstrom closed 5 months ago

aljungstrom commented 5 months ago

Contains:

New induction principle for smash products: ⋀̃→⋀-ind in Cubical.HITs.SmashProduct.Induction
Changed of a typo in Cubical.HITs.SmashProduct.Base ('3' to '2')
Added finite families of types (needed for first point)
Updated related paper file.