diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
index d2b7952..018c62f 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
@@ -97,10 +97,11 @@ lemma cellLeftCartesian : cartesian (cellLeft f u) := by
   simp only [id_obj, mk_left, comp_obj, pullback_obj_left, Functor.comp_map]
   unfold cellLeft
   intros i j f'
-  have α := pullbackMapTriangle (w f u) (e f u)
+  have α := pullbackMapTriangle (w f u) (e f u) u (cellLeftTriangle f u)
   simp only [id_obj, mk_left] at α u
   sorry
 
+
 def cellRightCommSq : CommSq (g f u) (w f u) (v f u) f :=
   IsPullback.toCommSq (IsPullback.of_hasPullback _ _)
 
@@ -110,24 +111,20 @@ def cellRight' : pushforward (g f u) ⋙ map (v f u)
 lemma cellRightCartesian : cartesian (cellRight' f u).hom :=
   cartesian_of_isIso ((cellRight' f u).hom)
 
-def pasteCell1 : pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) ⟶
+abbrev pasteCell1 : pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) ⟶
   pullback (e f u) ⋙ map (w f u) ⋙ pushforward f := by
   apply whiskerLeft
   exact (cellRight' f u).hom
 
-def pasteCell2 : (pullback (e f u) ⋙ map (w f u)) ⋙ pushforward f
-   ⟶ (map u) ⋙ pushforward f := by
-  apply whiskerRight
-  exact cellLeft f u
+abbrev pasteCell2 : (pullback (e f u) ⋙ map (w f u)) ⋙ pushforward f
+   ⟶ (map u) ⋙ pushforward f := whiskerRight (cellLeft f u) _
 
 def pasteCell := pasteCell1 f u ≫ pasteCell2 f u
 
 def paste : cartesian (pasteCell f u) := by
   apply cartesian.comp
-  · unfold pasteCell1
-    apply cartesian.whiskerLeft (cellRightCartesian f u)
-  · unfold pasteCell2
-    apply cartesian.whiskerRight (cellLeftCartesian f u)
+  · exact cartesian.whiskerLeft (cellRightCartesian f u) _
+  · exact cartesian.whiskerRight (cellLeftCartesian f u) _
 
 #check pushforwardPullbackTwoSquare
 
@@ -136,6 +133,10 @@ def pentagonIso : map u ⋙ pushforward f ≅
   pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) := by
   have := cartesian_of_isPullback_to_terminal (pasteCell f u)
   letI : IsIso ((pasteCell f u).app (⊤_ Over ((𝟭 (Over B)).obj (Over.mk u)).left)) := sorry
+  -- by {
+  --   have : TwoSquare (pushforward (g f u)) (Over.pullback _) (Over.pullback _) (pushforward f) := by
+  --    apply pushforwardPullbackTwoSquare _ _ _ f u
+  -- }
   have := isIso_of_cartesian (pasteCell f u) (paste f u)
   exact (asIso (pasteCell f u)).symm
 
diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean
index 3edc114..bd47bb5 100644
--- a/Poly/MvPoly/Basic.lean
+++ b/Poly/MvPoly/Basic.lean
@@ -61,11 +61,6 @@ example [HasInitial C] {X Y : C} (f : Y ⟶ X) :
 
 /-- Given an object `X`, The unique map `initial.to X : ⊥_ C ⟶ X ` is exponentiable. -/
 instance [HasInitial C] (X : C) : ExponentiableMorphism (initial.to X) := sorry
-  -- functor := {
-  --   obj := sorry
-  --   map := sorry
-  -- }
-  -- adj := sorry
 
 /-- The constant polynomial in many variables: for this we need the initial object. -/
 def const {I O : C} [HasInitial C] (A : C) [HasBinaryProduct O A] : MvPoly I O :=
@@ -81,16 +76,53 @@ def sum {I O : C} [HasBinaryCoproducts C] (P Q : MvPoly I O) : MvPoly I O where
   B := P.B ⨿ Q.B
   i := coprod.desc P.i Q.i
   p := coprod.map P.p Q.p
-  exp := sorry
+  exp := by {
+    refine { exists_rightAdjoint := by {
+      have F : Over (P.E ⨿ Q.E) ⥤ Over (P.B ⨿ Q.B) := sorry
+      use F
+      haveI : HasBinaryCoproducts (Over (P.E ⨿ Q.E)) := by {
+        sorry
+      }
+      have hf : PreservesPullbacksOfInclusions F := by {
+        sorry
+      }
+      sorry
+
+
+
+
+
+
+    }
+    }}
   o := coprod.desc P.o Q.o
+--#check PreservesPullbacksOfInclusions
+
+--#check PreservesPullbacksOfInclusions.preservesPullbackInl
+
+
+/-For sums: assuming extensiveness, you can express the slice over
+the sum as the product of slices. Then you can calculate pullback
+ as the product of two functors, amd then you take the products of their adjoints-/
 
 /-- The product of two polynomials in many variables. -/
-def prod {I O : C} [HasBinaryProducts C] [FinitaryExtensive C] (P Q : MvPoly I O) : MvPoly I O where
+def prod {I O : C} [HasBinaryProducts C] [FinitaryExtensive C] (P Q : MvPoly I O) :
+    MvPoly I O where
   E := (pullback (P.p ≫ P.o) Q.o) ⨿ (pullback P.o (Q.p ≫ Q.o))
   B := pullback P.o Q.o
   i := coprod.desc (pullback.fst _ _ ≫ P.i) (pullback.snd _ _ ≫ Q.i)
-  p := coprod.desc (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _) (by aesop) (by aesop)) (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _) (by aesop) (by aesop))
-  exp := sorry -- by extensivity -- PreservesPullbacksOfInclusions
+  p := coprod.desc (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _)
+    (comp_id _) (by rw [comp_id, id_comp]))
+    (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _)
+    (by rw [comp_id, id_comp]) (comp_id _))
+  exp := by {
+    refine { exists_rightAdjoint := by {sorry
+
+    }
+
+
+    }
+  } -- by extensivity -- PreservesPullbacksOfInclusions
   o := pullback.fst (P.o) Q.o ≫ P.o
 
 protected def functor {I O : C} (P : MvPoly I O) :
