1 (edited by AntHirosaki 2019-10-27 10:23:30)

Topic: Using Coq to help write Dalilcoin drafts

I did some work in Coq that allowed me to prove some theorems (conjectures with bounties in this case) in Coq and then port the proofs to a Dalilcoin draft. There is too much to say, so I may split this information over multiple posts.

Note: I am always using Coq with the "-nois" (no initial state) option, so that it does not use the initialization from the Coq standard library.

First I have a Coq file that wraps some application, lambdas and foralls into definitions like _Ap, _Lam, _All, etc. There is then prefix notation given for each of these definitions. For some reason Coq has trouble parsing terms given in the prefix notation, but it will print them this way. Since Dalilcoin drafts require the prefix notation, it is enough to construct terms in Coq, have Coq print them in prefix notation and then copy and paste this to a Dalilcoin draft.

Here is the first file Dalilcoin.v:

Definition _TpAll (F:Type -> Type) : Type := (forall X:Type, F X).
Notation "'TpAll' X Y" := (_TpAll (fun X:Type => Y)) (at level 75, right associativity).
Definition _TpArr (X Y:Type) : Type := (X -> Y).
Notation "'TpArr' X Y" := (_TpArr X Y) (at level 75, right associativity).
Definition _Ap {X Y:Type} (F:X -> Y) (A:X) := F A.
Notation "'Ap' F A" := (_Ap F A) (at level 75, right associativity).
Definition _Lam {X Y:Type} (F:X -> Y) := (fun A:X => F A).
Notation "'Lam' A X B" := (_Lam (fun A:X => B)) (at level 75, right associativity).
Definition _Imp (A B:Prop) : Prop := A -> B.
Notation "'Imp' F A" := (_Imp F A) (at level 75, right associativity).
Definition _All {X:Type} (F:X -> Prop) := (forall A:X, F A).
Notation "'All' A X B" := (_All (fun A:X => B)) (at level 75, right associativity).
Definition _TTpAp {Y:Type -> Type} (F:forall X:Type, Y X) (X:Type) := F X.
Notation "'TTpAp' F X" := (_TTpAp F X) (at level 75, right associativity).
Definition _TTpLam {Y:Type -> Type} (F:forall X:Type, Y X) := fun X:Type => F X.
Notation "'TTpLam' X A" := (_TTpLam (fun X:Type => A)) (at level 75, right associativity).
Definition _TTpAll (F:forall X:Type, Prop) : Prop := forall X:Type, F X.
Notation "'TTpAll' X A" := (_TTpAll (fun X:Type => A)) (at level 75, right associativity).
Definition _PrAp {X Y:Prop} (F:X -> Y) (A:X) := F A.
Notation "'PrAp' F A" := (_PrAp F A) (at level 75, right associativity).
Definition _TmAp {X:Type} {Y:X -> Prop} (F:forall x:X, Y x) (A:X) := F A.
Notation "'TmAp' F A" := (_TmAp F A) (at level 75, right associativity).
Definition _TpAp {Y:Type -> Prop} (F:forall X:Type, Y X) (X:Type) := F X.
Notation "'TpAp' F X" := (_TpAp F X) (at level 75, right associativity).
Definition _PrLa {A B:Prop} (F:A -> B) := (fun H:A => F H).
Notation "'PrLa' H A F" := (_PrLa (fun H:A => F)) (at level 75, right associativity).
Definition _TmLa {X:Type} {B:X -> Prop} (F:forall A:X, B A) := fun A:X => F A.
Notation "'TmLa' A X F" := (_TmLa (fun A:X => F)) (at level 75, right associativity).
Definition _TpLa {F:forall X:Type, Prop} (D:forall X:Type, F X) := fun X:Type => D X.
Notation "'TpLa' X A" := (_TpLa (fun X:Type => A)) (at level 75, right associativity).

I modified my copy of dalilcoin to export Coq readable versions of drafts when I call "readdraft".
Using this I made a Coq file (Firstsig.v) corresponding to the signature called firstsig here:

https://github.com/aliibrahim80/dalilco … c/firstsig

Here is Firstsig.v:

Require Export Dalilcoin.

