Mercurial > hg > Members > kono > Proof > category
changeset 1013:39e2b29e3279
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 20 Mar 2021 20:48:46 +0900 |
| parents | 5dcbf2b9194e |
| children | 4f1db956d3b4 |
| files | src/Polynominal.agda |
| diffstat | 1 files changed, 14 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Sat Mar 20 20:33:28 2021 +0900 +++ b/src/Polynominal.agda Sat Mar 20 20:48:46 2021 +0900 @@ -279,17 +279,20 @@ f o g ∎ ... | v {_} {_} {_} {f} y = begin ( (k x y o < π o π , < π' o π , π' > >) *) o < x o (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩ - ( (k x y o < π o π , < π' o π , π' > >) o < < x o ○ b , id1 A _ > o π , π' > ) * ≈⟨ {!!} ⟩ - ( k x y o ( < π o π , < π' o π , π' > > o < < x o ○ b , id1 A _ > o π , π' > ) ) * ≈⟨ {!!} ⟩ - ( k x y o < (π o π) o < < x o ○ b , id1 A _ > o π , π' > , < π' o π , π' > o < < x o ○ b , id1 A _ > o π , π' > > ) * ≈⟨ {!!} ⟩ - ( k x y o < π o (π o < < x o ○ b , id1 A _ > o π , π' > ) , < (π' o π) o < < x o ○ b , id1 A _ > o π , π' > , π' o < < x o ○ b , id1 A _ > o π , π' > > > ) * ≈⟨ {!!} ⟩ - ( k x y o < π o ( < x o ○ b , id1 A _ > o π ) , < π' o (π o < < x o ○ b , id1 A _ > o π , π' >) , π' > > ) * ≈⟨ {!!} ⟩ - ( k x y o < (π o < x o ○ b , id1 A _ > o π ) , < π' o (< x o ○ b , id1 A _ > o π ) , π' > > ) * ≈⟨ {!!} ⟩ - ( k x y o < (π o < x o ○ b , id1 A _ > ) o π , < (π' o < x o ○ b , id1 A _ > ) o π , π' > > ) * ≈⟨ {!!} ⟩ - ( k x y o < ( (x o ○ b ) o π ) , < id1 A _ o π , π' > > ) * ≈⟨ {!!} ⟩ - ( k x y o < ( (x o ○ b ) o π ) , < π , π' > > ) * ≈⟨ IsCCC.*-cong isCCC ( cdr (IsCCC.π-cong isCCC {!!} {!!} )) ⟩ - ( k x y o < x o ○ _ , id1 A _ > ) * ≈⟨ IsCCC.*-cong isCCC (fc0 record { hom = f ; phi = y}) ⟩ - f * ∎ + ( (k x y o < π o π , < π' o π , π' > >) o < < x o ○ b , id1 A _ > o π , π' > ) * ≈⟨ IsCCC.*-cong isCCC ( begin + ( k x y o < π o π , < π' o π , π' > >) o < < x o ○ b , id1 A _ > o π , π' > ≈↑⟨ assoc ⟩ + k x y o ( < π o π , < π' o π , π' > > o < < x o ○ b , id1 A _ > o π , π' > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ + k x y o < (π o π) o < < x o ○ b , id1 A _ > o π , π' > , < π' o π , π' > o < < x o ○ b , id1 A _ > o π , π' > > + ≈⟨ cdr (IsCCC.π-cong isCCC (sym assoc) (IsCCC.distr-π isCCC )) ⟩ + k x y o < π o (π o < < x o ○ b , id1 A _ > o π , π' > ) , < (π' o π) o < < x o ○ b , id1 A _ > o π , π' > , π' o < < x o ○ b , id1 A _ > o π , π' > > > ≈⟨ {!!} ⟩ + k x y o < π o ( < x o ○ b , id1 A _ > o π ) , < π' o (π o < < x o ○ b , id1 A _ > o π , π' >) , π' > > ≈⟨ {!!} ⟩ + k x y o < (π o < x o ○ b , id1 A _ > o π ) , < π' o (< x o ○ b , id1 A _ > o π ) , π' > > ≈⟨ {!!} ⟩ + k x y o < (π o < x o ○ b , id1 A _ > ) o π , < (π' o < x o ○ b , id1 A _ > ) o π , π' > > ≈⟨ {!!} ⟩ + k x y o < ( (x o ○ b ) o π ) , < id1 A _ o π , π' > > ≈⟨ {!!} ⟩ + k x y o < ( (x o ○ b ) o π ) , < π , π' > > ≈⟨ cdr (IsCCC.π-cong isCCC {!!} {!!} ) ⟩ + k x y o < x o ○ _ , id1 A _ > ≈⟨ fc0 record { hom = f ; phi = y} ⟩ + f ∎ ) ⟩ + f * ∎ ... | φ-cong y z = {!!}