{- Bishop Equivalence:
   - Equivalence Classes.
   Copyright (c) Groupoid Infinity, 2017-2018. -}

module bishop where
import proto
import subtype
import path

-- Propositional Equality By Errett Bishop
hrel       (X: U): U = X -> X -> PROP
isrefl     (X: U) (R: hrel X): U = (x: X) -> (R x x).1
issymm     (X: U) (R: hrel X): U = (x1 x2: X) -> (R x1 x2).1 -> (R x2 x1).1
istrans    (X: U) (R: hrel X): U = (x1 x2 x3: X) -> (R x1 x2).1 -> (R x2 x3).1 -> (R x1 x3).1
ispreorder (X: U) (R: hrel X): U = prod (istrans X R) (isrefl X R)
iseqrel    (X: U) (R: hrel X): U = prod (ispreorder X R) (issymm X R)
eqrel      (X: U) : U = (R: hrel X) * (iseqrel X R)
eqrelrefl  (X: U) (R: eqrel X): isrefl X R.1 = R.2.1.2
eqrelsymm  (X: U) (R: eqrel X): issymm X R.1 = R.2.2
eqreltrans (X: U) (R: eqrel X): istrans X R.1 = R.2.1.1

iseqrelpair (A B: U) (R0: hrel A) (R1: hrel B) (E0: iseqrel A R0) (E1: iseqrel B R1): iseqrel (prod A B) (hrelpair A B R0 R1)
 = ((tax, rax), sax) where
    T : U = prod A B
    R : hrel T = hrelpair A B R0 R1
    rax : isrefl T R = \ (t0 : T) -> (E0.1.2 t0.1, E1.1.2 t0.2)
    sax : issymm T R = \ (t0 t1 : T) (e : (R t0 t1).1) -> (E0.2 t0.1 t1.1 e.1, E1.2 t0.2 t1.2 e.2)
    tax : istrans T R = \ (t0 t1 t2 : T) (e0 : (R t0 t1).1) (e1 : (R t1 t2).1) ->
                          (E0.1.1 t0.1 t1.1 t2.1 e0.1 e1.1, E1.1.1 t0.2 t1.2 t2.2 e0.2 e1.2)

eqrelpair (A B : U) (R0 : eqrel A) (R1 : eqrel B) : eqrel (prod A B)
  = (hrelpair A B R0.1 R1.1, iseqrelpair A B R0.1 R1.1 R0.2 R1.2)

iseqclasspair (A B : U) (R0 : hrel A) (R1 : hrel B) (H0 : hsubtypes A)
    (H1 : hsubtypes B) (E0 : iseqclass A R0 H0) (E1 : iseqclass B R1 H1)
  : iseqclass (prod A B) (hrelpair A B R0 R1) (hsubtypespair A B H0 H1)
  = let
    H : hsubtypes (prod A B) = hsubtypespair A B H0 H1
    a (P : PROP) (f : carr (prod A B) H -> P.1) : P.1
      = let
        g (x0 : carr A H0) : P.1 = let h (x1 : carr B H1) : P.1 = f ((x0.1, x1.1), (x0.2, x1.2)) in E1.1.1 P h
      in E0.1.1 P g
    b (x0 x1 : prod A B) (r : (hrelpair A B R0 R1 x0 x1).1) (h0 : (H x0).1) : (H x1).1
      = (E0.1.2 x0.1 x1.1 r.1 h0.1, E1.1.2 x0.2 x1.2 r.2 h0.2)
    c (x0 x1 : prod A B) (h0 : (H x0).1) (h1 : (H x1).1) : (hrelpair A B R0 R1 x0 x1).1
      = (E0.2 x0.1 x1.1 h0.1 h1.1, E1.2 x0.2 x1.2 h0.2 h1.2)
  in ((a, b), c)