module Information where -- my information
  open import HoTT 

• Phone : +1-585-301-0796
• Personal Email : i [at] zhuyi [dot] fan
• Work Email : yifanzhu [at] rochester [dot] edu
• School Office : 3602 Wegmans Hall
• Twitter : ZhuSchrodinger
• Telegram : schrodingerzhu
• Github: SchrodingerZhu
• Position: Full Time Ph.D. Student
• Advisor: Prof. Chen Ding

  postulate
    ZYF : Set
    ZYF-singleton : is-singleton ZYF
    WorkEmail : Set
  FindMe = λ (x : WorkEmail) → center ZYF ZYF-singleton

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)