Proof of function extensionality using interval type.

Interval.agda

{-# OPTIONS --without-K #-}

module Interval where

-- https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/

data _≡_ {A : Set} (x : A) : A → Set where
    refl : x ≡ x

cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

module Interval where
    private
        data I' : Set where
            Zero : I'
            One  : I'

    I : Set
    I = I'

    zero : I
    zero = Zero

    one : I
    one = One

    I-rec : ∀ {A : Set} (x y : A) (p : x ≡ y) → I → A
    I-rec x y _ Zero = x
    I-rec x y _ One  = y

    postulate
        seg : zero ≡ one
        βseg : ∀ {A : Set} {x y : A} (p : x ≡ y)
            → cong (I-rec x y p) seg ≡ p

open Interval

extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x) → f ≡ g
extensionality {A} {B} {f} {g} α = cong h seg
    where
    h : I → A → B
    h i = λ x → I-rec (f x) (g x) (α x) i