Skip to content

Instantly share code, notes, and snippets.

@bond15

bond15/hit.agda

Created September 2, 2022 04:40
Show Gist options
  • Save bond15/8693422165ab3ff2723a6979254b354e to your computer and use it in GitHub Desktop.
Save bond15/8693422165ab3ff2723a6979254b354e to your computer and use it in GitHub Desktop.
Download ZIP
S1
Raw
hit.agda
data S₁ : Set where
base : S₁
loop : base ≡ base
_ : S₁
_ = base
_ : S₁
_ = loop i0
_ : S₁
_ = loop i1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment