Mercurial > hg > Members > kono > Proof > category
changeset 1098:0484477868fe
explict x in Poly is bad in Internal Language
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 29 Aug 2021 13:44:54 +0900 |
| parents | 321f0fef54c2 |
| children | 34f2f65d33d5 |
| files | src/Polynominal.agda src/ToposIL.agda |
| diffstat | 2 files changed, 114 insertions(+), 97 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Sat Jul 31 06:58:48 2021 +0900 +++ b/src/Polynominal.agda Sun Aug 29 13:44:54 2021 +0900 @@ -34,8 +34,20 @@ -- from page. 51 -- + open Functor + open import Relation.Binary.PropositionalEquality hiding ( [_] ; resp ) renaming ( sym to ≡sym ) + + open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) + data _H≈_ {a b c d : Obj A } ( x : Hom A a b ) (y : Hom A c d ) : Set ( c₁ ⊔ c₂ ⊔ ℓ) where + feq : a ≡ c → b ≡ d → (z : Hom A a b) → z ≅ y → A [ x ≈ z ] → x H≈ y + + record SA {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ) where + field + F : Functor A A + without-x : {b c : Obj A} → (f : Hom A b c) → ¬ ( FMap F f H≈ x ) + data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where i : {b c : Obj A} (k : Hom A b c ) → φ x k ii : φ x {⊤} {a} x @@ -67,9 +79,8 @@ -- if we use equality on f as in A, Poly is ovioously Hom c b of a Category. -- it is better to define A[x] as an extension of A as described before - record Poly (a c b : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + record Poly {a} (x : Hom A １ a) (c b : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where field - x : Hom A １ a f : Hom A b c phi : φ x {b} {c} f @@ -83,14 +94,20 @@ -- since we have A[x] now, we can proceed the proof on p.64 in some possible future + Ax : {a ⊤ : Obj A } ( x : Hom A １ a ) → SA x → Functor A A + Ax {a} {⊤} x sa = record { + FObj = λ a → FObj (SA.F sa) a + ; FMap = λ {c} {d} f → {!!} + ; isFunctor = {!!} + } + -- -- Proposition 6.1 -- -- For every polynominal ψ(x) : b → c in an indeterminate x : 1 → a over a cartesian or cartesian closed -- category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x). - record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where - x = Poly.x p + record Functional-completeness {a b c : Obj A} (x : Hom A １ a ) ( p : Poly x c b ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where field fun : Hom A (a ∧ b) c fp : A [ fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ] @@ -99,15 +116,15 @@ -- ε form -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x - record Fc {a b : Obj A } ( φ : Poly a b １ ) + record Fc {a b : Obj A } (x : Hom A １ a ) ( φ : Poly x b １ ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field sl : Hom A a b g : Hom A １ (b <= a) g = ( sl ∙ π' ) * field - isSelect : A [ ε ∙ < g , Poly.x φ > ≈ Poly.f φ ] - isUnique : (f : Hom A １ (b <= a) ) → A [ ε ∙ < f , Poly.x φ > ≈ Poly.f φ ] + isSelect : A [ ε ∙ < g , x > ≈ Poly.f φ ] + isUnique : (f : Hom A １ (b <= a) ) → A [ ε ∙ < f , x > ≈ Poly.f φ ] → A [ g ≈ f ] -- we should open IsCCC isCCC @@ -144,13 +161,13 @@ ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp )) ⟩ ( k x fp ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨⟩ k x (v fp ) ∎ - k-cong : {a b c : Obj A} → (f g : Poly a c b ) - → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f) ≈ k (Poly.x g) (Poly.phi g) ] - k-cong {a} {b} {c} f g f=f = begin - k (Poly.x f) (Poly.phi f) ≈↑⟨ ki (Poly.x f) (Poly.f f) (Poly.phi f) ⟩ + k-cong : {a b c : Obj A} → (x : Hom A １ a ) → (f g : Poly x c b ) + → A [ Poly.f f ≈ Poly.f g ] → A [ k x (Poly.phi f) ≈ k x (Poly.phi g) ] + k-cong {a} {b} {c} x f g f=f = begin + k x (Poly.phi f) ≈↑⟨ ki x (Poly.f f) (Poly.phi f) ⟩ Poly.f f ∙ π' ≈⟨ car f=f ⟩ - Poly.f g ∙ π' ≈⟨ ki (Poly.x g) (Poly.f g) (Poly.phi g) ⟩ - k (Poly.x g) (Poly.phi g) ∎ + Poly.f g ∙ π' ≈⟨ ki x (Poly.f g) (Poly.phi g) ⟩ + k x (Poly.phi g) ∎ -- proof in p.59 Lambek -- @@ -158,11 +175,11 @@ -- Instead of replacing x in Poly.phi ψ, we can use simple application with this fuctional completeness -- in the internal language of Topos. -- - functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p - functional-completeness {a} {b} {c} p = record { - fun = k (Poly.x p) (Poly.phi p) - ; fp = fc0 (Poly.x p) (Poly.f p) (Poly.phi p) - ; uniq = λ f eq → uniq (Poly.x p) (Poly.f p) (Poly.phi p) f eq + functional-completeness : {a b c : Obj A} (x : Hom A １ a ) ( p : Poly x c b ) → Functional-completeness x p + functional-completeness {a} {b} {c} x p = record { + fun = k x (Poly.phi p) + ; fp = fc0 x (Poly.f p) (Poly.phi p) + ; uniq = λ f eq → uniq x (Poly.f p) (Poly.phi p) f eq } where fc0 : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) → A [ k x phi ∙ < x ∙ ○ b , id1 A b > ≈ f ] @@ -245,61 +262,61 @@ -- fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p -- (ε ∙ < g ∙ π , π' >) ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p -- could be simpler - FC : {a b : Obj A} → (φ : Poly a b １ ) → Fc {a} {b} φ - FC {a} {b} φ = record { - sl = k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > + FC : {a b : Obj A} → (x : Hom A １ a ) → (φ : Poly x b １ ) → Fc {a} {b} x φ + FC {a} {b} x φ = record { + sl = k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ; isSelect = isSelect ; isUnique = uniq } where π-exchg = IsCCC.π-exchg isCCC - fc0 : {b c : Obj A} (p : Poly b c １) → A [ k (Poly.x p ) (Poly.phi p) ∙ < Poly.x p ∙ ○ １ , id1 A １ > ≈ Poly.f p ] - fc0 p = Functional-completeness.fp (functional-completeness p) - gg : A [ ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈ Poly.f φ ] + fc0 : {b c : Obj A} (p : Poly x c １) → A [ k x (Poly.phi p) ∙ < x ∙ ○ １ , id1 A １ > ≈ Poly.f p ] + fc0 p = Functional-completeness.fp (functional-completeness x p) + gg : A [ ( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ x ≈ Poly.f φ ] gg = begin - ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC ) ) ⟩ - k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ∙ Poly.x φ , ○ a ∙ Poly.x φ > ≈⟨ cdr (π-cong idL e2 ) ⟩ - k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ , ○ １ > ≈⟨ cdr (π-cong (trans-hom (sym idR) (cdr e2) ) (sym e2) ) ⟩ - k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ fc0 φ ⟩ + ( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ x ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC ) ) ⟩ + k x (Poly.phi φ) ∙ < id1 A _ ∙ x , ○ a ∙ x > ≈⟨ cdr (π-cong idL e2 ) ⟩ + k x (Poly.phi φ) ∙ < x , ○ １ > ≈⟨ cdr (π-cong (trans-hom (sym idR) (cdr e2) ) (sym e2) ) ⟩ + k x (Poly.phi φ) ∙ < x ∙ ○ １ , id1 A １ > ≈⟨ fc0 φ ⟩ Poly.f φ ∎ - isSelect : A [ ε ∙ < ( ( k (Poly.x φ ) ( Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * , Poly.x φ > ≈ Poly.f φ ] + isSelect : A [ ε ∙ < ( ( k x ( Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * , x > ≈ Poly.f φ ] isSelect = begin - ε ∙ < ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ π') * , Poly.x φ > ≈↑⟨ cdr (π-cong idR refl-hom ) ⟩ - ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ id1 A _ , Poly.x φ > ) ≈⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩ - ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ １ , Poly.x φ > ) ≈↑⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩ - ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (○ a ∙ Poly.x φ) , Poly.x φ > ) ≈↑⟨ cdr (π-cong (sym assoc) idL ) ⟩ - ε ∙ (< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) ∙ Poly.x φ , id1 A _ ∙ Poly.x φ > ) + ε ∙ < ((k (x) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ π') * , x > ≈↑⟨ cdr (π-cong idR refl-hom ) ⟩ + ε ∙ (< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ id1 A _ , x > ) ≈⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩ + ε ∙ (< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ １ , x > ) ≈↑⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩ + ε ∙ (< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (○ a ∙ x) , x > ) ≈↑⟨ cdr (π-cong (sym assoc) idL ) ⟩ + ε ∙ (< (((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) ∙ x , id1 A _ ∙ x > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ - ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) , id1 A _ > ) ∙ Poly.x φ ) + ε ∙ ((< (((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) , id1 A _ > ) ∙ x ) ≈↑⟨ cdr (car (π-cong (cdr (IsCCC.e3a isCCC) ) refl-hom)) ⟩ - ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (π ∙ < ○ a , id1 A _ > )) , id1 A _ > ) ∙ Poly.x φ ) + ε ∙ ((< (((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (π ∙ < ○ a , id1 A _ > )) , id1 A _ > ) ∙ x ) ≈⟨ cdr (car (π-cong assoc (sym (IsCCC.e3b isCCC)) )) ⟩ - ε ∙ ((< ((((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π ) ∙ < ○ a , id1 A _ > ) , (π' ∙ < ○ a , id1 A _ > ) > ) ∙ Poly.x φ ) + ε ∙ ((< ((((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π ) ∙ < ○ a , id1 A _ > ) , (π' ∙ < ○ a , id1 A _ > ) > ) ∙ x ) ≈↑⟨ cdr (car (IsCCC.distr-π isCCC)) ⟩ - ε ∙ ((< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ ) ≈⟨ assoc ⟩ - (ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ) ∙ Poly.x φ ≈⟨ car assoc ⟩ - ((ε ∙ < ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ) ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ + ε ∙ ((< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ∙ x ) ≈⟨ assoc ⟩ + (ε ∙ (< ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ) ∙ x ≈⟨ car assoc ⟩ + ((ε ∙ < ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ) ∙ < ○ a , id1 A _ > ) ∙ x ≈⟨ car (car (IsCCC.e4a isCCC)) ⟩ - ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ ≈↑⟨ car assoc ⟩ - (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ (π' ∙ < ○ a , id1 A _ > ) ) ∙ Poly.x φ ≈⟨ car (cdr (IsCCC.e3b isCCC)) ⟩ - (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ id1 A _ ) ∙ Poly.x φ ≈⟨ car idR ⟩ - ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈⟨ gg ⟩ + ((( k x (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) ∙ < ○ a , id1 A _ > ) ∙ x ≈↑⟨ car assoc ⟩ + (( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ (π' ∙ < ○ a , id1 A _ > ) ) ∙ x ≈⟨ car (cdr (IsCCC.e3b isCCC)) ⟩ + (( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ id1 A _ ) ∙ x ≈⟨ car idR ⟩ + ( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ x ≈⟨ gg ⟩ Poly.f φ ∎ - uniq : (f : Hom A １ (b <= a)) → A [ ε ∙ < f , Poly.x φ > ≈ Poly.f φ ] → - A [ (( k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a > )∙ π' ) * ≈ f ] + uniq : (f : Hom A １ (b <= a)) → A [ ε ∙ < f , x > ≈ Poly.f φ ] → + A [ (( k (x) (Poly.phi φ) ∙ < id1 A _ , ○ a > )∙ π' ) * ≈ f ] uniq f eq = begin - (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * ≈⟨ IsCCC.*-cong isCCC ( begin - (k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ≈↑⟨ assoc ⟩ - k (Poly.x φ) (Poly.phi φ) ∙ (< id1 A _ , ○ a > ∙ π') ≈⟨ car ( sym (Functional-completeness.uniq (functional-completeness φ) _ ( begin - ((ε ∙ < f ∙ π , π' >) ∙ < π' , π >) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈↑⟨ assoc ⟩ - (ε ∙ < f ∙ π , π' >) ∙ ( < π' , π > ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ - (ε ∙ < f ∙ π , π' >) ∙ < π' ∙ < Poly.x φ ∙ ○ １ , id1 A １ > , π ∙ < Poly.x φ ∙ ○ １ , id1 A １ > > + (( k x (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * ≈⟨ IsCCC.*-cong isCCC ( begin + (k (x) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ≈↑⟨ assoc ⟩ + k (x) (Poly.phi φ) ∙ (< id1 A _ , ○ a > ∙ π') ≈⟨ car ( sym (Functional-completeness.uniq (functional-completeness x φ) _ ( begin + ((ε ∙ < f ∙ π , π' >) ∙ < π' , π >) ∙ < x ∙ ○ １ , id1 A １ > ≈↑⟨ assoc ⟩ + (ε ∙ < f ∙ π , π' >) ∙ ( < π' , π > ∙ < x ∙ ○ １ , id1 A １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ + (ε ∙ < f ∙ π , π' >) ∙ < π' ∙ < x ∙ ○ １ , id1 A １ > , π ∙ < x ∙ ○ １ , id1 A １ > > ≈⟨ cdr (π-cong (IsCCC.e3b isCCC) (IsCCC.e3a isCCC)) ⟩ - (ε ∙ < f ∙ π , π' >) ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ≈↑⟨ assoc ⟩ - ε ∙ ( < f ∙ π , π' > ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ - ε ∙ ( < (f ∙ π ) ∙ < id1 A １ , Poly.x φ ∙ ○ １ > , π' ∙ < id1 A １ , Poly.x φ ∙ ○ １ > > ) ≈⟨ cdr (π-cong (sym assoc) (IsCCC.e3b isCCC)) ⟩ - ε ∙ ( < f ∙ (π ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ) , Poly.x φ ∙ ○ １ > ) ≈⟨ cdr (π-cong (cdr (IsCCC.e3a isCCC)) (cdr (trans-hom e2 (sym e2)))) ⟩ - ε ∙ ( < f ∙ id1 A １ , Poly.x φ ∙ id1 A １ > ) ≈⟨ cdr (π-cong idR idR ) ⟩ - ε ∙ < f , Poly.x φ > ≈⟨ eq ⟩ + (ε ∙ < f ∙ π , π' >) ∙ < id1 A １ , x ∙ ○ １ > ≈↑⟨ assoc ⟩ + ε ∙ ( < f ∙ π , π' > ∙ < id1 A １ , x ∙ ○ １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ + ε ∙ ( < (f ∙ π ) ∙ < id1 A １ , x ∙ ○ １ > , π' ∙ < id1 A １ , x ∙ ○ １ > > ) ≈⟨ cdr (π-cong (sym assoc) (IsCCC.e3b isCCC)) ⟩ + ε ∙ ( < f ∙ (π ∙ < id1 A １ , x ∙ ○ １ > ) , x ∙ ○ １ > ) ≈⟨ cdr (π-cong (cdr (IsCCC.e3a isCCC)) (cdr (trans-hom e2 (sym e2)))) ⟩ + ε ∙ ( < f ∙ id1 A １ , x ∙ id1 A １ > ) ≈⟨ cdr (π-cong idR idR ) ⟩ + ε ∙ < f , x > ≈⟨ eq ⟩ Poly.f φ ∎ ))) ⟩ ((ε ∙ < f ∙ π , π' > ) ∙ < π' , π > ) ∙ ( < id1 A _ , ○ a > ∙ π' ) ≈↑⟨ assoc ⟩ (ε ∙ < f ∙ π , π' > ) ∙ (< π' , π > ∙ ( < id1 A _ , ○ a > ∙ π' ) ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
--- a/src/ToposIL.agda Sat Jul 31 06:58:48 2021 +0900 +++ b/src/ToposIL.agda Sun Aug 29 13:44:54 2021 +0900 @@ -19,25 +19,25 @@ record IsLogic (Ω : Obj A) (⊤ : Hom A １ Ω) (P : Obj A → Obj A) (_==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω) (_∈_ : {a : Obj A} (x : Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω) - (select : {a : Obj A} → ( φ : Poly a Ω １ ) → Hom A １ (P a)) - (apply : {a : Obj A} (p : Poly a Ω １ ) → ( x : Hom A １ a ) → Poly a Ω １ ) + (select : {a : Obj A} (x : Hom A １ a) → ( φ : Poly x Ω １ ) → Hom A １ (P a)) + (apply : {a : Obj A} (x : Hom A １ a) (p : Poly x Ω １ ) → ( x : Hom A １ a ) → Poly x Ω １ ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field - isSelect : {a : Obj A} → ( φ : Poly a Ω １ ) → {c : Obj A} (h : Hom A c １ ) - → A [ ( ( Poly.x φ ∈ select φ ) == Poly.f φ ) ∙ h ≈ ⊤ ∙ ○ c ] - uniqueSelect : {a : Obj A} → ( φ : Poly a Ω １ ) → (α : Hom A １ (P a) ) + isSelect : {a : Obj A} → (x : Hom A １ a) → ( φ : Poly x Ω １ ) → {c : Obj A} (h : Hom A c １ ) + → A [ ( ( x ∈ select x φ ) == Poly.f φ ) ∙ h ≈ ⊤ ∙ ○ c ] + uniqueSelect : {a : Obj A} → (x : Hom A １ a) → ( φ : Poly x Ω １ ) → (α : Hom A １ (P a) ) → {c : Obj A} (h : Hom A c １ ) - → A [ ( Poly.f φ == ( Poly.x φ ∈ α ) ) ∙ h ≈ ⊤ ∙ ○ c ] - → A [ ( select φ == α ) ∙ h ≈ ⊤ ∙ ○ c ] - isApply : {a : Obj A} (x y : Hom A １ a ) → (q p : Poly a Ω １ ) + → A [ ( Poly.f φ == ( x ∈ α ) ) ∙ h ≈ ⊤ ∙ ○ c ] + → A [ ( select x φ == α ) ∙ h ≈ ⊤ ∙ ○ c ] + isApply : {a : Obj A} (x y : Hom A １ a ) → (q p : Poly x Ω １ ) → {c : Obj A} (h : Hom A c １ ) → A [ ( x == y ) ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] - → A [ Poly.f (apply p x ) ∙ h ≈ ⊤ ∙ ○ c ] - → A [ Poly.f (apply p y ) ∙ h ≈ ⊤ ∙ ○ c ] - applyCong : {a : Obj A} (x : Hom A １ a ) → (q p : Poly a Ω １ ) + → A [ Poly.f (apply x p x ) ∙ h ≈ ⊤ ∙ ○ c ] + → A [ Poly.f (apply x p y ) ∙ h ≈ ⊤ ∙ ○ c ] + applyCong : {a : Obj A} (x : Hom A １ a ) → (q p : Poly x Ω １ ) → {c : Obj A} (h : Hom A c １ ) → ( A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] ) - → ( A [ Poly.f (apply q x ) ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f (apply p x ) ∙ h ≈ ⊤ ∙ ○ c ] ) + → ( A [ Poly.f (apply x q x ) ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f (apply x p x ) ∙ h ≈ ⊤ ∙ ○ c ] ) record InternalLanguage (Ω : Obj A) (⊤ : Hom A １ Ω) (P : Obj A → Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where @@ -45,14 +45,14 @@ _==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω _∈_ : {a : Obj A} (x : Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω -- { x ∈ a | φ x } : P a - select : {a : Obj A} → ( φ : Poly a Ω １ ) → Hom A １ (P a) - apply : {a : Obj A} (p : Poly a Ω １ ) → ( x : Hom A １ a ) → Poly a Ω １ + select : {a : Obj A} → (x : Hom A １ a) → ( φ : Poly x Ω １ ) → Hom A １ (P a) + apply : {a : Obj A} (x : Hom A １ a) (p : Poly x Ω １ ) → ( x : Hom A １ a ) → Poly x Ω １ isIL : IsLogic Ω ⊤ P _==_ _∈_ select apply - _⊢_ : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) - _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] + _⊢_ : {a b : Obj A} (x : Hom A １ a) (p : Poly x Ω b ) (q : Poly x Ω b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) + _⊢_ {a} {b} x p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] - _,_⊢_ : {a b : Obj A} (p : Poly a Ω b ) (p1 : Poly a Ω b ) (q : Poly a Ω b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) - _,_⊢_ {a} {b} p p1 q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] + _,_⊢_ : {a b : Obj A} (x : Hom A １ a) (p : Poly x Ω b ) (p1 : Poly x Ω b ) (q : Poly x Ω b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) + _,_⊢_ {a} {b} x p p1 q = {c : Obj A} (h : Hom A c b ) → 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 Ω １ @@ -81,18 +81,18 @@ -- functional completeness FC0 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) - FC0 = {a b : Obj A} (t : Topos A c) ( φ : Poly a (Ω t) b) → Functional-completeness φ + FC0 = {a b : Obj A} (t : Topos A c) (x : Hom A １ a) ( φ : Poly x (Ω t) b) → Functional-completeness x φ FC1 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) - FC1 = {a : Obj A} (t : Topos A c) ( φ : Poly a (Ω t) １) → Fc φ + FC1 = {a : Obj A} (t : Topos A c) (x : Hom A １ a) ( φ : Poly x (Ω t) １) → Fc x φ topos→logic : (t : Topos A c ) → ToposNat A １ → FC0 → FC1 → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a) topos→logic t n fc0 fc = record { _==_ = λ {b} f g → A [ char t < id1 A b , id1 A b > (δmono t n ) o < f , g > ] ; _∈_ = λ {a} x α → A [ ε o < α , x > ] -- { x ∈ a | φ x } : P a - ; select = λ {a} φ → Fc.g ( fc t φ ) - ; apply = λ {a} φ x → record { x = x ; f = Functional-completeness.fun (fc0 t φ ) ∙ < x ∙ ○ _ , id1 A _ > ; phi = i _ } + ; select = λ {a} x φ → Fc.g ( fc t x φ ) + ; apply = λ {a} φ x y → record { x = x ; f = Functional-completeness.fun (fc0 t y ? ) ∙ < ? ∙ ○ _ , id1 A _ > ; phi = i _ } ; isIL = record { isSelect = {!!} ; uniqueSelect = {!!} @@ -101,8 +101,8 @@ } } where open ≈-Reasoning A hiding (_∙_) - _⊢_ : {a b : Obj A} (p : Poly a (Topos.Ω t) b ) (q : Poly a (Topos.Ω t) b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) - _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] + _⊢_ : {a b : Obj A} {x : Hom A １ a} (p : Poly x (Topos.Ω t) b ) (q : Poly x (Topos.Ω t) b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) + _⊢_ {a} {b} {x} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] → A [ Poly.f q ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] -- -- iso ○ c @@ -113,18 +113,18 @@ -- + ------→ b -----------→ Ω -- ker h fp / fq -- - tl01 : {a b : Obj A} (p q : Poly a (Topos.Ω t) b ) + tl01 : {a b : Obj A} (x : Hom A １ a) (p q : Poly x (Topos.Ω t) b ) → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] - tl01 {a} {b} p q p<q q<p = begin + tl01 {a} {b} x p q p<q q<p = begin Poly.f p ≈↑⟨ tt p ⟩ char t (equalizer (kp p) ) (eMonic A (kp p)) ≈⟨ IsTopos.char-iso (Topos.isTopos t) (equalizer (kp p) ) (equalizer (kp q) ) (eMonic A (kp p)) (eMonic A (kp q)) pqiso ei ⟩ char t (equalizer (kp q) ) (eMonic A (kp q)) ≈⟨ tt q ⟩ Poly.f q ∎ where open import equalizer using ( monic ) open IsEqualizer renaming ( k to ek ) - kp : (p : Poly a (Topos.Ω t) b ) → Equalizer A _ _ - kp p = Ker t ( Poly.f p ) - ee : (p q : Poly a (Topos.Ω t) b ) → q ⊢ p + kp : (p : Poly x (Topos.Ω t) b ) → Equalizer A _ _ + kp p = Ker t ( Poly.f p ) + ee : (p q : Poly x (Topos.Ω t) b ) → q ⊢ p → A [ A [ Poly.f p o equalizer (Ker t ( Poly.f q )) ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer (Ker t ( Poly.f q ))] ] ee p q q<p = begin Poly.f p o equalizer (Ker t ( Poly.f q )) ≈⟨ q<p _ ( begin @@ -135,9 +135,9 @@ ⊤ t ∙ ○ (equalizer-c (Ker t ( Poly.f q ))) ≈↑⟨ cdr e2 ⟩ ⊤ t ∙ ( ○ b ∙ equalizer (Ker t (Poly.f q) )) ≈⟨ assoc ⟩ (⊤ t ∙ ○ b) ∙ equalizer (Ker t (Poly.f q) ) ∎ - qtop : (p q : Poly a (Topos.Ω t) b ) → q ⊢ p → Hom A (equalizer-c (Ker t ( Poly.f q ))) (equalizer-c (Ker t ( Poly.f p ))) + qtop : (p q : Poly x (Topos.Ω t) b ) → q ⊢ p → Hom A (equalizer-c (Ker t ( Poly.f q ))) (equalizer-c (Ker t ( Poly.f p ))) qtop p q q<p = ek (isEqualizer (Ker t ( Poly.f p))) (equalizer (Ker t ( Poly.f q))) (ee p q q<p) - qq=1 : (p q : Poly a (Topos.Ω t) b ) → (q<p : q ⊢ p ) → (p<q : p ⊢ q) → A [ A [ qtop p q q<p o qtop q p p<q ] ≈ id1 A (equalizer-c (Ker t ( Poly.f p ))) ] + qq=1 : (p q : Poly x (Topos.Ω t) b ) → (q<p : q ⊢ p ) → (p<q : p ⊢ q) → A [ A [ qtop p q q<p o qtop q p p<q ] ≈ id1 A (equalizer-c (Ker t ( Poly.f p ))) ] qq=1 p q q<p p<q = begin qtop p q q<p o qtop q p p<q ≈↑⟨ uniqueness (isEqualizer (Ker t ( Poly.f p ))) (begin equalizer (kp p) ∙ (qtop p q q<p ∙ qtop q p p<q ) ≈⟨ assoc ⟩ @@ -150,12 +150,12 @@ pqiso = record { ≅← = qtop p q q<p ; ≅→ = qtop q p p<q ; iso→ = qq=1 p q q<p p<q ; iso← = qq=1 q p p<q q<p } ei : A [ equalizer (Ker t (Poly.f p)) ≈ A [ equalizer (Ker t (Poly.f q)) o Iso.≅→ pqiso ] ] ei = sym (ek=h (isEqualizer (kp q)) ) - tt : (q : Poly a (Topos.Ω t) b ) → A [ char t (equalizer (Ker t (Poly.f q))) (eMonic A (Ker t (Poly.f q))) ≈ Poly.f q ] + tt : (q : Poly x (Topos.Ω t) b ) → A [ char t (equalizer (Ker t (Poly.f q))) (eMonic A (Ker t (Poly.f q))) ≈ Poly.f q ] tt q = IsTopos.char-uniqueness (Topos.isTopos t) {b} {a} module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P : Obj A → Obj A) (il : InternalLanguage Ω ⊤ P) (t : Topos A c) where open InternalLanguage il - il00 : {a : Obj A} (p : Poly a Ω １ ) → p ⊢ p + il00 : {a : Obj A} (x : Hom A １ a) (p : Poly x Ω １ ) → ?-- p ⊢ p il00 {a} p h eq = eq --- Poly.f p ∙ h ≈ ⊤ ∙ ○ c @@ -185,16 +185,16 @@ il04 {a} x y q p eq q<px h qt = IsLogic.isApply (InternalLanguage.isIL il ) x y q p h (eq h) qt (q<px h qt ) --- ⊨ x ∈ select φ == φ x - il05 : {a : Obj A} → (q : Poly a Ω １ ) - → ⊨ ( ( Poly.x q ∈ select q ) == Poly.f q ) - il05 {a} = IsLogic.isSelect (InternalLanguage.isIL il ) + il05 : {a : Obj A} (x : Hom A １ a) → (q : Poly x Ω １ ) + → ⊨ ( ( x ∈ select q ) == Poly.f q ) + il05 {a} x = IsLogic.isSelect (InternalLanguage.isIL il ) --- q ⊢ φ x == x ∈ α --- ----------------------- --- q ⊢ select φ == α --- - il06 : {a : Obj A} → (q : Poly a Ω １ ) → (α : Hom A １ (P a) ) - → ⊨ ( Poly.f q == ( Poly.x q ∈ α ) ) + il06 : {a : Obj A} (x : Hom A １ a) → (q : Poly a Ω １ ) → (α : Hom A １ (P a) ) + → ⊨ ( Poly.f q == ( x ∈ α ) ) → ⊨ ( select q == α ) - il06 {a} q p eq h = IsLogic.uniqueSelect (InternalLanguage.isIL il ) q p h (eq h) + il06 {a} x q p eq h = IsLogic.uniqueSelect (InternalLanguage.isIL il ) q p h (eq h)