Parameter set : Type.
Definition False: Prop := _All (fun x0:Prop => x0).
Definition True: Prop := _All (fun x0:Prop => _Imp x0 x0).
Axiom TrueI: True.
Definition not: _TpArr Prop Prop := _Lam (fun x0:Prop => _Imp x0 False).
Definition and: _TpArr Prop (_TpArr Prop Prop) := _Lam (fun x0:Prop => _Lam (fun x1:Prop => _All (fun x2:Prop => _Imp (_Imp x0 (_Imp x1 x2)) x2))).
Axiom andI: _All (fun x0:Prop => _All (fun x1:Prop => _Imp x0 (_Imp x1 (_Ap (_Ap and x0) x1)))).
Definition or: _TpArr Prop (_TpArr Prop Prop) := _Lam (fun x0:Prop => _Lam (fun x1:Prop => _All (fun x2:Prop => _Imp (_Imp x0 x2) (_Imp (_Imp x1 x2) x2)))).
Axiom orIL: _All (fun x0:Prop => _All (fun x1:Prop => _Imp x0 (_Ap (_Ap or x0) x1))).
Axiom orIR: _All (fun x0:Prop => _All (fun x1:Prop => _Imp x1 (_Ap (_Ap or x0) x1))).
Definition iff: _TpArr Prop (_TpArr Prop Prop) := _Lam (fun x0:Prop => _Lam (fun x1:Prop => _Ap (_Ap and (_Imp x0 x1)) (_Imp x1 x0))).
Definition eq: _TpAll (fun A0:Type => _TpArr A0 (_TpArr A0 Prop)) := _TTpLam (fun A0:Type => _Lam (fun x0:A0 => _Lam (fun x1:A0 => _All (fun x2:_TpArr A0 Prop => _Imp (_Ap x2 x0) (_Ap x2 x1))))).
Axiom eqI: _TTpAll (fun A0:Type => _All (fun x0:A0 => _Ap (_Ap (_TTpAp eq A0) x0) x0)).
Axiom eq_sym: _TTpAll (fun A0:Type => _All (fun x0:A0 => _All (fun x1:A0 => _Imp (_Ap (_Ap (_TTpAp eq A0) x0) x1) (_Ap (_Ap (_TTpAp eq A0) x1) x0)))).
Axiom eq_trans: _TTpAll (fun A0:Type => _All (fun x0:A0 => _All (fun x1:A0 => _All (fun x2:A0 => _Imp (_Ap (_Ap (_TTpAp eq A0) x0) x1) (_Imp (_Ap (_Ap (_TTpAp eq A0) x1) x2) (_Ap (_Ap (_TTpAp eq A0) x0) x2)))))).
Axiom f_equal: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:A0 => _All (fun x1:A0 => _All (fun x2:_TpArr A0 A1 => _Imp (_Ap (_Ap (_TTpAp eq A0) x0) x1) (_Ap (_Ap (_TTpAp eq A1) (_Ap x2 x0)) (_Ap x2 x1))))))).
Definition ex: _TpAll (fun A0:Type => _TpArr (_TpArr A0 Prop) Prop) := _TTpLam (fun A0:Type => _Lam (fun x0:_TpArr A0 Prop => _All (fun x1:Prop => _Imp (_All (fun x2:A0 => _Imp (_Ap x0 x2) x1)) x1))).
Axiom exI: _TTpAll (fun A0:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:A0 => _Imp (_Ap x0 x1) (_Ap (_TTpAp ex A0) (_Lam (fun x2:A0 => _Ap x0 x2)))))).
Axiom prop_ext2: _All (fun x0:Prop => _All (fun x1:Prop => _Imp (_Imp x0 x1) (_Imp (_Imp x1 x0) (_Ap (_Ap (_TTpAp eq Prop) x0) x1)))).
Axiom func_ext: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 A1 => _All (fun x1:_TpArr A0 A1 => _Imp (_All (fun x2:A0 => _Ap (_Ap (_TTpAp eq A1) (_Ap x0 x2)) (_Ap x1 x2))) (_Ap (_Ap (_TTpAp eq (_TpArr A0 A1)) x0) x1))))).
Definition symmetric: _TpAll (fun A0:Type => _TpArr (_TpArr A0 (_TpArr A0 Prop)) Prop) := _TTpLam (fun A0:Type => _Lam (fun x0:_TpArr A0 (_TpArr A0 Prop) => _All (fun x1:A0 => _All (fun x2:A0 => _Imp (_Ap (_Ap x0 x1) x2) (_Ap (_Ap x0 x2) x1))))).
Definition transitive: _TpAll (fun A0:Type => _TpArr (_TpArr A0 (_TpArr A0 Prop)) Prop) := _TTpLam (fun A0:Type => _Lam (fun x0:_TpArr A0 (_TpArr A0 Prop) => _All (fun x1:A0 => _All (fun x2:A0 => _All (fun x3:A0 => _Imp (_Ap (_Ap x0 x1) x2) (_Imp (_Ap (_Ap x0 x2) x3) (_Ap (_Ap x0 x1) x3))))))).
Definition per: _TpAll (fun A0:Type => _TpArr (_TpArr A0 (_TpArr A0 Prop)) Prop) := _TTpLam (fun A0:Type => _Lam (fun x0:_TpArr A0 (_TpArr A0 Prop) => _Ap (_Ap and (_Ap (_TTpAp symmetric A0) x0)) (_Ap (_TTpAp transitive A0) x0))).
Axiom per_tra: _TTpAll (fun A0:Type => _All (fun x0:_TpArr A0 (_TpArr A0 Prop) => _Imp (_Ap (_TTpAp per A0) x0) (_Ap (_TTpAp transitive A0) x0))).
Axiom per_stra1: _TTpAll (fun A0:Type => _All (fun x0:_TpArr A0 (_TpArr A0 Prop) => _Imp (_Ap (_TTpAp per A0) x0) (_All (fun x1:A0 => _All (fun x2:A0 => _All (fun x3:A0 => _Imp (_Ap (_Ap x0 x2) x1) (_Imp (_Ap (_Ap x0 x2) x3) (_Ap (_Ap x0 x1) x3)))))))).
Axiom per_ref1: _TTpAll (fun A0:Type => _All (fun x0:_TpArr A0 (_TpArr A0 Prop) => _Imp (_Ap (_TTpAp per A0) x0) (_All (fun x1:A0 => _All (fun x2:A0 => _Imp (_Ap (_Ap x0 x1) x2) (_Ap (_Ap x0 x1) x1)))))).
Axiom per_ref2: _TTpAll (fun A0:Type => _All (fun x0:_TpArr A0 (_TpArr A0 Prop) => _Imp (_Ap (_TTpAp per A0) x0) (_All (fun x1:A0 => _All (fun x2:A0 => _Imp (_Ap (_Ap x0 x1) x2) (_Ap (_Ap x0 x2) x2)))))).
Parameter Eps: _TpAll (fun A0:Type => _TpArr (_TpArr A0 Prop) A0).
Axiom EpsR: _TTpAll (fun A0:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:A0 => _Imp (_Ap x0 x1) (_Ap x0 (_Ap (_TTpAp Eps A0) (_Lam (fun x2:A0 => _Ap x0 x2))))))).
Axiom classic: _All (fun x0:Prop => _Ap (_Ap or x0) (_Ap not x0)).
Axiom NNPP: _All (fun x0:Prop => _Imp (_Ap not (_Ap not x0)) x0).
Parameter If: _TpAll (fun A0:Type => _TpArr Prop (_TpArr A0 (_TpArr A0 A0))).
Axiom If_0: _TTpAll (fun A0:Type => _All (fun x0:Prop => _All (fun x1:A0 => _All (fun x2:A0 => _Imp (_Ap not x0) (_Ap (_Ap (_TTpAp eq A0) (_Ap (_Ap (_Ap (_TTpAp If A0) x0) x1) x2)) x2))))).
Axiom If_1: _TTpAll (fun A0:Type => _All (fun x0:Prop => _All (fun x1:A0 => _All (fun x2:A0 => _Imp x0 (_Ap (_Ap (_TTpAp eq A0) (_Ap (_Ap (_Ap (_TTpAp If A0) x0) x1) x2)) x1))))).
Definition MetaFuncEquiv: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 A1) Prop)))) := _TTpLam (fun A0:Type => _TTpLam (fun A1:Type => _Lam (fun x0:_TpArr A0 Prop => _Lam (fun x1:_TpArr A0 A1 => _Lam (fun x2:_TpArr A0 A1 => _All (fun x3:A0 => _Imp (_Ap x0 x3) (_Ap (_Ap (_TTpAp eq A1) (_Ap x1 x3)) (_Ap x2 x3)))))))).
Axiom MetaFuncEquiv_ref: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 A1 => _Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncEquiv A0) A1) x0) x1) x1)))).
Axiom MetaFuncEquiv_sym: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _Ap (_TTpAp symmetric (_TpArr A0 A1)) (_Ap (_TTpAp (_TTpAp MetaFuncEquiv A0) A1) x0)))).
Axiom MetaFuncEquiv_tra: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _Ap (_TTpAp transitive (_TpArr A0 A1)) (_Ap (_TTpAp (_TTpAp MetaFuncEquiv A0) A1) x0)))).
Axiom MetaFuncEquiv_per: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _Ap (_TTpAp per (_TpArr A0 A1)) (_Ap (_TTpAp (_TTpAp MetaFuncEquiv A0) A1) x0)))).
Parameter MetaFuncC: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 A1) (_TpArr A0 A1)))).
Axiom MetaFuncC_rel: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 A1 => _Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncEquiv A0) A1) x0) x1) (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncC A0) A1) x0) x1))))).
Axiom MetaFuncC_eq: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 A1 => _All (fun x2:_TpArr A0 A1 => _Imp (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncEquiv A0) A1) x0) x1) x2) (_Ap (_Ap (_TTpAp eq (_TpArr A0 A1)) (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncC A0) A1) x0) x1)) (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncC A0) A1) x0) x2))))))).
Axiom MetaFuncC_idem: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 A1 => _Ap (_Ap (_TTpAp eq (_TpArr A0 A1)) (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncC A0) A1) x0) x1)) (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncC A0) A1) x0) (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncC A0) A1) x0) x1)))))).
Parameter MetaFuncQ: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 A1) Prop))).
Axiom MetaFuncQ_prop2: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 A1 => _All (fun x2:_TpArr A0 A1 => _Imp (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncQ A0) A1) x0) x1) (_Imp (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncQ A0) A1) x0) x2) (_Imp (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncEquiv A0) A1) x0) x1) x2) (_Ap (_Ap (_TTpAp eq (_TpArr A0 A1)) x1) x2)))))))).
Parameter In: _TpArr set (_TpArr set Prop).
Definition Subq: _TpArr set (_TpArr set Prop) := _Lam (fun x0:set => _Lam (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) x0) (_Ap (_Ap In x2) x1)))).
Axiom set_ext: _All (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap Subq x0) x1) (_Imp (_Ap (_Ap Subq x1) x0) (_Ap (_Ap (_TTpAp eq set) x0) x1)))).
Axiom In_ind: _All (fun x0:_TpArr set Prop => _Imp (_All (fun x1:set => _Imp (_All (fun x2:set => _Imp (_Ap (_Ap In x2) x1) (_Ap x0 x2))) (_Ap x0 x1))) (_All (fun x1:set => _Ap x0 x1))).
Parameter Empty: set.
Axiom EmptyE: _All (fun x0:set => _Ap not (_Ap (_Ap In x0) Empty)).
Parameter Union: _TpArr set set.
Axiom UnionE2: _All (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap Union x0)) (_All (fun x2:Prop => _Imp (_All (fun x3:set => _Imp (_Ap (_Ap In x1) x3) (_Imp (_Ap (_Ap In x3) x0) x2))) x2)))).
Axiom UnionI: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x1) x2) (_Imp (_Ap (_Ap In x2) x0) (_Ap (_Ap In x1) (_Ap Union x0)))))).
Parameter Power: _TpArr set set.
Axiom PowerE: _All (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap Power x0)) (_Ap (_Ap Subq x1) x0))).
Axiom PowerI: _All (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap Subq x1) x0) (_Ap (_Ap In x1) (_Ap Power x0)))).
Parameter Repl: _TpArr set (_TpArr (_TpArr set set) set).
Axiom ReplE2: _All (fun x0:set => _All (fun x1:_TpArr set set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap (_Ap Repl x0) (_Lam (fun x3:set => _Ap x1 x3)))) (_All (fun x3:Prop => _Imp (_All (fun x4:set => _Imp (_Ap (_Ap In x4) x0) (_Imp (_Ap (_Ap (_TTpAp eq set) x2) (_Ap x1 x4)) x3))) x3))))).
Axiom ReplI: _All (fun x0:set => _All (fun x1:_TpArr set set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) x0) (_Ap (_Ap In (_Ap x1 x2)) (_Ap (_Ap Repl x0) (_Lam (fun x3:set => _Ap x1 x3))))))).
Parameter Sep: _TpArr set (_TpArr (_TpArr set Prop) set).
Axiom SepI: _All (fun x0:set => _All (fun x1:_TpArr set Prop => _All (fun x2:set => _Imp (_Ap (_Ap In x2) x0) (_Imp (_Ap x1 x2) (_Ap (_Ap In x2) (_Ap (_Ap Sep x0) (_Lam (fun x3:set => _Ap x1 x3)))))))).
Axiom SepE: _All (fun x0:set => _All (fun x1:_TpArr set Prop => _All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap (_Ap Sep x0) (_Lam (fun x3:set => _Ap x1 x3)))) (_Ap (_Ap and (_Ap (_Ap In x2) x0)) (_Ap x1 x2))))).
Axiom SepE1: _All (fun x0:set => _All (fun x1:_TpArr set Prop => _All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap (_Ap Sep x0) (_Lam (fun x3:set => _Ap x1 x3)))) (_Ap (_Ap In x2) x0)))).
Axiom SepE2: _All (fun x0:set => _All (fun x1:_TpArr set Prop => _All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap (_Ap Sep x0) (_Lam (fun x3:set => _Ap x1 x3)))) (_Ap x1 x2)))).
Parameter binintersect: _TpArr set (_TpArr set set).
Axiom binintersectI: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) x0) (_Imp (_Ap (_Ap In x2) x1) (_Ap (_Ap In x2) (_Ap (_Ap binintersect x0) x1)))))).
Axiom binintersectE: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap (_Ap binintersect x0) x1)) (_Ap (_Ap and (_Ap (_Ap In x2) x0)) (_Ap (_Ap In x2) x1))))).
Axiom binintersectE1: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap (_Ap binintersect x0) x1)) (_Ap (_Ap In x2) x0)))).
Axiom binintersectE2: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap (_Ap binintersect x0) x1)) (_Ap (_Ap In x2) x1)))).
Parameter UPair: _TpArr set (_TpArr set set).
Axiom UPairE: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x0) (_Ap (_Ap UPair x1) x2)) (_Ap (_Ap or (_Ap (_Ap (_TTpAp eq set) x0) x1)) (_Ap (_Ap (_TTpAp eq set) x0) x2))))).
Axiom UPairI1: _All (fun x0:set => _All (fun x1:set => _Ap (_Ap In x0) (_Ap (_Ap UPair x0) x1))).
Axiom UPairI2: _All (fun x0:set => _All (fun x1:set => _Ap (_Ap In x1) (_Ap (_Ap UPair x0) x1))).
Parameter Sing: _TpArr set set.
Axiom SingI: _All (fun x0:set => _Ap (_Ap In x0) (_Ap Sing x0)).
Axiom SingE: _All (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap Sing x0)) (_Ap (_Ap (_TTpAp eq set) x1) x0))).
Parameter binunion: _TpArr set (_TpArr set set).
Axiom binunionI1: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) x0) (_Ap (_Ap In x2) (_Ap (_Ap binunion x0) x1))))).
Axiom binunionI2: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) x1) (_Ap (_Ap In x2) (_Ap (_Ap binunion x0) x1))))).
Axiom binunionE: _All (fun x0:set => _All (fun x1:set => _All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap (_Ap binunion x0) x1)) (_Ap (_Ap or (_Ap (_Ap In x2) x0)) (_Ap (_Ap In x2) x1))))).
Definition SetAdjoin: _TpArr set (_TpArr set set) := _Lam (fun x0:set => _Lam (fun x1:set => _Ap (_Ap binunion x0) (_Ap Sing x1))).
Definition TransSet: _TpArr set Prop := _Lam (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap In x1) x0) (_Ap (_Ap Subq x1) x0))).
Definition Union_closed: _TpArr set Prop := _Lam (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap In x1) x0) (_Ap (_Ap In (_Ap Union x1)) x0))).
Definition Power_closed: _TpArr set Prop := _Lam (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap In x1) x0) (_Ap (_Ap In (_Ap Power x1)) x0))).
Definition Repl_closed: _TpArr set Prop := _Lam (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap In x1) x0) (_All (fun x2:_TpArr set set => _Imp (_All (fun x3:set => _Imp (_Ap (_Ap In x3) x1) (_Ap (_Ap In (_Ap x2 x3)) x0))) (_Ap (_Ap In (_Ap (_Ap Repl x1) (_Lam (fun x3:set => _Ap x2 x3)))) x0))))).
Definition ZF_closed: _TpArr set Prop := _Lam (fun x0:set => _Ap (_Ap and (_Ap (_Ap and (_Ap Union_closed x0)) (_Ap Power_closed x0))) (_Ap Repl_closed x0)).
Axiom ZF_closed_I: _All (fun x0:set => _Imp (_Ap Union_closed x0) (_Imp (_Ap Power_closed x0) (_Imp (_Ap Repl_closed x0) (_Ap ZF_closed x0)))).
Axiom ZF_closed_E: _All (fun x0:set => _Imp (_Ap ZF_closed x0) (_All (fun x1:Prop => _Imp (_Imp (_Ap Union_closed x0) (_Imp (_Ap Power_closed x0) (_Imp (_Ap Repl_closed x0) x1))) x1))).
Parameter UnivOf: _TpArr set set.
Axiom UnivOf_In: _All (fun x0:set => _Ap (_Ap In x0) (_Ap UnivOf x0)).
Axiom UnivOf_TransSet: _All (fun x0:set => _Ap TransSet (_Ap UnivOf x0)).
Axiom UnivOf_ZF_closed: _All (fun x0:set => _Ap ZF_closed (_Ap UnivOf x0)).
Axiom UnivOf_Min: _All (fun x0:set => _All (fun x1:set => _Imp (_Ap (_Ap In x0) x1) (_Imp (_Ap TransSet x1) (_Imp (_Ap ZF_closed x1) (_Ap (_Ap Subq (_Ap UnivOf x0)) x1))))).

