bond15

open import Data.Nat
open import Data.Bool hiding(_<?_)
open import Level hiding (suc)

data ⊥ {ℓ : Level} : Set ℓ where

data type : Set where
  𝕦 𝕓 𝕟 : type

--P : Set

bond15

{-# OPTIONS --overlapping-instances #-}

record _<:_ (sub sup : Set) : Set where
  field
    inj : sub → sup

open import Function

open _<:_{{...}}

bond15

open import Data.Product
postulate
  P₁ P₂ P₃ : Set
  T₁ : P₁ → Set
  T₂ : P₂ → Set
  T₃ : P₃ → Set
  f₁ : P₁ → P₂
  f₂ : P₂ → P₃
  f₁⁻¹ : P₂ → P₁
  f₂⁻² : P₃ → P₂

bond15

record Univ : Set₁ where
  field
    U : Set
    El : U → Set
open Univ

record GeneralizedElement : Set₁ where
   constructor _∋_∋_
   field
    𝒰 : Univ

bond15

module foo where 
    data ⊘ : Set where
    data ⊤ : Set where tt : ⊤
    open import Cubical.Data.Bool
    open import Cubical.Foundations.Isomorphism  
    open import Cubical.Foundations.Prelude 
 
    postulate 
        f : Set → Bool
        reduction₁ : f (⊤ × ⊤) ≡ true

bond15

module Multiverse where 


module types where 
    open import Data.Nat 
    open import Data.String 
    open import Data.Bool 
    open import Data.Product

    data Type₁ : Set where 

bond15

record Poly : Set₁ where
  constructor _◂_◂_ 
  field
    pos : Set
    dir : pos → Set
    α : (p : pos)(d : dir p) → Set

open import Data.Product
 
_⇒_ : Poly → Poly → Poly

bond15

    data S₁ : Set where 
        base : S₁
        loop : base ≡ base

    _ : S₁ 
    _ = base 

    _ : S₁ 
    _ = loop i0

bond15

Module Type AT.
Parameter x : nat.
End AT.

Module A (Import a : AT).
Include a.
Definition y := a.x.

End A.
Print A.

bond15

In Granule (the base calculus is linear) these two tests violate linearity:

data Foo a = Bar a

test1 : Foo Int -> (Int , Int)
test1 (Bar mustUseOnce) = (mustUseOnce, mustUseOnce)

test2 : Foo Int -> Int
test2 (Bar mustUseOnce) = 42