open import Paths

// Also known as "Interval" in the HoTT book
open data Segment
| left | right
| seg : left = right

def uniqueness (b : Segment) : left = b
| left ⇒ idp
| right ⇒ \i ⇒ seg i
| seg i ⇒ \j ⇒ seg (i ∧ j)
def isContrSegment : isContr Segment ⇒ (_, uniqueness)

// The induction principle for Segment implies funExt. Here is a lemma.
private def funExt-lemma {A B : Type} (f g : A → B) (p : ∀ x → f x = g x) : Segment → A → B
// | f, g, p, left => f
// | f, g, p, right => g
| f, g, p, left, a ⇒ f a
| f, g, p, right, a ⇒ g a
| f, g, p, seg i, a ⇒ p a i

// Using theorems in MLTT and funExt-lemma to derive funExt
example def funExt' {A B : Type} (f g : A → B) (p : ∀ x → f x = g x) : f = g
  ⇒ pmap (funExt-lemma f g p) seg