(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : Alg _Ψ_542 _X_543 ?1 : _Ω_541 ⇛[ _f_544 ] _Ψ_542 ?2 : _x_547 ∈ ⟦ _Ω_541 ⟧ (_X_543 ∘ _f_544) _I_539 : Set [ at Issue1365.agda:165,37-43 ] _J_540 : Set [ at Issue1365.agda:165,37-43 ] _Ω_541 : Sig _I_539 [ at Issue1365.agda:165,37-43 ] _Ψ_542 : Sig _J_540 [ at Issue1365.agda:165,37-43 ] _X_543 : Pow _J_540 [ at Issue1365.agda:165,37-43 ] _f_544 : _I_539 → _J_540 [ at Issue1365.agda:165,37-43 ] _x_547 : _I_539 [ at Issue1365.agda:165,37-59 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _X_543 (_f_544 _x_547) =< μ (Ω″ ⋆^C W) (proj₂ (f i)) (blocked on _X_543) " nil)
((last . 1) . (agda2-goals-action '(0 1 2)))
(agda2-info-action "*Error*" "Issue1365.agda:165,37-64 (_proj₁_587 , _proj₂_588) ∈ (_V_555 (φ = φ) (m = m) (p = p) (k = k) (v = v) ∘ proj₁) → (_proj₁_587 , _proj₂_588) ∈ ((((λ o → Parameter Ω″ o) ◃ (λ {o} → Arity Ω″) / (λ {o} → input Ω″)) ⋆ (λ z → W z)) ∘ proj₂) !=< μ (Ω″ ⋆^C W) (proj₂ (f i)) when checking that the expression weaken ? ? ? has type proj₂ (f i) ∈ (Ω″ ⋆ W)" nil)
((last . 3) . (agda2-maybe-goto '("Issue1365.agda" . 4948)))
(agda2-highlight-load-and-delete-action)
(agda2-status-action "")
(agda2-info-action "*Error*" "Issue1365.agda:165,37-64 (_proj₁_587 , _proj₂_588) ∈ (_V_555 (φ = φ) (m = m) (p = p) (k = k) (v = v) ∘ proj₁) → (_proj₁_587 , _proj₂_588) ∈ ((((λ o → Parameter Ω″ o) ◃ (λ {o} → Arity Ω″) / (λ {o} → input Ω″)) ⋆ (λ z → W z)) ∘ proj₂) !=< μ (Ω″ ⋆^C W) (proj₂ (f i)) when checking that the expression weaken ? ? ? has type proj₂ (f i) ∈ (Ω″ ⋆ W)" nil)
((last . 3) . (agda2-maybe-goto '("Issue1365.agda" . 4948)))
(agda2-highlight-load-and-delete-action)
(agda2-status-action "")
