{- 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)