Now finally I did the same thing with this signature:

https://github.com/aliibrahim80/dalilco … ordefs1sig

This gave me a file I called Catfuncdefs1sig.v:

Require Export Firstsig.

Definition idT: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) Prop))))) := _TTpLam (fun A0:Type => _TTpLam (fun A1:Type => _Lam (fun x0:_TpArr A0 Prop => _Lam (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _Lam (fun x2:_TpArr A0 A1 => _Lam (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:A0 => _Imp (_Ap x0 x4) (_Ap (_Ap (_Ap x1 x4) x4) (_Ap x2 x4))))))))).
Definition compT: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) Prop))))) := _TTpLam (fun A0:Type => _TTpLam (fun A1:Type => _Lam (fun x0:_TpArr A0 Prop => _Lam (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _Lam (fun x2:_TpArr A0 A1 => _Lam (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:A0 => _All (fun x5:A0 => _All (fun x6:A0 => _All (fun x7:A1 => _All (fun x8:A1 => _Imp (_Ap x0 x4) (_Imp (_Ap x0 x5) (_Imp (_Ap x0 x6) (_Imp (_Ap (_Ap (_Ap x1 x4) x5) x7) (_Imp (_Ap (_Ap (_Ap x1 x5) x6) x8) (_Ap (_Ap (_Ap x1 x4) x6) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x4) x5) x6) x8) x7))))))))))))))))).
Definition idL: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) Prop))))) := _TTpLam (fun A0:Type => _TTpLam (fun A1:Type => _Lam (fun x0:_TpArr A0 Prop => _Lam (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _Lam (fun x2:_TpArr A0 A1 => _Lam (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:A0 => _All (fun x5:A0 => _All (fun x6:A1 => _Imp (_Ap x0 x4) (_Imp (_Ap x0 x5) (_Imp (_Ap (_Ap (_Ap x1 x4) x5) x6) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x4) x4) x5) x6) (_Ap x2 x4))) x6)))))))))))).
Definition idR: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) Prop))))) := _TTpLam (fun A0:Type => _TTpLam (fun A1:Type => _Lam (fun x0:_TpArr A0 Prop => _Lam (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _Lam (fun x2:_TpArr A0 A1 => _Lam (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:A0 => _All (fun x5:A0 => _All (fun x6:A1 => _Imp (_Ap x0 x4) (_Imp (_Ap x0 x5) (_Imp (_Ap (_Ap (_Ap x1 x4) x5) x6) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x4) x5) x5) (_Ap x2 x5)) x6)) x6)))))))))))).
Definition compAssoc: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) Prop))))) := _TTpLam (fun A0:Type => _TTpLam (fun A1:Type => _Lam (fun x0:_TpArr A0 Prop => _Lam (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _Lam (fun x2:_TpArr A0 A1 => _Lam (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:A0 => _All (fun x5:A0 => _All (fun x6:A0 => _All (fun x7:A0 => _All (fun x8:A1 => _All (fun x9:A1 => _All (fun x10:A1 => _Imp (_Ap x0 x4) (_Imp (_Ap x0 x5) (_Imp (_Ap x0 x6) (_Imp (_Ap x0 x7) (_Imp (_Ap (_Ap (_Ap x1 x4) x5) x8) (_Imp (_Ap (_Ap (_Ap x1 x5) x6) x9) (_Imp (_Ap (_Ap (_Ap x1 x6) x7) x10) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x4) x5) x7) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x5) x6) x7) x10) x9)) x8)) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x4) x6) x7) x10) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x4) x5) x6) x9) x8)))))))))))))))))))))).
Parameter MetaCat: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) Prop))))).
Axiom MetaCatI: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp idT A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp compT A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp idL A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp idR A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp compAssoc A0) A1) x0) x1) x2) x3) (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3))))))))))).
Axiom MetaCatE: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_All (fun x4:Prop => _Imp (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp idT A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp compT A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp idL A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp idR A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp compAssoc A0) A1) x0) x1) x2) x3) x4))))) x4)))))))).
Parameter MetaFunctor: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpAll (fun A2:Type => _TpAll (fun A3:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr (_TpArr A2 Prop) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A3 Prop))) (_TpArr (_TpArr A2 A3) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3))))) (_TpArr (_TpArr A0 A2) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A3))) Prop))))))))))))).
Axiom MetaFunctorI: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _Imp (_All (fun x10:A0 => _Imp (_Ap x0 x10) (_Ap x4 (_Ap x8 x10)))) (_Imp (_All (fun x10:A0 => _All (fun x11:A0 => _All (fun x12:A1 => _Imp (_Ap x0 x10) (_Imp (_Ap x0 x11) (_Imp (_Ap (_Ap (_Ap x1 x10) x11) x12) (_Ap (_Ap (_Ap x5 (_Ap x8 x10)) (_Ap x8 x11)) (_Ap (_Ap (_Ap x9 x10) x11) x12)))))))) (_Imp (_All (fun x10:A0 => _Imp (_Ap x0 x10) (_Ap (_Ap (_TTpAp eq A3) (_Ap (_Ap (_Ap x9 x10) x10) (_Ap x2 x10))) (_Ap x6 (_Ap x8 x10))))) (_Imp (_All (fun x10:A0 => _All (fun x11:A0 => _All (fun x12:A0 => _All (fun x13:A1 => _All (fun x14:A1 => _Imp (_Ap x0 x10) (_Imp (_Ap x0 x11) (_Imp (_Ap x0 x12) (_Imp (_Ap (_Ap (_Ap x1 x10) x11) x13) (_Imp (_Ap (_Ap (_Ap x1 x11) x12) x14) (_Ap (_Ap (_TTpAp eq A3) (_Ap (_Ap (_Ap (_Ap (_Ap x7 (_Ap x8 x10)) (_Ap x8 x11)) (_Ap x8 x12)) (_Ap (_Ap (_Ap x9 x11) x12) x14)) (_Ap (_Ap (_Ap x9 x10) x11) x13))) (_Ap (_Ap (_Ap x9 x10) x12) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x10) x11) x12) x14) x13))))))))))))) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9)))))))))))))))))).
Axiom MetaFunctorE: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) (_All (fun x10:Prop => _Imp (_Imp (_All (fun x11:A0 => _Imp (_Ap x0 x11) (_Ap x4 (_Ap x8 x11)))) (_Imp (_All (fun x11:A0 => _All (fun x12:A0 => _All (fun x13:A1 => _Imp (_Ap x0 x11) (_Imp (_Ap x0 x12) (_Imp (_Ap (_Ap (_Ap x1 x11) x12) x13) (_Ap (_Ap (_Ap x5 (_Ap x8 x11)) (_Ap x8 x12)) (_Ap (_Ap (_Ap x9 x11) x12) x13)))))))) (_Imp (_All (fun x11:A0 => _Imp (_Ap x0 x11) (_Ap (_Ap (_TTpAp eq A3) (_Ap (_Ap (_Ap x9 x11) x11) (_Ap x2 x11))) (_Ap x6 (_Ap x8 x11))))) (_Imp (_All (fun x11:A0 => _All (fun x12:A0 => _All (fun x13:A0 => _All (fun x14:A1 => _All (fun x15:A1 => _Imp (_Ap x0 x11) (_Imp (_Ap x0 x12) (_Imp (_Ap x0 x13) (_Imp (_Ap (_Ap (_Ap x1 x11) x12) x14) (_Imp (_Ap (_Ap (_Ap x1 x12) x13) x15) (_Ap (_Ap (_TTpAp eq A3) (_Ap (_Ap (_Ap (_Ap (_Ap x7 (_Ap x8 x11)) (_Ap x8 x12)) (_Ap x8 x13)) (_Ap (_Ap (_Ap x9 x12) x13) x15)) (_Ap (_Ap (_Ap x9 x11) x12) x14))) (_Ap (_Ap (_Ap x9 x11) x13) (_Ap (_Ap (_Ap (_Ap (_Ap x3 x11) x12) x13) x15) x14))))))))))))) x10)))) x10)))))))))))))))).
Parameter MetaNatTrans: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpAll (fun A2:Type => _TpAll (fun A3:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr (_TpArr A2 Prop) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A3 Prop))) (_TpArr (_TpArr A2 A3) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3))))) (_TpArr (_TpArr A0 A2) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A3))) (_TpArr (_TpArr A0 A2) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A3))) (_TpArr (_TpArr A0 A3) Prop)))))))))))))))).
Axiom MetaNatTransI: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x10:_TpArr A0 A2 => _All (fun x11:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x12:_TpArr A0 A3 => _Imp (_All (fun x13:A0 => _Imp (_Ap x0 x13) (_Ap (_Ap (_Ap x5 (_Ap x8 x13)) (_Ap x10 x13)) (_Ap x12 x13)))) (_Imp (_All (fun x13:A0 => _All (fun x14:A0 => _All (fun x15:A1 => _Imp (_Ap x0 x13) (_Imp (_Ap x0 x14) (_Imp (_Ap (_Ap (_Ap x1 x13) x14) x15) (_Ap (_Ap (_TTpAp eq A3) (_Ap (_Ap (_Ap (_Ap (_Ap x7 (_Ap x8 x13)) (_Ap x10 x13)) (_Ap x10 x14)) (_Ap (_Ap (_Ap x11 x13) x14) x15)) (_Ap x12 x13))) (_Ap (_Ap (_Ap (_Ap (_Ap x7 (_Ap x8 x13)) (_Ap x8 x14)) (_Ap x10 x14)) (_Ap x12 x14)) (_Ap (_Ap (_Ap x9 x13) x14) x15))))))))) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12))))))))))))))))))).
Axiom MetaNatTransE: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x10:_TpArr A0 A2 => _All (fun x11:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x12:_TpArr A0 A3 => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) (_All (fun x13:Prop => _Imp (_Imp (_All (fun x14:A0 => _Imp (_Ap x0 x14) (_Ap (_Ap (_Ap x5 (_Ap x8 x14)) (_Ap x10 x14)) (_Ap x12 x14)))) (_Imp (_All (fun x14:A0 => _All (fun x15:A0 => _All (fun x16:A1 => _Imp (_Ap x0 x14) (_Imp (_Ap x0 x15) (_Imp (_Ap (_Ap (_Ap x1 x14) x15) x16) (_Ap (_Ap (_TTpAp eq A3) (_Ap (_Ap (_Ap (_Ap (_Ap x7 (_Ap x8 x14)) (_Ap x10 x14)) (_Ap x10 x15)) (_Ap (_Ap (_Ap x11 x14) x15) x16)) (_Ap x12 x14))) (_Ap (_Ap (_Ap (_Ap (_Ap x7 (_Ap x8 x14)) (_Ap x8 x15)) (_Ap x10 x15)) (_Ap x12 x15)) (_Ap (_Ap (_Ap x9 x14) x15) x16))))))))) x13)) x13))))))))))))))))))).
Axiom MetaIdFunctorThm: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) (_Lam (fun x4:A0 => x4))) (_Lam (fun x4:A0 => _Lam (fun x5:A0 => _Lam (fun x6:A1 => x6)))))))))).
Axiom MetaCompFunctorThm: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _TTpAll (fun A4:Type => _TTpAll (fun A5:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A4 Prop => _All (fun x9:_TpArr A4 (_TpArr A4 (_TpArr A5 Prop)) => _All (fun x10:_TpArr A4 A5 => _All (fun x11:_TpArr A4 (_TpArr A4 (_TpArr A4 (_TpArr A5 (_TpArr A5 A5)))) => _All (fun x12:_TpArr A0 A2 => _All (fun x13:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x14:_TpArr A2 A4 => _All (fun x15:_TpArr A2 (_TpArr A2 (_TpArr A3 A5)) => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x12) x13) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A2) A3) A4) A5) x4) x5) x6) x7) x8) x9) x10) x11) x14) x15) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A4) A5) x0) x1) x2) x3) x8) x9) x10) x11) (_Lam (fun x16:A0 => _Ap x14 (_Ap x12 x16)))) (_Lam (fun x16:A0 => _Lam (fun x17:A0 => _Lam (fun x18:A1 => _Ap (_Ap (_Ap x15 (_Ap x12 x16)) (_Ap x12 x17)) (_Ap (_Ap (_Ap x13 x16) x17) x18))))))))))))))))))))))))))))).
Parameter MetaFunctor_strict: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpAll (fun A2:Type => _TpAll (fun A3:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr (_TpArr A2 Prop) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A3 Prop))) (_TpArr (_TpArr A2 A3) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3))))) (_TpArr (_TpArr A0 A2) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A3))) Prop))))))))))))).
Axiom MetaFunctor_strict_I: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A2) A3) x4) x5) x6) x7) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor_strict A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9))))))))))))))))).
Axiom MetaFunctor_strict_E: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor_strict A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) (_All (fun x10:Prop => _Imp (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A2) A3) x4) x5) x6) x7) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10))) x10)))))))))))))))).
Parameter MetaNatTrans_strict: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpAll (fun A2:Type => _TpAll (fun A3:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr (_TpArr A2 Prop) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A3 Prop))) (_TpArr (_TpArr A2 A3) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3))))) (_TpArr (_TpArr A0 A2) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A3))) (_TpArr (_TpArr A0 A2) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A3))) (_TpArr (_TpArr A0 A3) Prop)))))))))))))))).
Axiom MetaNatTrans_strict_I: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x10:_TpArr A0 A2 => _All (fun x11:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x12:_TpArr A0 A3 => _Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A2) A3) x4) x5) x6) x7) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x10) x11) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans_strict A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12)))))))))))))))))))))).
Axiom MetaNatTrans_strict_E: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x10:_TpArr A0 A2 => _All (fun x11:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x12:_TpArr A0 A3 => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans_strict A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) (_All (fun x13:Prop => _Imp (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A2) A3) x4) x5) x6) x7) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x10) x11) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13))))) x13))))))))))))))))))).
Parameter MetaMonad: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr (_TpArr A0 A0) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A1))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 A1) Prop))))))))).
Axiom MetaMonadI: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A0 A0 => _All (fun x5:_TpArr A0 (_TpArr A0 (_TpArr A1 A1)) => _All (fun x6:_TpArr A0 A1 => _All (fun x7:_TpArr A0 A1 => _Imp (_All (fun x8:A0 => _Imp (_Ap x0 x8) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x4 (_Ap x4 (_Ap x4 x8)))) (_Ap x4 (_Ap x4 x8))) (_Ap x4 x8)) (_Ap x7 x8)) (_Ap (_Ap (_Ap x5 (_Ap x4 (_Ap x4 x8))) (_Ap x4 x8)) (_Ap x7 x8)))) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x4 (_Ap x4 (_Ap x4 x8)))) (_Ap x4 (_Ap x4 x8))) (_Ap x4 x8)) (_Ap x7 x8)) (_Ap x7 (_Ap x4 x8)))))) (_Imp (_All (fun x8:A0 => _Imp (_Ap x0 x8) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x4 x8)) (_Ap x4 (_Ap x4 x8))) (_Ap x4 x8)) (_Ap x7 x8)) (_Ap x6 (_Ap x4 x8)))) (_Ap x2 (_Ap x4 x8))))) (_Imp (_All (fun x8:A0 => _Imp (_Ap x0 x8) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x4 x8)) (_Ap x4 (_Ap x4 x8))) (_Ap x4 x8)) (_Ap x7 x8)) (_Ap (_Ap (_Ap x5 x8) (_Ap x4 x8)) (_Ap x6 x8)))) (_Ap x2 (_Ap x4 x8))))) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaMonad A0) A1) x0) x1) x2) x3) x4) x5) x6) x7))))))))))))).
Axiom MetaMonadE: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A0 A0 => _All (fun x5:_TpArr A0 (_TpArr A0 (_TpArr A1 A1)) => _All (fun x6:_TpArr A0 A1 => _All (fun x7:_TpArr A0 A1 => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaMonad A0) A1) x0) x1) x2) x3) x4) x5) x6) x7) (_All (fun x8:Prop => _Imp (_Imp (_All (fun x9:A0 => _Imp (_Ap x0 x9) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x4 (_Ap x4 (_Ap x4 x9)))) (_Ap x4 (_Ap x4 x9))) (_Ap x4 x9)) (_Ap x7 x9)) (_Ap (_Ap (_Ap x5 (_Ap x4 (_Ap x4 x9))) (_Ap x4 x9)) (_Ap x7 x9)))) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x4 (_Ap x4 (_Ap x4 x9)))) (_Ap x4 (_Ap x4 x9))) (_Ap x4 x9)) (_Ap x7 x9)) (_Ap x7 (_Ap x4 x9)))))) (_Imp (_All (fun x9:A0 => _Imp (_Ap x0 x9) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x4 x9)) (_Ap x4 (_Ap x4 x9))) (_Ap x4 x9)) (_Ap x7 x9)) (_Ap x6 (_Ap x4 x9)))) (_Ap x2 (_Ap x4 x9))))) (_Imp (_All (fun x9:A0 => _Imp (_Ap x0 x9) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x4 x9)) (_Ap x4 (_Ap x4 x9))) (_Ap x4 x9)) (_Ap x7 x9)) (_Ap (_Ap (_Ap x5 x9) (_Ap x4 x9)) (_Ap x6 x9)))) (_Ap x2 (_Ap x4 x9))))) x8))) x8)))))))))))).
Parameter MetaMonad_strict: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr (_TpArr A0 A0) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A1))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 A1) Prop))))))))).
Axiom MetaMonad_strict_I: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A0 A0 => _All (fun x5:_TpArr A0 (_TpArr A0 (_TpArr A1 A1)) => _All (fun x6:_TpArr A0 A1 => _All (fun x7:_TpArr A0 A1 => _Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) x4) x5) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) (_Lam (fun x8:A0 => x8))) (_Lam (fun x8:A0 => _Lam (fun x9:A0 => _Lam (fun x10:A1 => x10))))) x4) x5) x6) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) (_Lam (fun x8:A0 => _Ap x4 (_Ap x4 x8)))) (_Lam (fun x8:A0 => _Lam (fun x9:A0 => _Lam (fun x10:A1 => _Ap (_Ap (_Ap x5 (_Ap x4 x8)) (_Ap x4 x9)) (_Ap (_Ap (_Ap x5 x8) x9) x10)))))) x4) x5) x7) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaMonad A0) A1) x0) x1) x2) x3) x4) x5) x6) x7) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaMonad_strict A0) A1) x0) x1) x2) x3) x4) x5) x6) x7))))))))))))))).
Axiom MetaMonad_strict_E: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A0 A0 => _All (fun x5:_TpArr A0 (_TpArr A0 (_TpArr A1 A1)) => _All (fun x6:_TpArr A0 A1 => _All (fun x7:_TpArr A0 A1 => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaMonad_strict A0) A1) x0) x1) x2) x3) x4) x5) x6) x7) (_All (fun x8:Prop => _Imp (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) x4) x5) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) (_Lam (fun x9:A0 => x9))) (_Lam (fun x9:A0 => _Lam (fun x10:A0 => _Lam (fun x11:A1 => x11))))) x4) x5) x6) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) (_Lam (fun x9:A0 => _Ap x4 (_Ap x4 x9)))) (_Lam (fun x9:A0 => _Lam (fun x10:A0 => _Lam (fun x11:A1 => _Ap (_Ap (_Ap x5 (_Ap x4 x9)) (_Ap x4 x10)) (_Ap (_Ap (_Ap x5 x9) x10) x11)))))) x4) x5) x7) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaMonad A0) A1) x0) x1) x2) x3) x4) x5) x6) x7) x8))))) x8)))))))))))).
Parameter MetaAdjunction: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpAll (fun A2:Type => _TpAll (fun A3:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr (_TpArr A2 Prop) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A3 Prop))) (_TpArr (_TpArr A2 A3) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3))))) (_TpArr (_TpArr A0 A2) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A3))) (_TpArr (_TpArr A2 A0) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A3 A1))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A2 A3) Prop))))))))))))))))).
Axiom MetaAdjunctionI: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x10:_TpArr A2 A0 => _All (fun x11:_TpArr A2 (_TpArr A2 (_TpArr A3 A1)) => _All (fun x12:_TpArr A0 A1 => _All (fun x13:_TpArr A2 A3 => _Imp (_All (fun x14:A0 => _Imp (_Ap x0 x14) (_Ap (_Ap (_TTpAp eq A3) (_Ap (_Ap (_Ap (_Ap (_Ap x7 (_Ap x8 x14)) (_Ap x8 (_Ap x10 (_Ap x8 x14)))) (_Ap x8 x14)) (_Ap x13 (_Ap x8 x14))) (_Ap (_Ap (_Ap x9 x14) (_Ap x10 (_Ap x8 x14))) (_Ap x12 x14)))) (_Ap x6 (_Ap x8 x14))))) (_Imp (_All (fun x14:A2 => _Imp (_Ap x4 x14) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x10 x14)) (_Ap x10 (_Ap x8 (_Ap x10 x14)))) (_Ap x10 x14)) (_Ap (_Ap (_Ap x11 (_Ap x8 (_Ap x10 x14))) x14) (_Ap x13 x14))) (_Ap x12 (_Ap x10 x14)))) (_Ap x2 (_Ap x10 x14))))) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaAdjunction A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13)))))))))))))))))))).
Axiom MetaAdjunctionE: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x10:_TpArr A2 A0 => _All (fun x11:_TpArr A2 (_TpArr A2 (_TpArr A3 A1)) => _All (fun x12:_TpArr A0 A1 => _All (fun x13:_TpArr A2 A3 => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaAdjunction A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) (_All (fun x14:Prop => _Imp (_Imp (_All (fun x15:A0 => _Imp (_Ap x0 x15) (_Ap (_Ap (_TTpAp eq A3) (_Ap (_Ap (_Ap (_Ap (_Ap x7 (_Ap x8 x15)) (_Ap x8 (_Ap x10 (_Ap x8 x15)))) (_Ap x8 x15)) (_Ap x13 (_Ap x8 x15))) (_Ap (_Ap (_Ap x9 x15) (_Ap x10 (_Ap x8 x15))) (_Ap x12 x15)))) (_Ap x6 (_Ap x8 x15))))) (_Imp (_All (fun x15:A2 => _Imp (_Ap x4 x15) (_Ap (_Ap (_TTpAp eq A1) (_Ap (_Ap (_Ap (_Ap (_Ap x3 (_Ap x10 x15)) (_Ap x10 (_Ap x8 (_Ap x10 x15)))) (_Ap x10 x15)) (_Ap (_Ap (_Ap x11 (_Ap x8 (_Ap x10 x15))) x15) (_Ap x13 x15))) (_Ap x12 (_Ap x10 x15)))) (_Ap x2 (_Ap x10 x15))))) x14)) x14)))))))))))))))))))).
Parameter MetaAdjunction_strict: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpAll (fun A2:Type => _TpAll (fun A3:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr (_TpArr A2 Prop) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A3 Prop))) (_TpArr (_TpArr A2 A3) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3))))) (_TpArr (_TpArr A0 A2) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 A3))) (_TpArr (_TpArr A2 A0) (_TpArr (_TpArr A2 (_TpArr A2 (_TpArr A3 A1))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A2 A3) Prop))))))))))))))))).
Axiom MetaAdjunction_strict_I: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x10:_TpArr A2 A0 => _All (fun x11:_TpArr A2 (_TpArr A2 (_TpArr A3 A1)) => _All (fun x12:_TpArr A0 A1 => _All (fun x13:_TpArr A2 A3 => _Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A2) A3) x4) x5) x6) x7) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A2) A3) A0) A1) x4) x5) x6) x7) x0) x1) x2) x3) x10) x11) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) (_Lam (fun x14:A0 => x14))) (_Lam (fun x14:A0 => _Lam (fun x15:A0 => _Lam (fun x16:A1 => x16))))) (_Lam (fun x14:A0 => _Ap x10 (_Ap x8 x14)))) (_Lam (fun x14:A0 => _Lam (fun x15:A0 => _Lam (fun x16:A1 => _Ap (_Ap (_Ap x11 (_Ap x8 x14)) (_Ap x8 x15)) (_Ap (_Ap (_Ap x9 x14) x15) x16)))))) x12) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A2) A3) A2) A3) x4) x5) x6) x7) x4) x5) x6) x7) (_Lam (fun x14:A2 => _Ap x8 (_Ap x10 x14)))) (_Lam (fun x14:A2 => _Lam (fun x15:A2 => _Lam (fun x16:A3 => _Ap (_Ap (_Ap x9 (_Ap x10 x14)) (_Ap x10 x15)) (_Ap (_Ap (_Ap x11 x14) x15) x16)))))) (_Lam (fun x14:A2 => x14))) (_Lam (fun x14:A2 => _Lam (fun x15:A2 => _Lam (fun x16:A3 => x16))))) x13) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaAdjunction A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaAdjunction_strict A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13))))))))))))))))))))))))).
Axiom MetaAdjunction_strict_E: _TTpAll (fun A0:Type => _TTpAll (fun A1:Type => _TTpAll (fun A2:Type => _TTpAll (fun A3:Type => _All (fun x0:_TpArr A0 Prop => _All (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _All (fun x2:_TpArr A0 A1 => _All (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _All (fun x4:_TpArr A2 Prop => _All (fun x5:_TpArr A2 (_TpArr A2 (_TpArr A3 Prop)) => _All (fun x6:_TpArr A2 A3 => _All (fun x7:_TpArr A2 (_TpArr A2 (_TpArr A2 (_TpArr A3 (_TpArr A3 A3)))) => _All (fun x8:_TpArr A0 A2 => _All (fun x9:_TpArr A0 (_TpArr A0 (_TpArr A1 A3)) => _All (fun x10:_TpArr A2 A0 => _All (fun x11:_TpArr A2 (_TpArr A2 (_TpArr A3 A1)) => _All (fun x12:_TpArr A0 A1 => _All (fun x13:_TpArr A2 A3 => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaAdjunction_strict A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) (_All (fun x14:Prop => _Imp (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A0) A1) x0) x1) x2) x3) (_Imp (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat A2) A3) x4) x5) x6) x7) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A2) A3) A0) A1) x4) x5) x6) x7) x0) x1) x2) x3) x10) x11) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A0) A1) A0) A1) x0) x1) x2) x3) x0) x1) x2) x3) (_Lam (fun x15:A0 => x15))) (_Lam (fun x15:A0 => _Lam (fun x16:A0 => _Lam (fun x17:A1 => x17))))) (_Lam (fun x15:A0 => _Ap x10 (_Ap x8 x15)))) (_Lam (fun x15:A0 => _Lam (fun x16:A0 => _Lam (fun x17:A1 => _Ap (_Ap (_Ap x11 (_Ap x8 x15)) (_Ap x8 x16)) (_Ap (_Ap (_Ap x9 x15) x16) x17)))))) x12) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaNatTrans A2) A3) A2) A3) x4) x5) x6) x7) x4) x5) x6) x7) (_Lam (fun x15:A2 => _Ap x8 (_Ap x10 x15)))) (_Lam (fun x15:A2 => _Lam (fun x16:A2 => _Lam (fun x17:A3 => _Ap (_Ap (_Ap x9 (_Ap x10 x15)) (_Ap x10 x16)) (_Ap (_Ap (_Ap x11 x15) x16) x17)))))) (_Lam (fun x15:A2 => x15))) (_Lam (fun x15:A2 => _Lam (fun x16:A2 => _Lam (fun x17:A3 => x17))))) x13) (_Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaAdjunction A0) A1) A2) A3) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14))))))) x14)))))))))))))))))))).

