agda の abstract

圏論の Sheaf のところまでできたんですが、一箇所、つなげると agda が止まらなくなるところがある

Chat GPT と相談しながらやってたら、abstract が使えると。いつのまに、そんなものが登場したんだ?

確かに通る。しかも、

{-# OPTIONS --cubical-compatible --safe #-}

と両立する。すごい

値の接続は見ずに、型が一致してれば良いというものらしい

Γm : (p : Obj (top / X)) → {A B : Obj OX} → Hom OX A B → Hom HODSets (Γo p A) (Γo p B)
Γm p {a} {b} b⊆a = record {
　　　　 func = λ qs → & (F→FuncHOD (dfunc p {a} {b} b⊆a qs) )
　　　 ; is-func = Γo-⊆ p {a} {b} b⊆a
　　　 ; func-wld = lem02
　　 } where
　 lem02 : {x y : Ordinal} (ax : odef (Γo p a) x) (ay : odef (Γo p a) y) → x ≡ y
　　　 →　& (F→FuncHOD (dfunc p {a} {b} b⊆a ax)) ≡ & (F→FuncHOD (dfunc p {a} {b} b⊆a ay))
　 lem02　{x} {y} ax ay eq = ==→o≡ ( FuncEQ→HODEQ (dfunc p {a} {b} b⊆a　ax) (dfunc p {a} {b} b⊆a ay) lem10 )　where
　　　　-- lem10 it will take long time to check, so we need abstract
　　　 abstract
　　　　　 lem10 : (z : Ordinal) (az : odef (SObj.s b) z) → FuncEQ (dfunc p {a} {b} b⊆a ax) (dfunc p {a} {b} b⊆a ay) z az
　　　　　 lem10 z az = begin
　　　　　　　Func.func (dfunc p {a} {b} b⊆a ax) az　≡⟨ ΓCont-eq ax ay eq z (b⊆a az) ⟩
　　　　　　　Func.func (dfunc p {a} {b} b⊆a ay) az　∎　where open ≡-Reasoning