{-# OPTIONS --cubical --without-K #-}
module Main where -- welcome to my home page
figure
module Information where -- my information
  open import HoTT 

module Misc where
    import Calendar     -- jump to see my schedule
    import Publication  -- jump to see my publications
    import Project      -- jump to see my projects

module SomeFun where
  open import HoTT 
  _has-univalent-axiom : (𝓤 : Universe)  𝓤  ̇
  𝓤 has-univalent-axiom = (X Y : 𝓤 ̇ )  is-equiv (Id→Eq X Y)