Now when trying to write drafts that try to resolve the category theory conjectures, I could work in a Coq file that starts with

Require Export Catfuncdefs1sig.

Re: Using Coq to help write Dalilcoin drafts

I used my modified dalilcoin to also create Coq readable versions of the content of these three drafts, the ones with category theory conjectures with bounties:

https://github.com/aliibrahim80/dalilco … goryconjs1
https://github.com/aliibrahim80/dalilco … goryconjs2
https://github.com/aliibrahim80/dalilco … goryconjs3

The initial versions were very difficult to work with due to having very big terms. Because of this I have modified my dalilcoin code again to create intermediate abbreviations when it sees closed terms. These are automatically named "abbr1", "abbr2", etc. At first I was going through by hand renaming abbreviations to names I found meaningful, but eventually gave up.

I started to include the full contents of the categoryconjs1,2,3 documents in a semi-Coq readable form, but it makes my post too big. Here is a small part of the first one:

Parameter set:Type.
Parameter In: _TpArr set (_TpArr set Prop).
Parameter Empty: set.
Parameter Union: _TpArr set set.
Parameter UnivOf: _TpArr set set.
Definition terminal_p: _TpAll (fun A0:Type => _TpAll (fun A1:Type => _TpArr (_TpArr A0 Prop) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A1 Prop))) (_TpArr (_TpArr A0 A1) (_TpArr (_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1))))) (_TpArr A0 (_TpArr (_TpArr A0 A1) Prop))))))) := _TTpLam (fun A0:Type => _TTpLam (fun A1:Type => _Lam (fun x0:_TpArr A0 Prop => _Lam (fun x1:_TpArr A0 (_TpArr A0 (_TpArr A1 Prop)) => _Lam (fun x2:_TpArr A0 A1 => _Lam (fun x3:_TpArr A0 (_TpArr A0 (_TpArr A0 (_TpArr A1 (_TpArr A1 A1)))) => _Lam (fun x4:A0 => _Lam (fun x5:_TpArr A0 A1 => _Ap (_Ap and (_Ap x0 x4)) (_All (fun x6:A0 => _Imp (_Ap x0 x6) (_Ap (_Ap and (_Ap (_Ap (_Ap x1 x6) x4) (_Ap x5 x6))) (_All (fun x7:A1 => _Imp (_Ap (_Ap (_Ap x1 x6) x4) x7) (_Ap (_Ap (_TTpAp eq A1) x7) (_Ap x5 x6))))))))))))))).
...
Definition CF: _TpArr set (_TpArr (_TpArr set set) (_TpArr set set)) := _Lam (fun x0:set => _Lam (fun x1:_TpArr set set => _Ap (_Ap (_TTpAp (_TTpAp MetaFuncC set) set) (_Lam (fun x2:set => _Ap (_Ap In x2) x0))) x1)).
Definition CFHom: _TpAll (fun A0:Type => _TpArr (_TpArr A0 (_TpArr A0 (_TpArr (_TpArr set set) Prop))) (_TpArr (_TpArr A0 set) (_TpArr A0 (_TpArr A0 (_TpArr (_TpArr set set) Prop))))) := _TTpLam (fun A0:Type => _Lam (fun x0:_TpArr A0 (_TpArr A0 (_TpArr (_TpArr set set) Prop)) => _Lam (fun x1:_TpArr A0 set => _Lam (fun x2:A0 => _Lam (fun x3:A0 => _Lam (fun x4:_TpArr set set => _Ap (_Ap and (_Ap (_Ap (_Ap x0 x2) x3) x4)) (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncQ set) set) (_Lam (fun x5:set => _Ap (_Ap In x5) (_Ap x1 x2)))) x4))))))).
Let Id_i := (_Lam (fun x0:set => x0)).
Let abbr1 := (_Lam (fun x0:set => _Lam (fun x1:set => _Lam (fun x2:_TpArr set set => _All (fun x3:set => _Imp (_Ap (_Ap In x3) x0) (_Ap (_Ap In (_Ap x2 x3)) x1)))))).
Definition SetHom: _TpArr set (_TpArr set (_TpArr (_TpArr set set) Prop)) := _Ap (_Ap (_TTpAp CFHom set) abbr1) Id_i.
Let abbr2 := (_Lam (fun x0:set => _Lam (fun x1:set => _Lam (fun x2:set => _Lam (fun x3:_TpArr set set => _Lam (fun x4:_TpArr set set => _Ap (_Ap CF x0) (_Lam (fun x5:set => _Ap x3 (_Ap x4 x5))))))))).
Let abbr3 := (_Lam (fun x0:set => _Ap (_Ap CF x0) Id_i)).
Let abbr4 := SetHom.
Let abbr5 := True.
Let abbr6 := (_Lam (fun x0:set => abbr5)).
Definition MetaCatSet_conj: Prop := _Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp MetaCat set) (_TpArr set set)) abbr6) abbr4) abbr3) abbr2.Let abbr10 := (_Lam (fun x0:_TpArr set (_TpArr set set) => _Ap (_TTpAp ex (_TpArr set (_TpArr set (_TpArr set set)))) (_Lam (fun x1:_TpArr set (_TpArr set (_TpArr set set)) => _Ap (_TTpAp ex (_TpArr set (_TpArr set (_TpArr set set)))) (_Lam (fun x2:_TpArr set (_TpArr set (_TpArr set set)) => _Ap (_TTpAp ex (_TpArr set (_TpArr set (_TpArr set (_TpArr (_TpArr set set) (_TpArr (_TpArr set set) (_TpArr set set))))))) (_Lam (fun x3:_TpArr set (_TpArr set (_TpArr set (_TpArr (_TpArr set set) (_TpArr (_TpArr set set) (_TpArr set set))))) => _Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp product_constr_p set) (_TpArr set set)) abbr6) abbr4) abbr3) abbr2) x0) x1) x2) x3)))))))).

The conjectures were printed as definitions. When I wanted to try to prove a conjecture, I created a new Coq file starting with

Require Export Catfuncdefs1sig.

I then copied in the needed dependencies (like Definitions and Lets) from above, include the definition of the conjecture. I change the conjecture from being Definition to being Theorem (removing ": Prop") and start trying to prove it in Coq.

Re: Using Coq to help write Dalilcoin drafts

One thing that becomes very clear is that some types occur repeatedly. First "TpArr set TpArr set set" (i.e., "set -> set -> set") occurs often. In my Coq files I made a definition:

Let set2 := _TpArr set (_TpArr set set).

and textually replaced other occurrences of this with "set2." After this it's clear that some types using 'set2" are repeated, so I did the same with these. For example:

Let set2_5 := _TpArr (_TpArr set2 (_TpArr set2 (_TpArr set2 (_TpArr set2 (_TpArr set2 set2))))) set2.

After doing this, the conjectures in question become (almost) readable. For example:

Theorem MetaCatRngForgetful: _Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor set2_5) (_TpArr set set)) set) (_TpArr set set)) abbr188) abbr186) abbr180) abbr179) KT_i) SetHom) IdSet) CompSet) abbr181) abbr201.

set2_5 is the type of objects of the domain category, "_TpArr set set" is the type of arrows of both categories, and "set" is the type of the codomain category. The remaining arguments are abbreviations meaning the following:

