{- 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=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 = (\(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 -> tt fromUnitK : (a : I) -> Path I (fromUnit (toUnit a)) a = split { i0 -> i0; i1 -> seg {I} @ i; seg @ i -> 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