(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : Alg _Ψ_538 _X_539 ?1 : _Ω_537 ⇛[ _f_540 ] _Ψ_538 ?2 : ⟦ _Ω_537 ⟧ ((λ {x} → _X_539) ∘ _f_540) _x_543 _I_535 : Set [ at Issue1365.agda:165,37-43 ] _J_536 : Set [ at Issue1365.agda:165,37-43 ] _Ω_537 : Sig _I_535 [ at Issue1365.agda:165,37-43 ] _Ψ_538 : Sig _J_536 [ at Issue1365.agda:165,37-43 ] _X_539 : Pow _J_536 [ at Issue1365.agda:165,37-43 ] _f_540 : _I_535 → _J_536 [ at Issue1365.agda:165,37-43 ] _x_543 : _I_535 [ at Issue1365.agda:165,37-59 ] _545 : μ (Ω″ ⋆^C W) (proj₂ (f i)) [ at Issue1365.agda:165,37-64 ] _546 : μ (Ω″ ⋆^C W) (proj₂ (f i)) [ at Issue1365.agda:165,37-64 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _545 := λ {I} {i} {J} {K} {Ω} {Ω′} {Ω″} {U} {V} {W} {f} φ m p k v → weaken (?0 (φ = φ) (m = m) (p = p) (k = k) (v = v)) (?1 (φ = φ) (m = m) (p = p) (k = k) (v = v)) (?2 (φ = φ) (m = m) (p = p) (k = k) (v = v)) [blocked on problem 1049] [1049] _X_539 (_f_540 _x_543) =< μ (Ω″ ⋆^C W) (proj₂ (f i)) : Set " nil)
((last . 1) . (agda2-goals-action '(0 1 2)))
(agda2-info-action "*Error*" "Issue1365.agda:165,37-64 _V_551 _583 → (((λ o → Parameter Ω″ o) ◃ (λ {o} → Arity Ω″) / (λ {o} → input Ω″)) ⋆ (λ z → W z)) _584 !=< μ (Ω″ ⋆^C W) (proj₂ (f i)) of type Set 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 _V_551 _583 → (((λ o → Parameter Ω″ o) ◃ (λ {o} → Arity Ω″) / (λ {o} → input Ω″)) ⋆ (λ z → W z)) _584 !=< μ (Ω″ ⋆^C W) (proj₂ (f i)) of type Set 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 "")
