{- Interval Type:
   Copyright (c) Groupoid Infinity, 2014-2018.

   HoTT 6.3 The interval -}

module interval where
import equiv
import iso
import prop

-- I = (X:U) -> isSet X -> (x y: X) -> Path X x y -> X

data I = i0
       | i1
       | seg <i> [(i=0) -> i0,
                  (i=1) -> i1]

pathToHtpy (A: U) (x y: A) (p: Path A x y): I -> A
   = split { i0 -> x; i1 -> y; seg @ i -> p @ i }

-- H_{f,g:X→Y}: X × [0,1] → Y,  f(x)=g(x)
homotopy  (X Y: U)
          (f g: X -> Y)
          (p: (x: X) -> Path Y (f x) (g x))
          (x: X): I -> Y = pathToHtpy Y (f x) (g x) (p x)

-- Proof of funext from the interval
fext (A B: U) (f g: A -> B) (p: (x: A) -> Path B (f x) (g x)): Path (A -> B) f g
   = <j> (\(x : A) -> homotopy A B f g p x (seg{I} @ j))

toUnit : I -> unit = split { i0 -> tt; i1  -> tt; seg @ i -> tt }
fromUnit : unit -> I = split tt -> i0
toUnitK : (a : unit) -> Path unit (toUnit (fromUnit a)) a = split tt -> <i> tt
fromUnitK : (a : I) -> Path I (fromUnit (toUnit a)) a
   = split { i0 -> <i> i0; i1 -> <i> seg {I} @ i; seg @ i -> <j> seg {I} @ i /\ j }

unitEqI: Path U unit I = isoPath unit I fromUnit toUnit fromUnitK toUnitK
propI: isProp I = subst U isProp unit I unitEqI propUnit

T: U = Path I i0 i0
p0: T = refl I i0
test: T = propI i0 i0