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

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

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

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

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

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

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

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

open import Function

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

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

record LDepDialSet {ℓ : Level}{L : Set ℓ} : Set (lsuc ℓ) where 
    field 
        pos : Set ℓ
        dir : pos → Set ℓ
        α : (p : pos) → dir p → L

open import Lineale
record LDepDialSetMap {ℓ}{L} (A B : LDepDialSet{ℓ}{L})
        {{pl : Proset L}}
        {{_ : MonProset L}}

bond15

{-# OPTIONS --guardedness --type-in-type #-}
module cursed where
    open import Agda.Builtin.String
    open import IO
    postulate 
        ex' : String

    {-# FOREIGN GHC
        {-# LANGUAGE ForeignFunctionInterface #-}
        import Data.Text

bond15

    open import Data.Bool
    open import Data.Unit 
    open import Data.Empty
    open import Cubical.Core.Everything 

    ty : Bool → Set 
    ty false = ⊥
    ty true  = ⊤