M2Internship/Report/diapoNotes.md

M2 Presentation

Introduction slide

Notes on my internship

Plan of the presentation

First present what is the subject of my study, and what i tried to achieve.

The whole proof is too formal and complex: Informally prove one specific example.

Then, i will present the «structure» of the global proof, and show some things discovered along the way

GAT and 2-sortification

What is a GAT

A GAT for a function in set

A GAT can be composed of three kinds of lines:

• Sort declarations
• Objects costructors A model is the data of a function from a set to another set i.e. a triple the data of two sets, and a «mapping» between them We can spice up this GAT: Gat of isomorphic functions.
• Equalities

A GAT for a category

Another example of GATs: A category is the data of ...... with ...... such that ......

A GAT for Type Theory

Last example that of type theory -> a lot to add, contructors, equalities ..., just for the example.

2-sortification

Known process Used by Sestini Can simplify a study of GATs to only GATs of two sorts

2-sortification of the Set function GAT

Sort specification is always the same. O will describe «sorts» and El will describe «objects of that sort»

Then, we replace Set occuneces by O and we prefix everything else by El

2-sortification of the Type Theoyr GAT

Goal of the internship

One Example

Category of Models & Generalization

Category of models of the Transformed GAT

Adding transformed sort declarations

Constructing the functors

Contsructing G3

Constructing F3

Adjunction FG

The complete proof & Discoveries

Structure of the proof

Fibration of C

S from syntax

Conclusion

Conclusion

Future work