abbr188 : the predicate identifying objects of the domain category (Rings)
abbr186 : the "Hom" predicate identifying arrows of the domain category (Ring homomorphisms)
abbr180 : function giving the identity arrow for each object of the domain category
abbr179 : the composition operator for the domain category
KT_i : the predicate identifying objects of the codomain category (Sets, so the predicate is constantly True, as the manually chosen name suggests)
SetHom : the "Hom" predicate on Set
IdSet : function giving identity arrow on a set
CompSet : composition operator for Set arrows
abbr181 : a function from set2_5 to set "forgetting" the Ring structure
abbr201 : a function taking two objects and an arrow in the Ring cat and giving an arrow in the Set cat (essentially "fun X Y F => F").

Here are the relevant abbreviations to be more precise:

Definition CF: _TpArr set (_TpArr (_TpArr set set) (_TpArr set set)) := _Lam (fun x0:set => _Lam (fun x1:_TpArr set set => _Ap (_Ap (_TTpAp (_TTpAp MetaFuncC set) set) (_Lam (fun x2:set => _Ap (_Ap In x2) x0))) x1)).
Definition CFHom: _TpAll (fun A0:Type => _TpArr (_TpArr A0 (_TpArr A0 (_TpArr (_TpArr set set) Prop))) (_TpArr (_TpArr A0 set) (_TpArr A0 (_TpArr A0 (_TpArr (_TpArr set set) Prop))))) := _TTpLam (fun A0:Type => _Lam (fun x0:_TpArr A0 (_TpArr A0 (_TpArr (_TpArr set set) Prop)) => _Lam (fun x1:_TpArr A0 set => _Lam (fun x2:A0 => _Lam (fun x3:A0 => _Lam (fun x4:_TpArr set set => _Ap (_Ap and (_Ap (_Ap (_Ap x0 x2) x3) x4)) (_Ap (_Ap (_TTpAp (_TTpAp MetaFuncQ set) set) (_Lam (fun x5:set => _Ap (_Ap In x5) (_Ap x1 x2)))) x4))))))).

Let Id_i := (_Lam (fun x0:set => x0)).
Let Mapp_i := (_Lam (fun x0:set => _Lam (fun x1:set => _Lam (fun x2:_TpArr set set => _All (fun x3:set => _Imp (_Ap (_Ap In x3) x0) (_Ap (_Ap In (_Ap x2 x3)) x1)))))).

Definition SetHom: _TpArr set (_TpArr set (_TpArr (_TpArr set set) Prop)) := _Ap (_Ap (_TTpAp CFHom set) Mapp_i) Id_i.

Let CompSet := (_Lam (fun x0:set => _Lam (fun x1:set => _Lam (fun x2:set => _Lam (fun x3:_TpArr set set => _Lam (fun x4:_TpArr set set => _Ap (_Ap CF x0) (_Lam (fun x5:set => _Ap x3 (_Ap x4 x5))))))))).
Let IdSet := (_Lam (fun x0:set => _Ap (_Ap CF x0) Id_i)).
Let KT_i := (_Lam (fun x0:set => True)).

Let Id_ii := _Lam (fun x2:_TpArr set set => x2).

Let set2 := _TpArr set (_TpArr set set).

Let abbr112 := (_Lam (fun x6:set2 => _Lam (fun x7:set2 => _Lam (fun x8:set2 => x6)))).
Let abbr116 := _Lam (fun x8:set2 => x8).
Let abbr117 := _Lam (fun x7:set2 => abbr116).
Let abbr118 := (_Lam (fun x6:set2 => abbr117)).
Let abbr119 := _Lam (fun x5:set2 => _Lam (fun x6:set2 => x5)).
Let abbr120 := (_Lam (fun x4:set2 => abbr119)).

