Skip to content
Snippets Groups Projects
Verified Commit 617084f9 authored by ColinRothgang's avatar ColinRothgang
Browse files

Make extended category theory example more readable

parent a7cd4550
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
scala/latin2/tptp/DIHOLExporter.scala
+ 5
− 3
View file @ 617084f9
......@@ -107,11 +107,13 @@ class DIHOLExporter extends logicExporter {
val tpPred = THFAnnotated(type_pred_decl_name(name), "type",
THF.Typing(type_pred_name(name), predTp), None)
List(tpDecl, tpPred)
case (Context.empty, ctxTm, ret, true, false) =>
case (ctxTp, ctxTm, ret, true, false) =>
// ignore the difference to allow using LF Pis instead of depfun
val ctx = ctxTp ++ ctxTm
pathMap ::= (path, translated_fun_name(name))
val funDecl = THFAnnotated(type_decl_name(name), "type",
THF.Typing(translated_fun_name(name), translate_type(PiOrEmpty(ctxTm, ret))), None)
val retPred = typing_pred(PiOrEmpty(ctxTm, ret), OMS(path))
THF.Typing(translated_fun_name(name), translate_type(PiOrEmpty(ctx, ret))), None)
val retPred = typing_pred(PiOrEmpty(ctx, ret), OMS(path))
lazy val tpAx = THFAnnotated(tp_ax_decl_name(name), "axiom",
THF.Logical(retPred), None)
List(funDecl, tpAx)
......
source/casestudies/2023-cade/MMT_example_problems/cat.mmt
+ 26
− 30
View file @ 617084f9
......@@ -15,40 +15,36 @@ theory Cat : latin:/?DHOL =
theory CatExtended : latin:/?DPHOL =
obj : tp❙
mor : {x:tm obj,y:tm obj} tp ❙
id: tm Πͭ [x] mor x x ❙
comp: tm Πͭ [x] Πͭ [y] Πͭ [z] Πͭ [f:tm mor x y] Πͭ [g:tm mor y z] mor x z ❘# 5 ◦ 4 prec 50 ❙
ax1: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] comp @ x @ y @ y @ m @ (id @ y) =ͭ m ❙
ax2: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] comp @ x @ x @ y @ (id @ x) @ m =ͭ m ❙
id: {x: tm obj} tm mor x x ❙
comp: {x: tm obj, y: tm obj, z: tm obj, f:tm mor x y, g:tm mor y z} tm mor x z ❘ # 5 ◦ 4 prec 50 ❙
ax1: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] (id y) ◦ m =ͭ m ❙
ax2: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] m ◦ (id x) =ͭ m ❙
isoPred : tm Πͭ [u: tm obj] Πͭ [m: tm (mor u u)] bool ❘ = λ[u: tm obj] λ[m: tm (mor u u)] ∃ͭ [i: tm (mor u u)] (comp @ u @ u @ u @ m @ i =ͭ id @ u ) ∧
( (comp @ u @ u @ u @ i @ m) =ͭ (id @ u) ) ❙
isomor = [u: tm obj] (mor u u) | ( [m: mor u u] (isoPred @ u @ m) ) ❙
isIsomorphism : {x:tm obj, y:tm obj, m: tm mor x y} prop ❘ = [x: tm obj, y: tm obj, m: tm mor x y]
∃ͭ [i: tm mor y x] i ◦ m =ͭ id y ∧ m ◦ i =ͭ id x ❘# isIso 3 ❙
areIsomorphic : {x:tm obj, y:tm obj} prop ❘ = [x: tm obj, y: tm obj] ∃ͭ [i: tm mor x y] isIso i ❙
isomorphisms = [u: tm obj] mor u u | ( [m: mor u u] isIso m ) ❙
prod: tm Πͭ [x:tm obj] Πͭ [y:tm obj] obj ❙
proj1: tm Πͭ [x:tm obj] Πͭ [y:tm obj] mor (prod @ x @ y) x ❙
proj2: tm Πͭ [x:tm obj] Πͭ [y:tm obj] mor (prod @ x @ y) y ❙
prod: {x:tm obj, y:tm obj} tm obj ❙
proj1: {x:tm obj, y:tm obj} tm mor (prod x y) x ❙
proj2: {x:tm obj, y:tm obj} tm mor (prod x y) y ❙
/T prodUnivMorph: tm Πͭ [x:tm obj] Πͭ [y:tm obj] Πͭ [z:tm obj] Πͭ [f:tm (mor z x)] Πͭ [g:tm (mor z y)] mor z (prod @ x @ y) ❙
prodInMorphPred: tm Πͭ [x:tm obj] Πͭ [y:tm obj] Πͭ [z:tm obj] Πͭ [f:tm (mor z x)] Πͭ [g:tm (mor z y)] Πͭ [u:tm (mor z (prod @ x @ y))] bool ❘ =
λ[x: tm obj] (λ[y: tm obj] (λ[z: tm obj] (λ[f: tm (mor z x)] (λ[g: tm (mor z y)] (λ[u:tm (mor z (prod @ x @y))] (
( (comp @ z @ (prod @ x @y) @ x @ (proj1 @ x @ y) @ u) =ͭ f) ∧
( (comp @ z @ (prod @ x @y) @ y @ (proj2 @ x @ y) @ u) =ͭ g)
) ))))) ❙
univMorphPred: tm Πͭ [x:tm obj] Πͭ [y:tm obj] Πͭ [p: tm Πͭ [m:tm (mor x y)] bool] Πͭ [m:tm (mor x y)] bool ❘ =
λ[x: tm obj] (λ[y: tm obj] (λ[p: tm Πͭ [m:tm (mor x y)] bool] (λ[m:tm (mor x y)]
( (p @ m) ∧ (∀ͭ[u:tm (mor x y)] (p @ u) ⇒ m =ͭ u ) ) ))) ❙
prodUnivMorphPred: tm Πͭ [x:tm obj] Πͭ [y:tm obj] Πͭ [z:tm obj] Πͭ [f:tm (mor z x)] Πͭ [g:tm (mor z y)] Πͭ [u:tm (mor z (prod @ x @ y))] bool ❘ =
λ[x: tm obj] (λ[y: tm obj] (λ[z: tm obj] (λ[f: tm (mor z x)] (λ[g: tm (mor z y)] (λ[u:tm (mor z (prod @ x @ y))]
(univMorphPred @ x @ y @ (λ[m:tm (mor x y)] prodInMorphPred @ x @ y @ z @ f @ g @ m) @ u) ))))) ❙
prodPred: tm Πͭ [x:tm obj] Πͭ [y:tm obj] Πͭ [xy: tm obj] bool ❘ = λ[x: tm obj] λ[y: tm obj] λ[xy: tm obj]
∀ͭ[z: tm obj] ∀ͭ[f: tm (mor z x)] ∀ͭ[g: tm (mor z y)] ∃ͭ [u: tm (mor z xy)] prodUnivMorphPred @ x @ y @ z @ f @ g @ u ❙
prodUnivMorph_ax: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] (prodPred @ x @ y @ (prod @ x @ y)) ❙
isomorphPred : tm Πͭ [x:tm obj] Πͭ [y:tm obj] Πͭ [m: tm (mor x y)] bool ❘ = λ[x: tm obj] λ[y: tm obj] λ[m: tm (mor x y)]
∃ͭ [i: tm (mor y x)] (((comp @ y @ x @ y @ m @ i) =ͭ (id @ y)) ∧ ((comp @ x @ y @ x @ i @ m) =ͭ (id @ x))) ❙
isoObjPred : tm Πͭ [x:tm obj] Πͭ [y:tm obj] bool ❘ = λ[x: tm obj] λ[y: tm obj] ∃ͭ [i: tm (mor x y)] isomorphPred @ x @ y @ i ❙
factorizesProjections: {x:tm obj, y:tm obj, z:tm obj, f:tm mor z x, g:tm mor z y, u:tm mor z (prod @ x @ y)} prop ❘ =
[x: tm obj, y: tm obj, z: tm obj, f: tm mor z x, g: tm mor z y, u:tm mor z (prod x y)]
u ◦ (proj1 x y) =ͭ f ∧ u ◦ (proj2 x y) =ͭ g ❘# factorizesProjs 4 5 6 ❙
isUniqueMorphismWith: {x:tm obj, y:tm obj, p: {m:tm mor x y} prop, m:tm mor x y} prop ❘ =
[x: tm obj, y: tm obj, p: tm Πͭ [m:tm (mor x y)] bool, m: tm (mor x y)]
p m ∧ ∀ͭ[u:tm mor x y] p u ⇒ m =ͭ u ❙
isUniversalMorphismOfProduct: {x:tm obj, y:tm obj, z:tm obj, f:tm mor z x, g:tm mor z y, u:tm mor z (prod x y)} prop ❘ =
[x: tm obj, y: tm obj, z: tm obj, f: tm mor z x, g: tm mor z y, u:tm mor z (prod x y)]
isUniqueMorphismWith x y ([m:tm mor x y] factorizesProjs f g m) u ❘# isUnivMorProd 4 5 6 ❙
isProd: {x:tm obj, y:tm obj, xy: tm obj} bool ❘ = [x: tm obj, y: tm obj, xy: tm obj]
∀ͭ[z: tm obj] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y] ∃ͭ [u: tm mor z xy] isUnivMorProd f g u ❙
prodUnivMorph_ax: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] isProd x y (prod x y) ❙
uniquenessProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj]
prodPred @ x @ y @ z ⇒ isoObjPred @ z @ (prod @ x @ y) ❙
symmetricProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] isoObjPred @ (prod @ x @ y) @ (prod @ y @ x) ❙
isProd x y z ⇒ areIsomorphic z (prod x y) ❙
symmetricProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] areIsomorphic (prod x y) (prod y x) ❙
❚
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment