--#include "Pi.agda" --#include "Prod.agda" -- Definition of Id types -- --------------------------------------------------------------------------- package EQ_ (|X::Con_o) (A::Ty_o X) where AA :: Ty_o X = Prod A A XA :: Con_o = Compr X A XAA :: Con_o = Compr X AA EQ_fm_set (xab::XAA.set) :: Set = let x = xab.fst a = xab.snd.fst b = xab.snd.snd in (A.fm x).eq a b EQ :: Ty_o XAA = struct fm = \(xab::XAA.set) -> mk_triv (EQ_fm_set xab) subst = \(xab::XAA.set) |-> \(yab'::XAA.set) |-> \(pqr::XAA.eq xab yab')-> let x = xab.fst a = xab.snd.fst b = xab.snd.snd y = yab'.fst a' = yab'.snd.fst b' = yab'.snd.snd Ay = A.fm y p :: X.eq x y = pqr.fst q :: Ay.eq ((A.subst (x_i p)).fn a) a' = pqr.snd.fst r :: Ay.eq ((A.subst (x_i p)).fn b) b' = pqr.snd.snd in struct fn = \(e::(A.fm x).eq a b)-> Ay.trans (Ay.sym q) (Ay.trans ((A.subst (x_i p)).resp e) r) resp = \(e1::(A.fm x).eq a b) |-> \(e2::(A.fm x).eq a b) |-> \tt -> tt@_ reflS = \(xab::XAA.set)-> \(e::(fm xab).set) -> (fm xab).refl e transS = \(x::XAA.set) |-> \(y::XAA.set) |-> \(z::XAA.set) |-> \(p::XAA.eq x y) -> \(q::XAA.eq y z)-> \(e::(fm x).set)-> (fm x).refl e -- (x,a) -> (x,a,a) w :: Con_m XA XAA = let lem1 ::Con_m XA X = c_fst c_id lem2 ::Tm_o XA (Ty_m lem1 A) = c_snd c_id lem3 ::Tm_o XA (Ty_m lem1 (Prod A A)) = prod_pair lem2 lem2 in c_pair lem1 lem3 EQ' :: Ty_o XA = Ty_m w EQ Refl0 :: Set = Tm_o XA EQ' Refl :: Set = Tm_o X (Pi A EQ') refl0 :: Refl0 = struct tm = \(xa::XA.set) -> (A.fm xa.fst).refl xa.snd resp = \(xa::XA.set) |-> \(yb::XA.set) |-> \(pq::XA.eq xa yb) -> tt@_ refl :: Refl = lam refl0 EQ (|X::Con_o) (A::Ty_o X) :: Ty_o (Compr X (Prod A A)) = (EQ_ A).EQ refl0 (|X::Con_o) (A::Ty_o X) :: (EQ_ A).Refl0 = (EQ_ A).refl0 refl (|X::Con_o) (A::Ty_o X) :: (EQ_ A).Refl = (EQ_ A).refl -- --------------------------------------------------------------------------- package EQ_subst_ (|X::Con_o) (A::Ty_o X) (B::Ty_o (Compr X A)) where AA :: Ty_o X = Prod A A XA :: Con_o = Compr X A XAA :: Con_o = Compr X AA -- (x,a,b,q) -> (x,a) w1 :: Con_m (Compr XAA (EQ A)) XA = let lem1 :: Con_m (Compr XAA (EQ A)) XAA = c_fst c_id lem2 :: Con_m XAA X = c_fst c_id lem3 :: Tm_o XAA (Ty_m lem2 AA) = c_snd c_id lem4 :: Con_m XAA XA = c_pair lem2 (prod_fst |XAA |(Ty_m lem2 A) |(Ty_m lem2 A) lem3) in lem4 `c_o` lem1 -- (x,a,b,q,y) -> (x,b) w2 :: Con_m (Compr (Compr XAA (EQ A)) (Ty_m w1 B)) XA = let lem1 :: Con_m (Compr (Compr XAA (EQ A)) (Ty_m w1 B)) XAA = c_fst c_id `c_o` c_fst c_id lem2 :: Con_m XAA X = c_fst c_id lem3 :: Tm_o XAA (Ty_m lem2 A) = prod_snd |XAA |(Ty_m lem2 A) |(Ty_m lem2 A) (c_snd c_id) in (c_pair lem2 lem3) `c_o` lem1 Subst0 :: Set = Tm_o (Compr (Compr XAA (EQ A)) (Ty_m w1 B)) (Ty_m w2 B) Subst :: Set = Tm_o X (Pi (Prod A A) (Pi (EQ A) (Pi (Ty_m w1 B) (Ty_m w2 B)))) subst0 :: Subst0 = struct tm :: (xabqy::(Compr (Compr XAA (EQ A)) (Ty_m w1 B)).set)-> ((Ty_m w2 B).fm xabqy).set = \(xabqy::(Compr (Compr XAA (EQ A)) (Ty_m w1 B)).set)-> let xabq :: (Compr XAA (EQ A)).set = xabqy.fst x :: X.set = xabq.fst.fst a :: (A.fm x).set = xabq.fst.snd.fst b :: (A.fm x).set = xabq.fst.snd.snd q :: (A.fm x).eq a b = xabq.snd y :: ((Ty_m w1 B).fm xabq).set = xabqy.snd in (B.subst (right |X |A q)).fn y resp :: (xabqy ::(Compr (Compr XAA (EQ A)) (Ty_m w1 B)).set) |-> (xabqy'::(Compr (Compr XAA (EQ A)) (Ty_m w1 B)).set) |-> (p::(Compr (Compr XAA (EQ A)) (Ty_m w1 B)).eq xabqy xabqy') -> ((Ty_m w2 B).fm xabqy').eq (((Ty_m w2 B).subst |xabqy |xabqy' (x_i p)).fn (tm xabqy)) (tm xabqy') = \(xabqy ::(Compr (Compr XAA (EQ A)) (Ty_m w1 B)).set) |-> \(xabqy'::(Compr (Compr XAA (EQ A)) (Ty_m w1 B)).set) |-> \(p::(Compr (Compr XAA (EQ A)) (Ty_m w1 B)).eq xabqy xabqy')-> let xabq :: (Compr XAA (EQ A)).set = xabqy.fst x :: X.set = xabq.fst.fst a :: (A.fm x).set = xabq.fst.snd.fst b :: (A.fm x).set = xabq.fst.snd.snd q :: (A.fm x).eq a b = xabq.snd y :: ((Ty_m w1 B).fm xabq).set = xabqy.snd xabq' :: (Compr XAA (EQ A)).set = xabqy'.fst x' :: X.set = xabq'.fst.fst a' :: (A.fm x').set = xabq'.fst.snd.fst b' :: (A.fm x').set = xabq'.fst.snd.snd q' :: (A.fm x').eq a' b' = xabq'.snd y' :: ((Ty_m w1 B).fm xabq').set = xabqy'.snd lem1 :: Con_m_eq ((Ty_m w2 B).subst |xabqy |xabqy' (x_i p) `c_o` B.subst (right |X |A q)) (B.subst (right |X |A q') `c_o` (Ty_m w1 B).subst |xabq |xabq' (x_i p.fst)) = squareS |XA |B (right |X |A q) (w2.resp |xabqy |xabqy' (x_i p)) (w1.resp |xabq |xabq' (x_i p.fst)) (right |X |A q') lem2 :: (B.fm (mk_xa |X |A x' b')).eq ((B.subst (right |X |A q')).fn (((Ty_m w1 B).subst |xabq |xabq' (x_i p.fst)).fn y)) ((B.subst (right |X |A q')).fn y') = (B.subst (right |X |A q')).resp p.snd in (B.fm (mk_xa |X |A x' b')).trans (lem1 y) lem2 subst :: Subst = lam (lam (lam subst0)) subst0 (|X::Con_o) (A::Ty_o X) (B::Ty_o (Compr X A)) :: (EQ_subst_ A B).Subst0 = (EQ_subst_ A B).subst0 subst (|X::Con_o) (A::Ty_o X) (B::Ty_o (Compr X A)) :: (EQ_subst_ A B).Subst = (EQ_subst_ A B).subst -- --------------------------------------------------------------------------- package EQ_reflS_ (|X::Con_o) (A::Ty_o X) (B::Ty_o (Compr X A)) where XA :: Con_o = Compr X A XAA :: Con_o = Compr X (Prod A A) XAB :: Con_o = Compr XA B w1 :: Con_m XA XAA = let lem1 ::Con_m XA X = c_fst c_id lem2 ::Tm_o XA (Ty_m lem1 A) = c_snd c_id lem3 ::Tm_o XA (Ty_m lem1 (Prod A A)) = prod_pair lem2 lem2 in c_pair lem1 lem3 -- (x,a) -> (x,a,a,refl a) w2 :: Con_m XA (Compr XAA (EQ A)) = c_pair w1 (refl0 A) -- (x,a,y) -> (x,a) w3 :: Con_m XAB XA = c_fst c_id -- (x,a,y) -> (x,a,a,refl a) w4 :: Con_m XAB (Compr XAA (EQ A)) = w2 `c_o` w3 tmp1 :: Tm_o XAB (Ty_m w4 (Ty_m (EQ_subst_ A B).w1 B)) = c_snd c_id w5 :: Con_m XAB (Compr (Compr XAA (EQ A)) (Ty_m (EQ_subst_ A B).w1 B)) = c_pair w4 tmp1 tmp2 :: Tm_o (Compr (Compr XAA (EQ A)) (Ty_m (EQ_subst_ A B).w1 B)) (Ty_m (EQ_subst_ A B).w2 B) = subst0 A B tmp3 :: Tm_o XAB (Ty_m w3 B) = Tm_m w5 tmp2 tmp4 :: Tm_o XAB (Ty_m w3 B) = c_snd c_id tmp5 :: Tm_o XAB (Ty_m w3 (Prod B B)) = prod_pair tmp3 tmp4 -- (x,a,y) -> (x, B.subst A.refl(a) y, y) w :: Con_m XAB (Compr XA (Prod B B)) = c_pair w3 tmp5 ReflS0 :: Set = Tm_o XAB (Ty_m w (EQ B)) ReflS :: Set = Tm_o X (Pi A (Pi B (Ty_m w (EQ B)))) reflS0 :: ReflS0 = struct tm :: (xay::XAB.set)-> (B.fm xay.fst).eq ((B.subst (x_i (XA.refl xay.fst))).fn xay.snd) xay.snd = \(xay::XAB.set)-> B.reflS xay.fst xay.snd resp = \(xay ::XAB.set) |-> \(xay'::XAB.set) |-> \(p::XAB.eq xay xay')-> tt@_ reflS :: ReflS = lam (lam reflS0) reflS0 (|X::Con_o) (A::Ty_o X) (B::Ty_o (Compr X A)) :: (EQ_reflS_ A B).ReflS0 = (EQ_reflS_ A B).reflS0 reflS (|X::Con_o) (A::Ty_o X) (B::Ty_o (Compr X A)) :: (EQ_reflS_ A B).ReflS = (EQ_reflS_ A B).reflS -- --------------------------------------------------------------------------- package EQ_ext_ (|X::Con_o) (A::Ty_o X) (B::Ty_o (Compr X A)) where F :: Ty_o X = Pi A B FF :: Ty_o X = Prod F F XFF :: Con_o = Compr X FF w1 :: Con_m XFF X = c_fst c_id F' :: Ty_o XFF = Ty_m w1 F XFFA :: Con_o = Compr XFF (Ty_m w1 A) w2 :: Con_m XFFA (Compr (Compr X A) (Prod B B)) = let lem1 :: Con_m XFFA (Compr X A) = c_lift w1 lem2 :: Tm_o XFFA (Ty_m lem1 (Prod B B)) = let fg:: Tm_o XFF (Ty_m w1 FF) = c_snd c_id f :: Tm_o XFF F' = prod_fst |_ |F' |F' fg g :: Tm_o XFF F' = prod_snd |_ |F' |F' fg fa_ga :: Tm_o XFFA (Ty_m lem1 (Prod B B)) = prod_pair |_ |(Ty_m lem1 B) |(Ty_m lem1 B) (app f) (app g) in fa_ga in c_pair lem1 lem2 HYP :: Ty_o XFF = Pi (Ty_m w1 A) (Ty_m w2 (EQ B)) XFFH :: Con_o = Compr XFF HYP w :: Con_m XFFH XFF = c_fst c_id Ext0 :: Set = Tm_o XFFH (Ty_m w (EQ F)) Ext :: Set = Tm_o X (Pi FF (Pi HYP (Ty_m w (EQ F)))) ext0 :: Ext0 = struct tm :: (xfgq::XFFH.set)-> ((Ty_m w (EQ F)).fm xfgq).set = \(xfgq::XFFH.set)-> xfgq.snd.fn resp :: (x::XFFH.set) |-> (y::XFFH.set) |-> (p::XFFH.eq x y)-> T = \(x::XFFH.set) |-> \(y::XFFH.set) |-> \(p::XFFH.eq x y)-> tt@_ ext :: Ext = lam (lam ext0) ext (|X::Con_o) (|A::Ty_o X) (|B::Ty_o (Compr X A)) :: (EQ_ext_ A B).Ext = (EQ_ext_ A B).ext -- ---------------------------------------------------------------------------