(2022-06-25) メモ

Interval : Type
Path : (A : Type) -> A -> A -> Type
zero : Interval
one : Interval
segment : Path Interval zero one
abstract : (A : Type) -> (p : Interval -> A) -> Path A (p zero) (p one)
Interval_recursion : (P : Type) -> (constructor_zero : P) -> (constructor_one : P) -> (constructor_segment : Path P constuructor_zero constructor_one) -> Interval -> P
Path_recursion : (A : Type) -> (P : A -> A -> Type) -> (constructor_abstract : (p : Interval -> A) -> P (p zero) (p one)) -> (x : A) -> (y : A) -> Path A x y -> P x y
Path_recursion : (A : Type) -> (P : A -> A -> Type) -> (constructor_idpath : (x : A) -> P x x) -> (x : A) -> (y : A) -> Path A x y -> P x y