Mercurial > hg > Members > kono > Proof > category
changeset 1060:2458af98786a
FC isSelect done, kcong assumption
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 20 Apr 2021 23:44:21 +0900 |
| parents | e0819260ba18 |
| children | 805a4113ad74 |
| files | src/Polynominal.agda |
| diffstat | 1 files changed, 36 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Tue Apr 20 15:59:28 2021 +0900 +++ b/src/Polynominal.agda Tue Apr 20 23:44:21 2021 +0900 @@ -164,7 +164,7 @@ -- why k x {x ∙ ○ b} (iv ii i ) ≡ k x {x ∙ ○ b} i? Lambek p.60 -- if A is locally small, it is ≡-cong. postulate - k-cong : {a b c : Obj A} → (x : Hom A １ a) → (f g : Hom A b c ) → A [ f ≈ g ] → (fp : φ x {b} {c} f ) (gp : φ x {b} {c} g ) + k-cong : {a b c : Obj A} → (x : Hom A １ a) → (f g : Hom A b c ) → A [ f ≈ g ] → (fp : φ x {b} {c} f ) (gp : φ x {b} {c} g ) → A [ k x fp ≈ k x gp ] uniq : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) → A [ f' ∙ < x ∙ ○ b , id1 A b > ≈ f ] → A [ f' ≈ k x phi ] @@ -182,23 +182,50 @@ f' ∎ ) -- functional completeness ε form + -- + -- g : Hom A １ (b <= a) fun : Hom A (a ∧ １) c + -- fun * ε ∙ < g ∙ π , π' > + -- a -> d <= b <-> (a ∧ b ) -> d + -- + -- fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p + -- (ε ∙ < g ∙ π , π' >) ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p + -- FC : {a b : Obj A} → (φ : Poly a b １ ) → Fc {a} {b} φ FC {a} {b} φ = record { sl = A [ k (Poly.x φ ) (Poly.phi φ) o < id1 A _ , ○ a > ] ; isSelect = begin - ε ∙ < ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ π') * , Poly.x φ > ≈⟨ {!!} ⟩ - ε ∙ < (k (Poly.x φ) (Poly.phi φ)∙ (< id1 A _ , ○ a > ∙ π')) * , Poly.x φ > ≈⟨ {!!} ⟩ - ε ∙ ( < (k (Poly.x φ ) (Poly.phi φ) * ) ∙ (Poly.x φ ∙ ○ １) , id1 A １ > ) ≈⟨ {!!} ⟩ - ε ∙ ( < (k (Poly.x φ ) (Poly.phi φ) * ) ∙ (π ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ) , id1 A １ > ) ≈⟨ {!!} ⟩ - ε ∙ ( < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > , π' ∙ < Poly.x φ ∙ ○ １ , id1 A １ > > ) ≈⟨ {!!} ⟩ - ε ∙ ( < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' > ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ) ≈⟨ assoc ⟩ - (ε ∙ < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' > ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ car ( IsCCC.e4a isCCC ) ⟩ - k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ fc0 φ ⟩ + ε ∙ < ((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 φ > ) + ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ + ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) , id1 A _ > ) ∙ Poly.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 φ ) + ≈⟨ cdr (car (π-cong assoc (sym (IsCCC.e3b isCCC)) )) ⟩ + ε ∙ ((< ((((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π ) ∙ < ○ a , id1 A _ > ) , (π' ∙ < ○ a , id1 A _ > ) > ) ∙ Poly.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 φ + ≈⟨ 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 ⟩ Poly.f φ ∎ ; isUnique = {!!} } where 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 φ ] + 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 φ ⟩ + Poly.f φ ∎ -- end