It makes a difference whether we leave out an instance argument entirely or whether we give an underscore or question mark for it:
postulate
id : {t : Set} → t → t
_≡_ : {t : Set} → t → t → Set
⊤ : Set
record FunctorOp (F : Set → Set) : Set₁ where
field
map : ∀{A B} → (A → B) → F A → F B
record FunctorLaws (F : Set → Set) {{O : FunctorOp F}} : Set₁ where
field
map-id : ∀{A : Set} → O .FunctorOp.map (id {A}) ≡ (id {F A})
record ApplyOp (A : Set → Set) {{O : FunctorOp A}} {{L : FunctorLaws A}} : Set₁ where
field
iapply : ∀ {t₁ t₂} → A (t₁ → t₂) → A t₁ → A t₂
record ApplyLaws (A : Set → Set) {{O : FunctorOp A}} {{L : FunctorLaws A}} {{i : ApplyOp A}} : Set₁ where
open ApplyOp {{...}}
field
works : ∀ (f : A (⊤ → ⊤)) → (x : A ⊤) → (iapply f x) ≡ x
fails0 : ∀ (f : A (⊤ → ⊤)) → (x : A ⊤) → (iapply {{L₁ = _}} f x) ≡ x
fails : ∀ (f : A (⊤ → ⊤)) → (x : A ⊤) → (iapply {{L₁ = {!L!}}} f x) ≡ x
Note also the clever renaming of instance argument L to L_1 that Agda performs (see #2018).
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4