mirror of
https://github.com/Smaug123/CubicalTutorial
synced 2025-10-05 16:08:40 +00:00
15 lines
270 B
Agda
15 lines
270 B
Agda
{-# OPTIONS --safe --warning=error --without-K #-}
|
|
|
|
open import Agda.Primitive
|
|
|
|
module Basic where
|
|
|
|
data False : Set where
|
|
|
|
record True : Set where
|
|
|
|
data _||_ {a b : _} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
|
inl : A → A || B
|
|
inr : B → A || B
|
|
infix 1 _||_
|