Let set2_5 := _TpArr (_TpArr set2 (_TpArr set2 (_TpArr set2 (_TpArr set2 (_TpArr set2 set2))))) set2.

Let abbr139 := (_Lam (fun x6:set2 => _Lam (fun x7:set2 => _Lam (fun x8:set2 => _Lam (fun x9:set2 => x6))))).
Let abbr143 := (_Lam (fun x6:set2 => abbr120)).
Let abbr144 := (_Lam (fun x4:set2 => abbr112)).

Let abbr147 := (_Lam (fun x3:set2 => abbr118)).

Let abbr178 := (_Lam (fun x6:set2 => _Lam (fun x7:set2 => _Lam (fun x8:set2 => _Lam (fun x9:set2 => _Lam (fun x10:set2 => x6)))))).
Let abbr179 := (_Lam (fun x0:set2_5 => _Lam (fun x1:set2_5 => _Lam (fun x2:set2_5 => _Lam (fun x3:_TpArr set set => _Lam (fun x4:_TpArr set set => _Ap (_Ap CF (_Ap (_Lam (fun x5:set2_5 => _Ap (_Ap (_Ap x5 abbr178) Empty) Empty)) x0)) (_Lam (fun x5:set => _Ap x3 (_Ap x4 x5))))))))).
Let abbr180 := (_Lam (fun x0:set2_5 => _Ap (_Ap CF (_Ap (_Lam (fun x1:set2_5 => _Ap (_Ap (_Ap x1 abbr178) Empty) Empty)) x0)) Id_i)).
Let abbr181 := (_Lam (fun x0:set2_5 => _Ap (_Ap (_Ap x0 abbr178) Empty) Empty)).
Let abbr182 := (_Lam (fun x6:set2 => abbr147)).
Let abbr183 := (_Lam (fun x6:set2 => abbr144)).
Let abbr184 := (_Lam (fun x4:set2 => abbr139)).

Let abbr185a := (_Lam (fun x0:set2_5 => _Lam (fun x1:set2_5 => _Lam (fun x2:_TpArr set set => (_All (fun x3:set => _Imp (_Ap (_Ap In x3) (_Ap abbr181 x0)) (_Ap (_Ap In (_Ap x2 x3)) (_Ap abbr181 x1)))))))).
Let abbr185b := (_Lam (fun x0:set2_5 => _Lam (fun x1:set2_5 => _Lam (fun x2:_TpArr set set => (_Ap (_Ap (_TTpAp eq set) (_Ap x2 (_Ap (_Lam (fun x3:set2_5 => _Ap (_Ap (_Ap x3 abbr184) Empty) Empty)) x0))) (_Ap (_Lam (fun x3:set2_5 => _Ap (_Ap (_Ap x3 abbr184) Empty) Empty)) x1)))))).
Let abbr185c := (_Lam (fun x0:set2_5 => _Lam (fun x1:set2_5 => _Lam (fun x2:_TpArr set set => (_All (fun x3:set => _Imp (_Ap (_Ap In x3) (_Ap abbr181 x0)) (_All (fun x4:set => _Imp (_Ap (_Ap In x4) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap x2 (_Ap (_Ap (_Ap (_Lam (fun x5:set2_5 => _Ap x5 abbr183)) x0) x3) x4))) (_Ap (_Ap (_Ap (_Lam (fun x5:set2_5 => _Ap x5 abbr183)) x1) (_Ap x2 x3)) (_Ap x2 x4))))))))))).
Let abbr185d := (_Lam (fun x0:set2_5 => _Lam (fun x1:set2_5 => _Lam (fun x2:_TpArr set set => (_All (fun x3:set => _Imp (_Ap (_Ap In x3) (_Ap abbr181 x0)) (_All (fun x4:set => _Imp (_Ap (_Ap In x4) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap x2 (_Ap (_Ap (_Ap (_Lam (fun x5:set2_5 => _Ap x5 abbr182)) x0) x3) x4))) (_Ap (_Ap (_Ap (_Lam (fun x5:set2_5 => _Ap x5 abbr182)) x1) (_Ap x2 x3)) (_Ap x2 x4))))))))))).

Let abbr185 := (_Lam (fun x0:set2_5 => _Lam (fun x1:set2_5 => _Lam (fun x2:_TpArr set set => _Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap (_Ap abbr185a x0) x1) x2)) (_Ap (_Ap (_Ap abbr185b x0) x1) x2))) (_Ap (_Ap (_Ap abbr185c x0) x1) x2))) (_Ap (_Ap (_Ap abbr185d x0) x1) x2))))).

Let abbr186 := (_Ap (_Ap (_TTpAp CFHom (set2_5)) abbr185) abbr181).
Let abbr187 := (_Lam (fun x3:set2 => abbr143)).
Let abbr188 := (_Lam (fun x0:set2_5 => _Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap In (_Ap (_Lam (fun x1:set2_5 => _Ap (_Ap (_Ap x1 abbr184) Empty) Empty)) x0)) (_Ap abbr181 x0))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap abbr181 x0)) (_Ap (_Ap In (_Ap (_Ap (_Ap (_Lam (fun x3:set2_5 => _Ap x3 abbr183)) x0) x1) x2)) (_Ap abbr181 x0)))))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x2:set2_5 => _Ap x2 abbr183)) x0) (_Ap (_Lam (fun x2:set2_5 => _Ap (_Ap (_Ap x2 abbr184) Empty) Empty)) x0)) x1)) x1))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x2:set2_5 => _Ap x2 abbr183)) x0) x1) (_Ap (_Lam (fun x2:set2_5 => _Ap (_Ap (_Ap x2 abbr184) Empty) Empty)) x0))) x1))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap abbr181 x0)) (_All (fun x3:set => _Imp (_Ap (_Ap In x3) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr183)) x0) x1) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr183)) x0) x2) x3))) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr183)) x0) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr183)) x0) x1) x2)) x3)))))))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x2:set2_5 => _Ap x2 abbr183)) x0) x1) (_Ap (_Ap (_Lam (fun x2:set2_5 => _Ap (_Ap x2 abbr187) Empty)) x0) x1))) (_Ap (_Lam (fun x2:set2_5 => _Ap (_Ap (_Ap x2 abbr184) Empty) Empty)) x0)))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x2:set2_5 => _Ap x2 abbr183)) x0) (_Ap (_Ap (_Lam (fun x2:set2_5 => _Ap (_Ap x2 abbr187) Empty)) x0) x1)) x1)) (_Ap (_Lam (fun x2:set2_5 => _Ap (_Ap (_Ap x2 abbr184) Empty) Empty)) x0)))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x3:set2_5 => _Ap x3 abbr183)) x0) x1) x2)) (_Ap (_Ap (_Ap (_Lam (fun x3:set2_5 => _Ap x3 abbr183)) x0) x2) x1)))))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap abbr181 x0)) (_All (fun x3:set => _Imp (_Ap (_Ap In x3) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) x1) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) x2) x3))) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) x1) x2)) x3)))))))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap abbr181 x0)) (_All (fun x3:set => _Imp (_Ap (_Ap In x3) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) x1) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr183)) x0) x2) x3))) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr183)) x0) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) x1) x2)) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) x1) x3))))))))))) (_All (fun x1:set => _Imp (_Ap (_Ap In x1) (_Ap abbr181 x0)) (_All (fun x2:set => _Imp (_Ap (_Ap In x2) (_Ap abbr181 x0)) (_All (fun x3:set => _Imp (_Ap (_Ap In x3) (_Ap abbr181 x0)) (_Ap (_Ap (_TTpAp eq set) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr183)) x0) x1) x2)) x3)) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr183)) x0) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) x1) x3)) (_Ap (_Ap (_Ap (_Lam (fun x4:set2_5 => _Ap x4 abbr182)) x0) x2) x3))))))))))).

Let abbr200 := _Lam (fun x1:set2_5 => Id_ii).
Let abbr201 := (_Lam (fun x0:set2_5 => abbr200)).

In the case of "abbr185" I took the Let given to me by dalilcoin and manually separated it into 4 sub abbreviations I conjoined: abbr185a, abbr185b, abbr185c, abbr185d. I say why when describing the proof.

Re: Using Coq to help write Dalilcoin drafts

At first I would use Coq tactics like "apply" to build the proof. Then I would display the proof term and use "exact" in the file. I would then modify the proof term by hand to include wrappers like "_Ap" and "_Lam" in appropriate places so that the whole proof term could be printed in the prefix notation Dalilcoin can read.

Eventually I found I could avoid this by careful use of the "refine" tactic. Here is how I proved the conjecture above in Coq with five steps:

First I use a general lemma I called "MetaCatForgetful_gen" extracting the type and term arguments from relevant arguments in the conjecture. I leave the proof argument blank, leading to a new subgoal.

refine (_PrAp (_TmAp (_TmAp (_TmAp (_TpAp MetaCatForgetful_gen set2_5) abbr188) abbr181) abbr186) _).

The new subgoal is roughly "forall X, Obj X -> forall Y, Obj Y -> forall F, ...". We need to introduce the X, Y and F. We will not need the hypotheses that X and Y are objects, but we still need the lambdas. Instead of "intros", we use a refine with the (proof level) lambda wrappers:

refine
 (_TmLa (fun X:set2_5 => (_PrLa (fun (_: _Ap abbr188 X) =>
 (_TmLa (fun Y:set2_5 => (_PrLa (fun (_: _Ap abbr188 Y) =>
 (_TmLa (fun F:_TpArr set set => _)))))))))).

The result is a goal that can be proven with another lemma I called "CFHomForget":

refine (_TmAp (_TmAp (_TmAp (_PrAp (_TmAp (_TmAp (_TpAp CFHomForget set2_5) abbr181) abbr185) _) X) Y) F).

Here the argument "abbr185" can be found by its use in abbr186 as an argument of "CFHom".

We again need to introduce X, Y and F for the subgoal, along with a hypotheses HF saying F is an arrow (Ring Homomorphism).

