From 9b3a308c7248fd2fa94162e4401726327cc66aa3 Mon Sep 17 00:00:00 2001 From: Peter Mikkelsen Date: Wed, 23 Jun 2021 16:20:51 +0000 Subject: Add some agda test --- .../_tmp/agda-dfa/Agda.Primitive.Cubical.html | 55 ++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html (limited to 'sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html') diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html new file mode 100644 index 0000000..1be20f5 --- /dev/null +++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html @@ -0,0 +1,55 @@ + +Agda.Primitive.Cubical
{-# OPTIONS --cubical --no-subtyping #-}
+
+module Agda.Primitive.Cubical where
+
+{-# BUILTIN INTERVAL I  #-}  -- I : Setω
+
+{-# BUILTIN IZERO    i0 #-}
+{-# BUILTIN IONE     i1 #-}
+
+infix  30 primINeg
+infixr 20 primIMin primIMax
+
+primitive
+    primIMin : I → I → I
+    primIMax : I → I → I
+    primINeg : I → I
+
+{-# BUILTIN ISONE    IsOne    #-}  -- IsOne : I → Setω
+
+postulate
+  itIsOne : IsOne i1
+  IsOne1  : ∀ i j → IsOne i → IsOne (primIMax i j)
+  IsOne2  : ∀ i j → IsOne j → IsOne (primIMax i j)
+
+{-# BUILTIN ITISONE  itIsOne  #-}
+{-# BUILTIN ISONE1   IsOne1   #-}
+{-# BUILTIN ISONE2   IsOne2   #-}
+
+-- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ
+-- Partial i A = IsOne i → A
+
+{-# BUILTIN PARTIAL  Partial  #-}
+{-# BUILTIN PARTIALP PartialP #-}
+
+postulate
+  isOneEmpty : ∀ {ℓ} {A : Partial i0 (Set ℓ)} → PartialP i0 A
+
+{-# BUILTIN ISONEEMPTY isOneEmpty #-}
+
+primitive
+  primPOr : ∀ {ℓ} (i j : I) {A : Partial (primIMax i j) (Set ℓ)}
+            → (u : PartialP i (λ z → A (IsOne1 i j z)))
+            → (v : PartialP j (λ z → A (IsOne2 i j z)))
+            → PartialP (primIMax i j) A
+
+  -- Computes in terms of primHComp and primTransp
+  primComp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) {φ : I} (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1
+
+syntax primPOr p q u t = [ p ↦ u , q ↦ t ]
+
+primitive
+  primTransp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a : A i0) → A i1
+  primHComp  : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A
+
\ No newline at end of file -- cgit v1.2.3