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 #-}
module cursed where
    open import Agda.Builtin.String
    open import IO
    postulate 
        ex' : String

        
    {-# FOREIGN GHC
        {-# LANGUAGE ForeignFunctionInterface #-}

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

bond15

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])

bond15

Require Import Program.Tactics.

Lemma prf (n : nat)(p : n = 0) : bool.
Admitted.

Program Definition huh(n : nat) : bool :=
  match n with
  | O => prf n _.   (* Program adds the equation `n = 0` to the context of this match branch which is pickec up by the implicit *) 
  | S n => true
end.

bond15

module modal where

open import Data.Unit
open import Data.Nat
open import Data.Product
open import Data.String
open import Data.Bool

open import Agda.Builtin.String