Tealeaves.Functors.Pathspace

This file defines the pathspace functor which maps a type A to the set of proofs of equality between any two terms of A.

From Tealeaves Require Export
Classes.Categorical.Applicative.

Pathspace Applicative Functor

Inductive PathSpace (A: Type): Type :=
| path: ∀ (x y: A), x = y → PathSpace A.

#[export] Instance Map_Path: Map PathSpace :=
  fun A B (f: A → B) '(@path _ x y p)
  ⇒ @path _ (f x) (f y) (ltac:(subst; auto)).

#[export, program] Instance Path_End: Functor PathSpace.

Solve All Obligations with
  (intros; ext [? ?]; now destruct e).

Applicative Instance

#[export] Instance Pure_Path: Pure PathSpace :=
  fun (A: Type) (a: A) ⇒ @path A a a eq_refl.

#[export] Instance Path_Mult: Mult PathSpace :=
  ltac:(refine
          (fun A B '(@path _ a1 a2 eqa , @path _ b1 b2 eqb ) ⇒
             @path _ (a1 , b1 ) (a2 , b2 ) _); subst; reflexivity).

#[export, program] Instance App_Path: Applicative PathSpace.

Solve All Obligations with
  (intros; now repeat (match goal with
                       | x: PathSpace ?A |- _ ⇒
                           destruct x; subst end)).