--- a/README.md	Sat Apr 24 15:15:17 2021 +0900
+++ b/README.md	Sun Apr 25 21:18:48 2021 +0900
@@ -0,0 +1,62 @@
+Category Exercise on Higher order categorical logic
+====
+
+These are set of Agda exercise for Introduction to Higher order categorical logic.
+
+https://www.amazon.co.jp/gp/product/0521356539
+
+Based on Category Library (https://github.com/shinji-kono/category-agda)
+
+	CCC.agda                 Cartesian closed category p.52 and Topos p.139
+	CCCGraph.agda            CCC generated from Graph (iconmplete) p.55
+	CCCSets.agda             CCC on Sets and Topos on Sets (not on the book)
+	CCChom.agda              CCC as Hom Isomorphism p.54
+	CatExponetial.agda       Functor Cattegory  p.8
+	Comma.agda               Comma category p.27
+	Comma1.agda              Comma category p.27
+	HomReasoning.agda        Reasoning utilities
+	Polynominal.agda         Polynominal Category and functional completeness
+	S.agda                   Simple example on Sets Completeness
+	SetsCompleteness.agda    Completeness of Sets
+	ToposEx.agda             Topos Exercise (incomplete)                p.141
+	ToposIL.agda             Topos Internal Language (incomplete)       p.143
+	ToposSub.agda            Topos Subobject classifier (incomplete)
+	adj-monad.agda           Adjunction implies Monad   p.28
+	applicative.agda         Applicative Functor
+	bi-ccc.agda              Bi-cartesian closed category p.65
+	cat-utility.agda         various definitions
+	category-ex.agda         simple ex
+	code-data.agda           simple ex
+	cokleisli.agda           kleisli category on coMonad
+	comparison-em.agda       Elienburg Moore Comparison
+	comparison-functor.agda  kleisli Comparison
+	em-category.agda         Elienburg Moore Resolution
+	epi.agda                 epi example
+	equalizer.agda           Equalizer example p.21
+	free-monoid.agda         free monoid
+	freyd.agda               Adjoin Functor Theorem p.26
+	freyd1.agda               "
+	freyd2.agda               "
+	graph.agda               Category generated by a Graph 
+	idF.agda                 identit functor
+	kleisli.agda             Kleisli Category
+	level-ex.agda
+	limit-to.agda            Example related to Limits p.24
+	list-level.agda
+	list-monoid-cat.agda
+	list-nat.agda
+	list-nat0.agda
+	list.agda
+	maybe-monad.agda
+	maybeCat.agda
+	monad→monoidal.agda      Monad on Sets is a monoidal functor 
+	monoid-monad.agda        Monad with Monoid  p.28
+	monoidal.agda            Monoidal Functor
+	negnat.agda
+	pullback.agda            Pullback p.24
+	record-ex.agda
+	stdalone-kleisli.agda
+	system-f.agda
+	system-t.agda
+	universal-mapping.agda   Universal mapping p.13
+	yoneda.agda              Yoneda Functor p.11

--- a/src/ToposIL.agda	Sat Apr 24 15:15:17 2021 +0900
+++ b/src/ToposIL.agda	Sun Apr 25 21:18:48 2021 +0900
@@ -39,6 +39,40 @@
      _⊢_  : {a : Obj A}  (p : Poly a  Ω １ ) (q : Poly a  Ω １ ) → Set  ( c₁  ⊔  c₂ ⊔ ℓ ) 
      _⊢_  {a}  p q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙  h  ≈  ⊤ ∙  ○  c  ]
          → A [   Poly.f q ∙ h  ≈  ⊤ ∙  ○  c  ] 
