(* Title: HoTT/HoTT.thy Author: Josh Chen Load all the component modules for the HoTT logic. *) theory HoTT imports HoTT_Base Prod Sum begin \ \Maybe tactic setup can go in here?\ end