refine
 (_TmLa (fun X:set2_5 => 
 (_TmLa (fun Y:set2_5 => 
 (_TmLa (fun F:_TpArr set set =>
 (_PrLa (fun HF => _)))))))).

For some reason, even though there would be no naming conflict, Coq changes these names to X0, Y0 and F0, so I use these names in the last step.

For the last step I need to use HF to prove that the result of applying the "forgetting" functions yield an arrow in the category Set.

HF is a proof of abbr185 X0 Y0 F0. abbr185 X0 Y0 F0 is a conjunction of the form (((abbr185a X0 Y0 F0 "and" _) "and" _) "and" _). It turns out that "abbr185a X0 Y0 F0" (after definitions are expanded) is the same as the goal we want to prove. We complete the proof with a use of "exact":

exact (_PrAp (_TmAp (_TmAp (_TmAp (_TmAp andEL4 (_Ap (_Ap (_Ap abbr185a X0) Y0) F0)) (_Ap (_Ap (_Ap abbr185b X0) Y0) F0)) (_Ap (_Ap (_Ap abbr185c X0) Y0) F0)) (_Ap (_Ap (_Ap abbr185d X0) Y0) F0)) HF).

After this there are no subgoals. We can finish the proof with "Qed."

I then saved a Coq parseable version of the proof term as follows:

Unset Printing Notations.
Set Printing Depth 100.
Print MetaCatRngForgetful.

The printed proof term can be moved into the Coq file with a single "exact."

Then restarting and printing with notations, we get the prefix version Dalilcoin can (almost) read. I say "almost" because Dalilcoin apparently does not allow Let at type level, so the Coq abbreviations for "set2" and "set2_5" cannot be ported to Dalilcoin. Instead the user must textually replace these by their expanded version. Here is the result:

PrAp TmAp TmAp TmAp TpAp MetaCatForgetful_gen TpArr TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr set TpArr set set TpArr set TpArr set set abbr188 abbr181 abbr186 TmLa X TpArr TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr set TpArr set set TpArr set TpArr set set PrLa _ Ap abbr188 X TmLa Y TpArr TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr set TpArr set set TpArr set TpArr set set PrLa _ Ap abbr188 Y TmLa F TpArr set set TmAp TmAp TmAp PrAp TmAp TmAp TpAp CFHomForget TpArr TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr set TpArr set set TpArr set TpArr set set abbr181 abbr185 TmLa X0 TpArr TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr set TpArr set set TpArr set TpArr set set TmLa Y0 TpArr TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr TpArr set TpArr set set TpArr set TpArr set set TpArr set TpArr set set TmLa F0 TpArr set set PrLa HF Ap Ap Ap abbr185 X0 Y0 F0 PrAp TmAp TmAp TmAp TmAp andEL4 Ap Ap Ap abbr185a X0 Y0 F0 Ap Ap Ap abbr185b X0 Y0 F0 Ap Ap Ap abbr185c X0 Y0 F0 Ap Ap Ap abbr185d X0 Y0 F0 HF X Y F

5 (edited by AntHirosaki 2019-10-27 10:39:24)

Re: Using Coq to help write Dalilcoin drafts

To finish this explanation, I should briefly comment on the three lemmas I used. One was "andEL4" and allows one to prove A from (((A and B) and C) and D). This was easy to prove and since I have already done it earlier I can declare it as an Axiom in the Coq file and declare it as a "Known" in the Dalilcoin file.

Coq:

Axiom andEL4 : _All (fun A:Prop => _All (fun B:Prop => _All (fun C:Prop => _All (fun D:Prop => _Imp (_Ap (_Ap and (_Ap (_Ap and (_Ap (_Ap and A) B)) C)) D) A)))).

Dalilcoin:

Known andEL4 : All A Prop All B Prop All C Prop All D Prop Imp Ap Ap and Ap Ap and Ap Ap and A B C D A

The lemma "CFHomForget" provides a way to infer that some "F:set -> set" satisfying CFHom A R U X Y F
also satisfies SetHom (U X) (U Y) F. It turns out it is enough to prove that "R X Y F" implies "Mapp_i (U X) (U Y) F".

Coq:

Axiom CFHomForget : _TTpAll (fun A:Type => _All (fun (U:_TpArr A set) => _All (fun (R:_TpArr A (_TpArr A (_TpArr (_TpArr set set) Prop))) => _Imp (_All (fun X:A => _All (fun Y:A => _All (fun F:_TpArr set set => _Imp (_Ap (_Ap (_Ap R X) Y) F) (_Ap (_Ap (_Ap Mapp_i (_Ap U X)) (_Ap U Y)) F))))) (_All (fun (X:A) => (_All (fun (Y:A) => (_All (fun (F:_TpArr set set) => _Imp (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp CFHom A) R) U) X) Y) F) (_Ap (_Ap (_Ap SetHom (_Ap U X)) (_Ap U Y)) F)))))))))).

Dalilcoin:

Known CFHomForget : TTpAll A All U TpArr A set All R TpArr A TpArr A TpArr TpArr set set Prop Imp All X A All Y A All F TpArr set set Imp Ap Ap Ap R X Y F Ap Ap Ap Mapp_i Ap U X Ap U Y F All X A All Y A All F TpArr set set Imp Ap Ap Ap Ap Ap TTpAp CFHom A R U X Y F Ap Ap Ap SetHom Ap U X Ap U Y F

Finally, the main lemma was "MetaCatForgetful_gen".  It says that if we have a type A, a predicate Obj:A -> Prop, a "forgetful" U:A -> set, a Hom predicate A -> A -> (set -> set) -> Prop (using "set -> set" for arrows), then we have a forgetful functor to Set if we know that "Hom X Y F" implies "SetHom (U X) (U Y) F". This lemma applied for all the conjectures saying that a candidate functor is really a functor.

Coq:

Axiom MetaCatForgetful_gen: _TpAll (fun A => _All (fun Obj: _TpArr A Prop => _All (fun (U:_TpArr A set) => _All (fun (Hom: _TpArr A (_TpArr A (_TpArr (_TpArr set set) Prop))) => _Imp (_All (fun X:A => _Imp (_Ap Obj X) (_All (fun Y:A => _Imp (_Ap Obj Y) (_All (fun F: _TpArr set set => _Imp (_Ap (_Ap (_Ap Hom X) Y) F) (_Ap (_Ap (_Ap SetHom (_Ap U X)) (_Ap U Y)) F))))))) (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_Ap (_TTpAp (_TTpAp (_TTpAp (_TTpAp MetaFunctor A) (_TpArr set set)) set) (_TpArr set set)) (_Lam (fun x0:A => _Ap Obj x0))) Hom) (_Lam (fun x0:A => _Ap (_Ap CF (_Ap U x0)) (_Lam (fun x1:set => x1))))) (_Lam (fun x0:A => _Lam (fun x1:A => _Lam (fun x2:A => _Lam (fun x3:_TpArr set set => _Lam (fun x4:_TpArr set set => _Ap (_Ap CF (_Ap U x0)) (_Lam (fun x5:set => _Ap x3 (_Ap x4 x5)))))))))) (_Lam (fun x0:set => True))) SetHom) (_Lam (fun x0:set => _Ap (_Ap CF x0) (_Lam (fun x1:set => x1))))) (_Lam (fun x0:set => _Lam (fun x1:set => _Lam (fun x2:set => _Lam (fun x3:_TpArr set set => _Lam (fun x4:_TpArr set set => _Ap (_Ap CF x0) (_Lam (fun x5:set => _Ap x3 (_Ap x4 x5)))))))))) U) (_Lam (fun x0:A => _Lam (fun x1:A => _Lam (fun x2:_TpArr set set => x2))))))))).

Dalilcoin:

Known MetaCatForgetful_gen : TTpAll A All Obj TpArr A Prop All U TpArr A set All Hom TpArr A TpArr A TpArr TpArr set set Prop Imp All X A Imp Ap Obj X All Y A Imp Ap Obj Y All F TpArr set set Imp Ap Ap Ap Hom X Y F Ap Ap Ap SetHom Ap U X Ap U Y F Ap Ap Ap Ap Ap Ap Ap Ap Ap Ap TTpAp TTpAp TTpAp TTpAp MetaFunctor A TpArr set set set TpArr set set Lam x0 A Ap Obj x0 Hom Lam x0 A Ap Ap CF Ap U x0 Lam x1 set x1 Lam x0 A Lam _ A Lam _ A Lam x3 TpArr set set Lam x4 TpArr set set Ap Ap CF Ap U x0 Lam x5 set Ap x3 Ap x4 x5 Lam _ set True SetHom Lam x0 set Ap Ap CF x0 Lam x1 set x1 Lam x0 set Lam _ set Lam _ set Lam x3 TpArr set set Lam x4 TpArr set set Ap Ap CF x0 Lam x5 set Ap x3 Ap x4 x5 U Lam _ A Lam _ A Lam x2 TpArr set set x2

Re: Using Coq to help write Dalilcoin drafts

Here is the document with the theorem/proof described above:

https://dalilcoin.com/proofexplorer/que … 55a610ed1b

The specific theorem (MetaCatRngForgetful) is Theorem 0 in the document.

Here is the pure version of the theorem:

https://dalilcoin.com/proofexplorer/que … 744d742fb1

Here is the proof:

https://dalilcoin.com/proofexplorer/que … 3ec5181c24

Here are links to the terms for the three lemmas:

MetaCatForgetful_gen:

https://dalilcoin.com/proofexplorer/que … b12b668e42

CFHomForget:

https://dalilcoin.com/proofexplorer/que … 72e56c921e

andEL4:

https://dalilcoin.com/proofexplorer/que … d92d0ccae2

Re: Using Coq to help write Dalilcoin drafts

Your first file (Dalilcoin.v) didn't work for me, but this is probably due to us using different versions of Coq. Mine is 8.6 (December 2016). It worked for me after adding this as a first line:

Notation "X -> Y" := (forall x:X, Y) (at level 75, right associativity).

Thanks a lot for posting your work. I've spent a few weeks trying to translate Spartan Type Theory into Dalilcoin's format and I suspect using your Coq code will speed things up significantly.

Re: Using Coq to help write Dalilcoin drafts

I am glad to hear it is helping someone. Yes, I am still using an even older version of Coq. Thanks for posting your fix for newer versions.