+     _,_⊢_  : {a : Obj A}  (p : Poly a  Ω １ ) (p1 : Poly a  Ω １ ) (q : Poly a  Ω １ ) → Set  ( c₁  ⊔  c₂ ⊔ ℓ ) 
+     _,_⊢_  {a}  p p1 q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙  h  ≈  ⊤ ∙  ○  c  ]
+         → A [   Poly.f p1 ∙ h  ≈  ⊤ ∙  ○  c  ] 
+         → A [   Poly.f q  ∙ h  ≈  ⊤ ∙  ○  c  ] 
+     expr : {a b c  : Obj A}  (p : Hom A １ Ω  )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
+     expr p x = record { x = x ;  f = p ; phi = i }
+
+     apply : {a  : Obj A}  (p : Poly a  Ω １ )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
+     apply {a} p x = apply1 Ω (Poly.f p) (Poly.phi p)  where
+        apply1 :  (Ω : Obj A) (f :  Hom A １  Ω) ( phi  :  φ (Poly.x p) {１} { Ω} f ) →  Poly  a  Ω １
+        apply2 :  (Ω : Obj A) (f :  Hom A １  Ω) ( phi  :  φ (Poly.x p) {１} { Ω} f ) →  Poly.x ( apply1 Ω f phi ) ≡ x
+        apply1 _ f i = record { x = x ; f = f ; phi = i }
+        apply1 _ f ii = record { x = x ; f = x ; phi = ii }
+        apply1 .(c ∧ b) f (iii {_} {c} {b} {g} {h} pg ph ) =
+            record { x = x ; f = < Poly.f (apply1 _ g pg)  , Poly.f (apply1 _ h ph) >
+              ; phi = iii (subst (λ k → φ k (Poly.f ag)) (apply2 _ g pg) (Poly.phi ag))   
+               (subst (λ k → φ k (Poly.f ah)) (apply2 _ h ph) (Poly.phi ah)) }  where
+             ag : Poly  a  c １
+             ag = apply1 _ g pg
+             ah : Poly  a  b １
+             ah = apply1 _ h ph
+        apply1 _ .(_ ∙  _) (iv ph ph₁) = {!!}
+        apply1 _ .(_ *) (v ph) = {!!}
+        apply1 _ f (φ-cong x ph) = {!!}
+        apply2 _ f i = refl
+        apply2 _ f ii = refl
+        apply2 _ f (iii ph ph1) = refl
+        apply2 _ f (iv ph ph1 ) = refl
+        apply2 _ f (v ph) = refl
+        apply2 _ f (φ-cong x ph) = refl
+
+     ⊨_ :   (p : Hom A １ Ω  ) →  Set  ( c₁  ⊔  c₂ ⊔ ℓ )
+     ⊨  p = {c : Obj A} (h : Hom A c １ )  → A [ p  ∙ h  ≈  ⊤ ∙  ○  c ] 
+
 
 --             ○ b
 --       b -----------→ 1
@@ -79,4 +113,22 @@
      il01 : {a : Obj A}  (p : Poly a  Ω １ ) (q : Poly a  Ω １ )
         → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
      il01 {a} p q p<q q<p = {!!}
+
+     il011 : {a : Obj A}  (p q q1 : Poly a  Ω １ ) 
+        → q ⊢ p → q , q1 ⊢ p 
+     il011 {a} p q q1 p<q h tq tq1 = p<q h tq
+
+     il012 : {a : Obj A}  (p q r : Poly a  Ω １ ) 
+        → q ⊢ p → q , p  ⊢ r → q ⊢ r 
+     il012 {a} p q r p<q pq<r h  qt = pq<r h qt (p<q h qt) 
+     
+
+     il02 : {a : Obj A} (x : Hom A １ a ) → {c : Obj A} (h : Hom A c １ )  → A [ ( x == x )  ∙ h  ≈  ⊤ ∙  ○  c ]
+     il02 = {!!}
+
+     --- a == b → φ a  ⊢ φ b
+     il04 : {a : Obj A}  (x y : Hom A １ a ) → (q p : Poly a  Ω １ ) 
+        → {c : Obj A} (h : Hom A c １ )  → A [ ( x == y )  ∙ h  ≈  ⊤ ∙  ○  c ] 
+        → q ⊢ apply p x → q ⊢ apply p y
+     il04 {a} = {!!}