@@ -99,7 +131,8 @@ protected def functor {I O : C} (P : MvPoly I O) :
 
 variable (I O : C) (P : MvPoly I O)
 
-def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] : Over I → Over O := (P.functor).obj
+def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] :
+  Over I → Over O := (P.functor).obj
 
 /-TODO: write a coercion from `MvPoly` to a functor for evaluation of polynomials at a given
 object.-/
diff --git a/blueprint/src/chapter/all.tex b/blueprint/src/chapter/all.tex
index bf24d5b..e106a43 100644
--- a/blueprint/src/chapter/all.tex
+++ b/blueprint/src/chapter/all.tex
@@ -14,6 +14,8 @@ \chapter{Univaiate Polynomial Functors}
 \input{chapter/uvpoly}
 \chapter{Multivariate Polynomial Functors}
 \input{chapter/mvpoly}
+\chapter{Test}
+\input{chapter/mvpoly}
 
 % \bibliography{refs.bib}{}
 % \bibliographystyle{alpha}
diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex
index 0e7b313..662d98c 100644
--- a/blueprint/src/chapter/mvpoly.tex
+++ b/blueprint/src/chapter/mvpoly.tex
@@ -1,3 +1,144 @@
+<<<<<<< HEAD
+\begin{def}
+  We define a polynomial over C to be a diagram $F$ in C of shape
+  \begin{equation}
+  \lean{MvPoly}
+  \label{equ:poly}
+  \xymatrix{
+  I  & B \ar[l]_s \ar[r]^f & A \ar[r]^t & J \, . }
+  \end{equation}
+  We define $\poly{F}:\slice I \to \slice J$ as the composite
+  \[
+  \xymatrix{
+  \slice{I} \ar[r]^{\pbk{s}} & \slice{B} \ar[r]^{\radj{f}} & \slice{A} \ar[r]^{\ladj{t}} & \slice{J} \, . }
+  \]
+  We refer to $\poly{F}$ as the polynomial functor associated to $F$, or
+  the extension of $F$, and say that $F$ represents $\poly F$.
+\end{def}
+
+\begin{def}
+\lean{MvPoly.sum}
+\uses{structure:MvPoly}
+The sum of two polynomials in many variables.
+\end{def}
+
+\begin{def}
+\lean{MvPoly.prod}
+\uses{structure:MvPoly}
+The product of two polynomials in many variables.
+\end{def}
+
+\begin{para}\label{para:BC-distr}
+  We shall make frequent use of the Beck-Chevalley isomorphisms and
+  of the distributivity law of dependent sums over dependent
+  products~\cite{MoerdijkI:weltc}.  Given a cartesian square
+  \[
+  \xymatrix {
+  \cdot \drpullback \ar[r]^g \ar[d]_u & \cdot \ar[d]^v \\
+  \cdot \ar[r]_f & \cdot
+  }
+  \]
+  the Beck-Chevalley isomorphisms are
+  \[
+    \ladj g \, \pbk u \iso \pbk v \, \ladj f \qquad \text{and} \qquad
+    \radj g \, \pbk u \iso \pbk v \, \radj f \,.
+    \]
+
+  Given maps $C \stackrel u \longrightarrow B \stackrel f \longrightarrow A$,
+  we can construct the diagram
+  \begin{equation}\label{distr-diag}
+  \xymatrixrowsep{40pt}
+  \xymatrixcolsep{27pt}
+  \vcenter{\hbox{
+  \xymatrix @!=0pt {
+  &N \drpullback \ar[rr]^g \ar[ld]_e \ar[dd]^{w=\pbk f(v)}&& M \ar[dd]^{v=\radj f (u)} \\
+  C \ar[rd]_u && & \\
+  &B \ar[rr]_f && A\,,
+  }}}
+  \end{equation}
+  where $w = \pbk f\, \radj f(u)$ and $e$ is the counit
+  of $\pbk{f} \adjoint \radj{f}$.
+  For such diagrams the following
+  distributive law holds:
+  \begin{equation}\label{distr-law}
+  \radj f \, \ladj u \iso \ladj v \, \radj g \, \pbk e \,.
+  \end{equation}
+
+
+\begin{para}
+\label{para:comp}
+\lean{MvPoly.comp}
+\uses{structure:MvPoly}
+We now define the operation of substitution of polynomials, and show that the
+  extension of substitution is composition of polynomial functors, as expected.
+  In particular, the composite of two polynomial functors is again polynomial.
+  Given polynomials
+\[
+\xymatrix{
+ &  B \ar[r]^f  \ar[dl]_{s} & A \ar[dr]^{t} & \\
+ I \ar@{}[rrr]|{F} & & & J } \qquad
+\xymatrix{
+ & D \ar[r]^g \ar[dl]_{u} & C \ar[dr]^{v}   \\
+J \ar@{}[rrr]|{G}& & & K }
+\]
+we say that $F$ is a polynomial from $I$ to $J$ (and $G$ from
+$J$ to $K$), and
+we define $G\circ F$, the substitution of $F$ into $G$, to be the polynomial
+$I \leftarrow N \to M \to K$ constructed via this diagram:
+\begin{equation}
+\label{equ:compspan}
+\xycenter{
+  &  &  & N \ar[dl]_{n} \ar[rr]^{p} \ar@{}[dr] |{(iv)}
+&  & D'
+\ar[dl]^{\varepsilon} \ar[r]^{q} \ar@{}[ddr] |{(ii)} &
+M  \ar[dd]^{w} &  \\
+  &  & B' \ar[dl]_{m} \ar[rr]^{r} \ar@{} [dr]|{(iii)}
+&  & A'  \ar[dr]^{k} \ar[dl]_{h}
+\ar@{} [dd] |{(i)}
+&  &  &  \\
+   & B \ar[rr]^f \ar[dl]_{s} & & A \ar[dr]_{t} &   & D \ar[dl]^{u}
+\ar[r]^{g} & C \ar[dr]^{v} &    \\
+I  &    & &   & J &   &   & K   }
+\end{equation}
+Square $(i)$ is cartesian, and $(ii)$ is a distributivity diagram
+like \eqref{distr-diag}: $w$ is obtained
+by applying $\radj{g}$ to $k$, and $D'$ is the pullback of $M$ along $g$.
+The arrow $\varepsilon: D' \to A'$ is the $k$-component of the counit of
+the adjunction $\ladj g \adjoint \pbk g$.
+Finally, the squares $(iii)$ and $(iv)$ are
+cartesian.
+\end{para}
+
+\begin{proposition}\label{thm:subst}
+\lean{MvPoly.comp.functor}
+\uses{structure:MvPoly, def:MvPoly.comp}
+There is a natural isomorphism
+  $$
+  \poly{G\circ F} \iso \poly{G} \circ \poly{F} .
+  $$
+\end{proposition}
+
+\begin{proof}
+  Referring to Diagram~\eqref{equ:compspan} we have
+  the following chain of natural isomorphisms:
+\begin{eqnarray*}
+\extension{G} \circ \extension{F} & = & \ladj{v} \, \radj{g} \, \pbk{u}  \; \ladj{t}  \, \radj{f}
+\, \pbk{s} \\
+& \iso & \ladj{v} \, \radj{g}  \, \ladj{k}  \, \pbk{h}  \, \radj{f}  \, \pbk{s}\\
+ & \iso &
+\ladj{v} \, \ladj{w}  \, \radj{q}  \, \pbk{\varepsilon}  \, \pbk{h}  \, \radj{f} \, \pbk{s}\\
+& \iso &
+\ladj{v} \, \ladj{w}  \, \radj{q}  \, \radj{p}  \, \pbk{n}  \, \pbk{m} \, \pbk{s}\\
+& \iso &
+\ladj{(v\, w)} \, \radj{(q \, p)}  \, \pbk{(s\, m\, n)}\, \\
+& = & \extension{G \circ F}\,.
+\end{eqnarray*}
+Here we used the Beck-Chevalley isomorphism for the cartesian square
+$(i)$, the distributivity law for $(ii)$, Beck-Chevalley isomorphism
+for the cartesian squares $(iii)$ and $(iv)$, and finally pseudo-functoriality
+of the pullback functors and their adjoints.
+\end{proof}
+=======
 Let $\catC$ be category with pullbacks and terminal object.
 
 \begin{definition}[multivariable polynomial functor]\label{defn:Polynomial}
@@ -18,3 +159,4 @@
   $$\upP \seqbn{X_i}{i \in I} = \seqbn{\sum_{a \in A_j} \prod_{b \in B_a} X_{s(b)}}{j \in J}$$
   A \textbf{polynomial functor} is a functor that is naturally isomorphic to the extension of a polynomial.
   \end{definition}
+>>>>>>> refs/remotes/origin/master