Sum (!A::Set) (!B::A->Set) :: Set Sum = sig fst :: A snd :: B fst dep_pair (A::Set) (B::A->Set) :: (a::A) -> (b::B a) -> Sum A B dep_pair a b = struct fst :: A fst = a snd :: B fst snd = b ---------------------------------------------------------------------------- idata Id (X::Set) :: X -> X -> Set where refId (!x::X) :: Id x x symId (X::Set) (a,b::X) :: Id a b -> Id b a symId id = case id of (refId x)-> refId x tranId (X::Set) (a,b,c::X) :: Id a b -> Id b c -> Id a c tranId id1 id2 = case id1 of (refId x)-> case id2 of (refId x')-> refId x mapId (X,Y::Set) (!f::X->Y) (a,b::X) :: Id a b -> Id (f a) (f b) mapId id = case id of (refId x)-> refId (f x) substId (X::Set) (!P::X->Set) (x,y::X) :: Id x y -> P x -> P y substId id p = case id of (refId x')-> p postulate uniqueId :: (X::Set) |-> (x::X) |-> (P::Id x x->Set) -> P (refId x) -> (id::Id x x) -> P id postulate ext :: (A::Set) |-> (B::A->Set) |-> (f,g::(a::A)->B a) -> (eid::(a::A) -> Id (f a) (g a)) -> Id f g unitSubst (A::Set) (B::A->Set) (a::A) (!id::Id a a) (!b::B a) :: Id b (substId B id b) unitSubst = uniqueId (\(id::Id a a) -> Id b (substId B id b)) (refId b) id tranSubst (A::Set) (B::A->Set) (a1,a2,a3::A) (!id1::Id a1 a2) (!id2::Id a2 a3) (!b::B a1) :: Id (substId B id2 (substId B id1 b)) (substId B (tranId id1 id2) b) tranSubst = case id1 of (refId x)-> case id2 of (refId x')-> refId b UIP (X::Set) (a,b::X) (!id1,!id2::Id a b) :: Id id1 id2 UIP = case id1 of (refId x)-> uniqueId (\(id::Id a b) -> Id id1 id) (refId (refId x)) id2 pairId (A::Set) (B::A->Set) (a1,a2::A) (b1::B a1) (b2::B a2) :: (id1::Id a1 a2) -> Id (substId B id1 b1) b2 -> Id (dep_pair a1 b1) (dep_pair a2 b2) pairId id1 id2 = case id1 of (refId a)-> case id2 of (refId b)-> refId (dep_pair a b) unpairId (A::Set) (B::A->Set) (x,y::Sum A B) :: Id x y -> Sum (Id x.fst y.fst) (\id-> Id (substId B id x.snd) y.snd) unpairId id = case id of (refId z)-> struct fst :: Id z.fst z.fst fst = refId z.fst snd :: Id (substId B fst z.snd) z.snd snd = refId z.snd sndId (A::Set) (B::A->Set) (a::A) (b1,b2::B a) :: Id (dep_pair a b1) (dep_pair a b2) -> Id b1 b2 sndId id = let lem1 :: Sum (Id a a) (\(id'::Id a a) -> Id (substId B id' b1) b2) lem1 = unpairId id lem2 :: Id b1 (substId B lem1.fst b1) lem2 = unitSubst lem1.fst b1 in tranId lem2 lem1.snd ---------------------------------------------------------------------------- data Empty = data Unit = tt uu (X::Set) :: Empty -> X uu e = case e of { } uu_lemma (X::Set) (!f::Empty -> X) :: Id uu f uu_lemma = let eid (!e::Empty) :: Id (uu e) (f e) eid = case e of { } in ext uu f eid tt_lemma (X::Set) (!f::Unit -> X) :: Id (\(t::Unit)-> f tt) f tt_lemma = let eid (!t::Unit) :: Id (f tt) (f t) eid = case t of (tt)-> refId (f tt) in ext (\(t::Unit) -> f tt) f eid ---------------------------------------------------------------------------- data Either (A,B::Set) = Left (a::A) | Right (b::B) data Maybe (X::Set) = Nothing | Just (x::X) data Nat = Zero | Succ (n::Nat) ---------------------------------------------------------------------------- T (!A::Set) (!B::A->Set) :: Set -> Set T X = Sum A (\(a::A) -> B a -> X) fmapT (A::Set) (B::A->Set) (X,Y::Set) :: (X -> Y) -> (T A B X -> T A B Y) fmapT f x = struct fst :: A fst = x.fst snd :: B fst -> Y snd = \(b::B x.fst) -> f (x.snd b) fmapT_dist (A::Set) (B::A->Set) (X,Y,Z::Set) (!f::Y->Z) (!g::X->Y) (!t::T A B X) :: Id (fmapT f (fmapT g t)) (fmapT (\(x::X) -> f (g x)) t) fmapT_dist = refId (fmapT f (fmapT g t)) ---------------------------------------------------------------------------- data M' (!A::Set) (!B::A->Set) = mbot' -- ⊥ | msup' (a::A) (f::B a -> M' A B) msupId' (A::Set) (B::A->Set) (!a::A) (!f,!g::B a -> M' A B) (!id::(b::B a) -> Id (f b) (g b)) :: Id (msup' a f) (msup' a g) msupId' = mapId (msup' a) (ext f g (\(b::B a) -> id b)) alpha' (A::Set) (B::A->Set) :: T A B (Nat -> M' A B) -> Nat -> M' A B alpha' x n = case n of (Zero )-> mbot' (Succ n')-> msup' x.fst (\(b::B x.fst) -> x.snd b n') unfold' (A::Set) (B::A->Set) (X::Set) :: (X -> T A B X) -> (X -> (Nat->M' A B)) unfold' beta x n = case n of (Zero )-> mbot' (Succ n')-> msup' (beta x).fst (\(b::B (beta x).fst) -> unfold' beta ((beta x).snd b) n') prop1' (A::Set) (B::A->Set) (X::Set) (!beta :: X -> T A B X) (!x::X) :: Id (alpha' (fmapT (unfold' beta) (beta x))) (unfold' beta x) prop1' = let eid (!x::X) (!n::Nat) :: Id (alpha' (fmapT (unfold' beta) (beta x)) n) (unfold' beta x n) eid = case n of (Zero )-> refId mbot' (Succ n')-> msupId' (beta x).fst (\(b::B (beta x).fst) -> (fmapT (unfold' beta) (beta x)).snd b n') (\(b::B (beta x).fst) -> unfold' beta ((beta x).snd b) n') (\(b::B (beta x).fst) -> refId (unfold' beta ((beta x).snd b) n')) in ext (alpha' (fmapT (unfold' beta) (beta x))) (unfold' beta x) (eid x) prop2' (A::Set) (B::A->Set) (X::Set) (!beta :: X -> T A B X) (!g::X -> (Nat->M' A B)) (!id::(x::X) -> (n::Nat) -> Id (g x n) (alpha' (fmapT g (beta x)) n)) (!x::X) :: Id (g x) (unfold' beta x) prop2' = let eid (!x::X) (!n::Nat) :: Id (g x n) (unfold' beta x n) eid = case n of (Zero )-> id x Zero (Succ n')-> let lem1 :: Id (g x (Succ n')) (alpha' (fmapT g (beta x)) (Succ n')); lem1 = id x n lem2 :: Id (alpha' (fmapT g (beta x)) (Succ n')) (unfold' beta x (Succ n')) lem2 = msupId' (beta x).fst (\(b::B (beta x).fst) -> (fmapT g (beta x)).snd b n') (\(b::B (beta x).fst) -> unfold' beta ((beta x).snd b) n') (\(b::B (beta x).fst) -> eid ((beta x).snd b) n') in tranId lem1 lem2 in ext (g x) (unfold' beta x) (eid x) ---------------------------------------------------------------------------- data M'' (!A::Set) (!B::A->Set) = mbot'' | msup'' (a::A) (f::B a -> M'' A B) | mtruncated msupId'' (A::Set) (B::A->Set) (!a::A) (!f,!g::B a -> M'' A B) (!id::(b::B a) -> Id (f b) (g b)) :: Id (msup'' a f) (msup'' a g) msupId'' = mapId (msup'' a) (ext f g (\(b::B a) -> id b)) trunc' (A::Set) (B::A->Set) :: M'' A B -> (Nat -> M'' A B) trunc' m n = case n of (Zero )-> mbot'' (Succ n')-> case m of (mbot'' )-> mtruncated (mtruncated)-> mtruncated (msup'' a f)-> msup'' a (\(b::B a) -> trunc' (f b) n') ---------------------------------------------------------------------------- iota (A::Set) (B::A->Set) :: M' A B -> M'' A B iota m = case m of (mbot' )-> mbot'' (msup' a f)-> msup'' a (\(b::B a) -> iota (f b)) trunc (A::Set) (B::A->Set) :: M' A B -> (Nat -> M'' A B) trunc m n = trunc' (iota m) n M_eq (A::Set) (B::A->Set) (!m::Nat -> M' A B) :: Set M_eq = (n::Nat) -> Id (iota (m n)) (trunc (m (Succ n)) n) M (!A::Set) (!B::A->Set) :: Set M = Sum (Nat -> M' A B) M_eq alpha_eq (A::Set) (B::A->Set) (!x::T A B (M A B)) :: M_eq (alpha' (fmapT (\(m::M A B) -> m.fst) x)) alpha_eq n = case n of (Zero )-> refId (iota mbot') (Succ n')-> let y :: T A B (Nat -> M' A B); y = fmapT (\(m::M A B) -> m.fst) x in msupId'' y.fst (\(b::B x.fst) -> iota (y.snd b n')) (\(b::B x.fst) -> trunc' (iota (y.snd b (Succ n'))) n') (\(b::B x.fst) -> (x.snd b).snd n') alpha (A::Set) (B::A->Set) :: T A B (M A B) -> M A B alpha x = let y :: T A B (Nat -> M' A B); y = fmapT (\(m::M A B) -> m.fst) x in struct fst :: Nat -> M' A B fst = alpha' y snd :: M_eq fst snd = alpha_eq x unfold_eq (A::Set) (B::A->Set) (X::Set) (!beta::X -> T A B X) (!x::X) :: M_eq (unfold' beta x) unfold_eq n = case n of (Zero )-> refId (iota mbot') (Succ n')-> msupId'' (beta x).fst (\(b::B (beta x).fst) -> iota (unfold' beta ((beta x).snd b) n')) (\(b::B (beta x).fst) -> trunc' (iota (unfold' beta ((beta x).snd b) (Succ n'))) n') (\(b::B (beta x).fst) -> unfold_eq beta ((beta x).snd b) n') unfold (A::Set) (B::A->Set) (X::Set) :: (X -> T A B X) -> (X -> M A B) unfold beta x = struct fst :: Nat -> M' A B fst = unfold' beta x snd :: M_eq fst snd = unfold_eq beta x UIP2 (A::Set) (B::A->Set) (f,g::(a::A)->B a) (!id1,!id2::(a::A)->Id (f a) (g a)) :: Id id1 id2 UIP2 = let eid (!a::A) :: Id (id1 a) (id2 a) eid = UIP (id1 a) (id2 a) in ext id1 id2 eid liftId (A::Set) (B::A->Set) (m1,m2::M A B) :: Id m1.fst m2.fst -> Id m1 m2 liftId id = let id2 :: Id |(M_eq m2.fst) (substId M_eq id m1.snd) m2.snd id2 = UIP2 |Nat |(\(n::Nat) -> M'' A B) |(\(n::Nat) -> iota (m2.fst n)) |(\(n::Nat) -> trunc (m2.fst (Succ n)) n) (substId M_eq id m1.snd) m2.snd in pairId id id2 prop1 (A::Set) (B::A->Set) (X::Set) (!beta :: X -> T A B X) (!x::X) :: Id (alpha (fmapT (unfold beta) (beta x))) (unfold beta x) prop1 = liftId (prop1' beta x) prop2 (A::Set) (B::A->Set) (X::Set) (beta :: X -> T A B X) (g::X -> M A B) (id::(x::X) -> Id (g x) (alpha (fmapT g (beta x)))) (!x::X) :: Id (g x) (unfold beta x) prop2 = let g' :: X -> Nat -> M' A B; g' x = (g x).fst id' (!x'::X) (!n::Nat) :: Id (g' x' n) (alpha' (fmapT g' (beta x')) n) id' = mapId (\(m::M A B) -> m.fst n) (id x') lem :: Id (g' x) (unfold' beta x) lem = prop2' beta g' id' x in liftId lem ---------------------------------------------------------------------------- is_msup' (A::Set) (B::A->Set) (!m::M' A B) :: Set is_msup' = sig a :: A f :: B a -> M' A B id :: Id m (msup' a f) Foo (A::Set) (B::A->Set) (!m::M' A B) (!n::Nat) :: Set Foo = sig a :: A f :: B a -> M' A B id :: Id (trunc m (Succ n)) (trunc (msup' a f) (Succ n)) foo (A::Set) (B::A->Set) (!m::M' A B) (!n::Nat) :: Either (Id (trunc m (Succ n)) mtruncated) (Foo m n) foo = case m of (mbot' )-> Left (refId mtruncated) (msup' a' f')-> let lem :: Foo m n lem = struct a :: A a = a' f :: B a -> M' A B f = f' id :: Id (trunc m (Succ n)) (trunc (msup' a f) (Succ n)) id = refId (trunc (msup' a' f') (Succ n)) in Right lem bar (A::Set) (B::A->Set) (!m::M' A B) :: Either (Id m mbot') (is_msup' m) bar = case m of (mbot' )-> Left (refId mbot') (msup' a' f')-> let lem :: is_msup' m lem = struct a :: A a = a' f :: B a -> M' A B f = f' id :: Id m (msup' a f) id = refId (msup' a' f') in Right lem out' (A::Set) (B::A->Set) (!m::M A B) (!n::Nat) :: is_msup' (m.fst (Succ n)) out' = case bar (m.fst (Succ n)) of (Right h )-> h (Left id1)-> let id1' :: Id (iota (m.fst (Succ n))) mbot'' id1' = mapId iota id1 id2 :: Id (iota (m.fst (Succ n))) (trunc' (iota (m.fst (Succ (Succ n)))) (Succ n)) id2 = m.snd (Succ n) id3 :: Id mbot'' (trunc' (iota (m.fst (Succ (Succ n)))) (Succ n)) id3 = tranId (symId id1') id2 T :: M'' A B -> Set T m = case m of (mbot'' )-> Unit (msup'' a f)-> Empty (mtruncated)-> Empty in case foo (m.fst (Succ (Succ n))) n of (Left id4)-> let id :: Id mbot'' mtruncated id = tranId id3 id4 in case substId T id tt of { } (Right h)-> let id4 :: Id (trunc (m.fst (Succ (Succ n))) (Succ n)) (trunc (msup' h.a h.f) (Succ n)) id4 = h.id id :: Id mbot'' (trunc (msup' h.a h.f) (Succ n)) id = tranId id3 id4 in case substId T id tt of { } hoge (A::Set) (B::A->Set) (a::A) (f1::B a -> M'' A B) (f2::B a -> M'' A B) (!id::Id (msup'' a f1) (msup'' a f2)) :: Id f1 f2 hoge = let G (!x::M'' A B) :: Set G = case x of (msup'' a' f)-> T A B (M'' A B) (mbot'' )-> Unit (mtruncated )-> Unit dmy :: T A B (M'' A B) dmy = struct fst :: A fst = a snd :: B fst -> M'' A B snd = f1 g :: M'' A B -> T A B (M'' A B) g x = case x of (mbot'' )-> dmy (mtruncated )-> dmy (msup'' a' f)-> struct fst :: A fst = a' snd :: B fst -> M'' A B snd = f id2 :: Id |(T A B (M'' A B)) (dep_pair a f1) (dep_pair a f2) id2 = mapId g id in sndId id2 out_lem (A::Set) (B::A->Set) (!m::M A B) (!n::Nat) :: Sum (Id (out' m n).a (out' m (Succ n)).a) (\id-> (b::B (out' m n).a)-> Id (iota ((out' m n).f b)) (trunc ((out' m (Succ n)).f (substId B id b)) n)) out_lem = let b1 :: is_msup' (m.fst (Succ n)) b1 = out' m n b2 :: is_msup' (m.fst (Succ (Succ n))) b2 = out' m (Succ n) lem0 :: Id (iota (m.fst (Succ n))) (trunc (m.fst (Succ (Succ n))) (Succ n)) lem0 = m.snd (Succ n) lem1 :: Id (iota (m.fst (Succ n))) (iota (msup' b1.a b1.f)) lem1 = mapId iota b1.id lem2 :: Id (trunc (m.fst (Succ (Succ n))) (Succ n)) (trunc (msup' b2.a b2.f) (Succ n)) lem2 = mapId (\(m'::M' A B) -> trunc m' (Succ n)) b2.id lem3 :: Id (iota (msup' b1.a b1.f)) (trunc (msup' b2.a b2.f) (Succ n)) lem3 = tranId (symId lem1) (tranId lem0 lem2) lem4 :: Id (msup'' b1.a (\(b::B b1.a) -> iota (b1.f b))) (msup'' b2.a (\(b::B b2.a) -> trunc (b2.f b) n)) lem4 = lem3 id1 :: Id b1.a b2.a id1 = let g :: M'' A B -> A g m'' = case m'' of (mbot'' )-> b1.a (mtruncated)-> b1.a (msup'' a f)-> a in mapId g lem4 lem5 (!a::A) (!b::B a) (!f1,!f2::B a -> M'' A B) (!id::Id (msup'' a f1) (msup'' a f2)) :: Id (f1 b) (f2 b) lem5 = mapId (\(f::B a -> M'' A B) -> f b) (hoge id) k (a1,a2::A) (f1::B a1 -> M'' A B) (f2::B a2 -> M'' A B) (!id1::Id a1 a2) (!id2::Id (msup'' a1 f1) (msup'' a2 f2)) (!b::B a1) :: Id (f1 b) (f2 (substId B id1 b)) k = case id1 of (refId x)-> lem5 a1 b f1 f2 id2 lem6 :: (b::B (out' m n).a)-> Id (iota ((out' m n).f b)) (trunc ((out' m (Succ n)).f (substId B id1 b)) n) lem6 = k id1 lem4 in struct fst :: Id (out' m n).a (out' m (Succ n)).a fst = id1 snd :: (b::B (out' m n).a)-> Id (iota ((out' m n).f b)) (trunc ((out' m (Succ n)).f (substId B id1 b)) n) snd = lem6 out_a (A::Set) (B::A->Set) :: M A B -> A out_a m = (out' m Zero).a out_a_eq (A::Set) (B::A->Set) (!m::M A B) (!n::Nat) :: Id (out_a m) (out' m n).a out_a_eq = case n of (Zero )-> refId (out' m Zero).a (Succ n')-> let l1 :: Id (out_a m) (out' m n').a l1 = out_a_eq m n' l2 :: Id (out' m n').a (out' m n).a l2 = (out_lem m n').fst in tranId l1 l2 out_f' (A::Set) (B::A->Set) (!m::M A B) (!b::B (out_a m)) :: Nat -> M' A B out_f' n = (out' m n).f (substId B (out_a_eq m n) b) out_f_eq (A::Set) (B::A->Set) (!m::M A B) (!b::B (out_a m)) :: M_eq (out_f' m b) out_f_eq n = let f :: Nat -> M' A B f = out_f' m b b' :: B (out' m n).a b' = substId B (out_a_eq m n) b l :: Id (iota ((out' m n).f b')) (trunc ((out' m (Succ n)).f (substId B (out_lem m n).fst b')) n) l = (out_lem m n).snd b' l4 :: Id (substId B (out_lem m n).fst b') (substId B (tranId (out_a_eq m n) (out_lem m n).fst) b) l4 = tranSubst (out_a_eq m n) (out_lem m n).fst b l3 :: Id (substId B (out_lem m n).fst b') (substId B (out_a_eq m (Succ n)) b) l3 = l4 l2 :: Id (trunc ((out' m (Succ n)).f (substId B (out_lem m n).fst b')) n) (trunc (f (Succ n)) n) l2 = mapId (\(b::B (out' m (Succ n)).a) -> trunc ((out' m (Succ n)).f b) n) l3 in tranId l l2 out_f (A::Set) (B::A->Set) (!m::M A B) :: B (out_a m) -> M A B out_f b = struct fst :: Nat -> M' A B fst = out_f' m b snd :: M_eq fst snd = out_f_eq m b out (A::Set) (B::A->Set) :: M A B -> T A B (M A B) out m = struct fst :: A fst = out_a m snd :: B fst -> M A B snd = out_f m iotaInj (A::Set) (B::A->Set) (m1,m2::M' A B) :: Id (iota m1) (iota m2) -> Id m1 m2 iotaInj id = {! !} lemZ (A::Set) (B::A->Set) (!m::M A B) :: Id (m.fst Zero) mbot' lemZ = let lem :: Id (iota (m.fst Zero)) mbot'' lem = m.snd Zero in iotaInj lem iso1 (A::Set) (B::A->Set) (!m::M A B) :: Id (alpha (out m)) m iso1 = let lem1 (!n::Nat) :: Id (alpha' (fmapT (\(m'::M A B) -> m'.fst) (out m)) n) (m.fst n) lem1 = {! !} lem :: Id (alpha' (fmapT (\(m'::M A B) -> m'.fst) (out m))) m.fst lem = ext (alpha' (fmapT (\(m'::M A B) -> m'.fst) (out m))) m.fst lem1 in liftId lem iso2 (A::Set) (B::A->Set) (!x::T A B (M A B)) :: Id (out (alpha x)) x iso2 = {! !} {- f :: Nat -> Nat -> Nat f x n = case n of (Zero )-> x (Succ n')-> case x of (Zero )-> f x n' (Succ x')-> f x n' g :: Nat -> Nat -> Nat g x n' = case x of (Zero )-> f x n' (Succ x')-> f x n' h (!x::Nat) (!n'::Nat) :: (Id (f x (Succ n')) (g x n')) h = {!refId !} -- このゴールはrefine出来ない -}