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  = ⊤

Function extensionality is not derivable in Agda or Coq. It can be postulated as an axiom that is consistent with the theory, but you cannot construct a term for the type representing function extensionality.

In Cubical Agda it is derivable and it has a tauntingly concise definition. (removing Level for a moment since that is tangental)

funext : {A B : Set}{f g : A → B} → (∀ (a : A) → f a ≡ g a) → f ≡ g
funext p i a = p a i

That said, there is a fair amount to unpack to understand what is going on here.

Cubical Agda adds an abstract Interval Type I which has two endpoints i0 and i1. (see footnote [1])

	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

	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

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

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

	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₂

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

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

	open import Function

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

	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

	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}}

	{-# 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