So in homotopy type theory, dependent types correspond to fibrations and identity types correspond to path spaces. Why are these two correspondences the only ones explicitly mentioned in every source for homotopy type theory? Can the homotopy theoretical equivalences of other named types be constructed from these two? I am fairly new to these ideas and am trying to get a high level overview.