# 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