On 02/10/2011 04:32 PM, Nils Anders Danielsson wrote:
> f₁commutative : ∀ {ℓ} {TF : Set ℓ → Set ℓ} → op₂f₁ TF → Set (suc ℓ)
> f₁commutative {TF = TF} op =
> ∀ {A} (a b : TF A) → a ⟦ op ⟧ b ≡ b ⟦ op ⟧ a
>
sorry, but brief view of tutorials did not give me meaning of { TF = TF } here. Could you point me right doc, please?