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

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

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

	{-# OPTIONS --rewriting #-}

	module cont-cwf where

	open import Agda.Builtin.Sigma
	open import Agda.Builtin.Unit
	open import Agda.Builtin.Bool
	open import Agda.Builtin.Nat
	open import Data.Empty
	import Relation.Binary.PropositionalEquality as Eq

	module Presentation where

	{-


	Topics
	Agda
	Cubical Agda
	Interval / Paths
	Univalence

	module FinClosureEx where
	open import Agda.Primitive
	open import Data.Bool
	open import Data.Fin
	open import Data.List
	open import Data.Nat
	open import Data.Product
	open import Function.Base

	private

	Require Import PeanoNat.
	Require Import Coq.Logic.Eqdep_dec.
	Import EqNotations.
	Require Import Coq.Logic.JMeq.


	Infix "==" := JMeq (at level 70, no associativity).

	Print JMeq.
	Print eq.

	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

	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.

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

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