Skip to content

Instantly share code, notes, and snippets.

@bond15

bond15/cube.agda

Created July 17, 2021 00:11
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save bond15/f65183ea00222020f063c1f39f3cafcf to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save bond15/f65183ea00222020f063c1f39f3cafcf to your computer and use it in GitHub Desktop.
Download ZIP
Cubical Agda Int
Raw
cube.agda
{-# OPTIONS --cubical #-}
module cube where
open import Data.Nat
open import Cubical.Foundations.Prelude
data Int : Set where
pos : (n : ℕ) -> Int
neg : (n : ℕ) -> Int
z : pos 0 ≡ neg 0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment