Closed banacorn closed 4 years ago
platform: Darwin
(agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Ch2-7 (/Users/banacorn/agda/hott/src/Ch2-7.agda).\n" t)
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-0")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-1") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-2") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-3") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-4") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-5") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-6") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-7") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-8")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-9") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-10")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-11") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-12")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-13")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-14")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-15")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-16")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-17")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-18")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-19")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-20")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-21") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-22")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-23") (agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-24")
(agda2-highlight-load-and-delete-action "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-25")
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : A → Set (a ⊔ b)\n?1 : A → Set a\n?2 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) → Set b\n?3 : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))\n?4\n : Σ-syntax (proj₁ _x_552 ≡ proj₁ f)\n (λ p₁ →\n transport (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) p₁\n (proj₂ _x_552)\n ≡ proj₂ f)\n?5\n : (p : x ≡ y)\n (f : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) →\n transport (λ v → Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) p\n f\n ≡ (transport (λ v → A) p (proj₁ f) , _568 (p = p) (f = f))\n_x_552 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-52 ]\n_565 : ?2 _x_552 [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109 ]\n_566 : ?2 _x_552 [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109 ]\n_567\n : Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110 ]\n_568\n : Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110 ]\n\n———— Errors ————————————————————————————————————————————————\nFailed to solve the following constraints:\n _567\n := λ {a} {b} {A} {P} {Q} {x} {y} p f →\n transport (?2 (p = p) (f = f))\n (Definition-2-7-2-ii (_x_552 (p = p) (f = f)) f\n (?4 (p = p) (f = f)))\n (_566 (p = p) (f = f))\n [blocked on problem 1034]\n [1034] ?2 f\n =< Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u))\n : Set b\n _565 := λ {a} {b} {A} {P} {Q} {x} {y} p → proj₂\n [blocked on problem 1033]\n [1033] Σ (P (proj₁ f)) (λ u → Q (proj₁ f , u)) =< ?2 _x_552 : Set b\n" nil) ((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
Agda2>
``` ["agda2-status-action"] ``` ``` ["agda2-info-action", "*Type-checking*", "nil"] ``` ``` ["agda2-highlight-clear"] ``` ``` ["agda2-info-action", "*Type-checking*", "Checking Ch2-7 (/Users/banacorn/agda/hott/src/Ch2-7.agda).\n", "t"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-0"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-1"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-2"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-3"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-4"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-5"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-6"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-7"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-8"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-9"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-10"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-11"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-12"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-13"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-14"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-15"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-16"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-17"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-18"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-19"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-20"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-21"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-22"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-23"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-24"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-25"] ``` ``` ["agda2-status-action"] ``` ``` ["agda2-info-action", "*All Goals, Errors*", "?0 : A → Set (a ⊔ b)\n?1 : A → Set a\n?2 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) → Set b\n?3 : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))\n?4\n : Σ-syntax (proj₁ _x_552 ≡ proj₁ f)\n (λ p₁ →\n transport (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) p₁\n (proj₂ _x_552)\n ≡ proj₂ f)\n?5\n : (p : x ≡ y)\n (f : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) →\n transport (λ v → Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) p\n f\n ≡ (transport (λ v → A) p (proj₁ f) , _568 (p = p) (f = f))\n_x_552 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-52 ]\n_565 : ?2 _x_552 [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109 ]\n_566 : ?2 _x_552 [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109 ]\n_567\n : Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110 ]\n_568\n : Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110 ]\n\n———— Errors ————————————————————————————————————————————————\nFailed to solve the following constraints:\n _567\n := λ {a} {b} {A} {P} {Q} {x} {y} p f →\n transport (?2 (p = p) (f = f))\n (Definition-2-7-2-ii (_x_552 (p = p) (f = f)) f\n (?4 (p = p) (f = f)))\n (_566 (p = p) (f = f))\n [blocked on problem 1034]\n [1034] ?2 f\n =< Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u))\n : Set b\n _565 := λ {a} {b} {A} {P} {Q} {x} {y} p → proj₂\n [blocked on problem 1033]\n [1033] Σ (P (proj₁ f)) (λ u → Q (proj₁ f , u)) =< ?2 _x_552 : Set b\n", "nil"] ``` ``` [["last", ".", "1"], ".", ["agda2-goals-action", ["0", "1", "2", "3", "4", "5"]]] ``` ``` "Agda2>" ```
``` NoStatus ``` ``` ClearRunningInfo ``` ``` ClearHighlighting ``` ``` RunningInfo 1 Checking Ch2-7 (/Users/banacorn/agda/hott/src/Ch2-7.agda).\n ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-0 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-1 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-2 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-3 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-4 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-5 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-6 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-7 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-8 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-9 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-10 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-11 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-12 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-13 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-14 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-15 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-16 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-17 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-18 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-19 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-20 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-21 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-22 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-23 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-24 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-25 ``` ``` NoStatus ``` ``` DisplayInfo AllGoalsWarnings Metas *All Goals, Errors* [Output ?0 : A → Set (a ⊔ b), Output ?1 : A → Set a, Output ?2 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) → Set b, Output ?3 : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))), Output ?4 : Σ-syntax (proj₁ _x __552 ≡ proj₁ f) (λ p₁ → transport (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) p₁ (proj₂ _x __552 ) ≡ proj₂ f), Output ?5 : (p : x ≡ y) (f : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) → transport (λ v → Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) p f ≡ (transport (λ v → A) p (proj₁ f) , __568 (p = p) (f = f))] [Output _x __552 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-52, Output __565 : ?2 _x __552 /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109, Output __566 : ?2 _x __552 /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109, Output __567 : Σ (P (transport (λ v → A) p (proj₁ f))) (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110, Output __568 : Σ (P (transport (λ v → A) p (proj₁ f))) (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110] [] [[Failed to solve the following constraints: _567 := λ {a} {b} {A} {P} {Q} {x} {y} p f → transport (?2 (p = p) (f = f)) (Definition-2-7-2-ii (_x_552 (p = p) (f = f)) f (?4 (p = p) (f = f))) (_566 (p = p) (f = f)) [blocked on problem 1034] [1034] ?2 f =< Σ (P (transport (λ v → A) p (proj₁ f))) (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) : Set b _565 := λ {a} {b} {A} {P} {Q} {x} {y} p → proj₂ [blocked on problem 1033] [1033] Σ (P (proj₁ f)) (λ u → Q (proj₁ f , u)) =< ?2 _x_552 : Set b ]] ``` ``` InteractionPoints [0, 1, 2, 3, 4, 5] ```
Auto (Goal 3)
``` cannot read: IOTCM "/Users/banacorn/agda/hott/src/Ch2-7.agda" NonInteractive Indirect ( Cmd_auto 3 (intervalsToRange (Just (mkAbsolute "/Users/banacorn/agda/hott/src/Ch2-7.agda")) [Interval (Pn () 3554 108 84) (Pn () 3555 108 87)]) "" ) Agda2> ```
``` "Agda2>" ```
``` Parse error code: S4 "cannot read: IOTCM "/Users/banacorn/agda/hott/src/Ch2-7.agda" NonInteractive Indirect ( Cmd_auto 3 (intervalsToRange (Just (mkAbsolute "/Users/banacorn/agda/hott/src/Ch2-7.agda")) [Interval (Pn () 3554 108 84) (Pn () 3555 108 87)]) "" )" ```
Parse Log
platform: Darwin
raw text
s-expression
``` ["agda2-status-action"] ``` ``` ["agda2-info-action", "*Type-checking*", "nil"] ``` ``` ["agda2-highlight-clear"] ``` ``` ["agda2-info-action", "*Type-checking*", "Checking Ch2-7 (/Users/banacorn/agda/hott/src/Ch2-7.agda).\n", "t"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-0"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-1"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-2"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-3"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-4"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-5"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-6"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-7"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-8"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-9"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-10"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-11"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-12"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-13"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-14"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-15"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-16"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-17"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-18"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-19"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-20"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-21"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-22"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-23"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-24"] ``` ``` ["agda2-highlight-load-and-delete-action", "/var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-25"] ``` ``` ["agda2-status-action"] ``` ``` ["agda2-info-action", "*All Goals, Errors*", "?0 : A → Set (a ⊔ b)\n?1 : A → Set a\n?2 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) → Set b\n?3 : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))\n?4\n : Σ-syntax (proj₁ _x_552 ≡ proj₁ f)\n (λ p₁ →\n transport (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) p₁\n (proj₂ _x_552)\n ≡ proj₂ f)\n?5\n : (p : x ≡ y)\n (f : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) →\n transport (λ v → Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) p\n f\n ≡ (transport (λ v → A) p (proj₁ f) , _568 (p = p) (f = f))\n_x_552 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-52 ]\n_565 : ?2 _x_552 [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109 ]\n_566 : ?2 _x_552 [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109 ]\n_567\n : Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110 ]\n_568\n : Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) [ at /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110 ]\n\n———— Errors ————————————————————————————————————————————————\nFailed to solve the following constraints:\n _567\n := λ {a} {b} {A} {P} {Q} {x} {y} p f →\n transport (?2 (p = p) (f = f))\n (Definition-2-7-2-ii (_x_552 (p = p) (f = f)) f\n (?4 (p = p) (f = f)))\n (_566 (p = p) (f = f))\n [blocked on problem 1034]\n [1034] ?2 f\n =< Σ (P (transport (λ v → A) p (proj₁ f)))\n (λ u → Q (transport (λ v → A) p (proj₁ f) , u))\n : Set b\n _565 := λ {a} {b} {A} {P} {Q} {x} {y} p → proj₂\n [blocked on problem 1033]\n [1033] Σ (P (proj₁ f)) (λ u → Q (proj₁ f , u)) =< ?2 _x_552 : Set b\n", "nil"] ``` ``` [["last", ".", "1"], ".", ["agda2-goals-action", ["0", "1", "2", "3", "4", "5"]]] ``` ``` "Agda2>" ```
response
``` NoStatus ``` ``` ClearRunningInfo ``` ``` ClearHighlighting ``` ``` RunningInfo 1 Checking Ch2-7 (/Users/banacorn/agda/hott/src/Ch2-7.agda).\n ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-0 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-1 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-2 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-3 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-4 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-5 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-6 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-7 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-8 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-9 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-10 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-11 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-12 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-13 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-14 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-15 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-16 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-17 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-18 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-19 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-20 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-21 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-22 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-23 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-24 ``` ``` HighlightingInfoIndirect /var/folders/fw/gsq83z9j6_j5w6hrzj7480x00000gn/T/agda2-mode74503-25 ``` ``` NoStatus ``` ``` DisplayInfo AllGoalsWarnings Metas *All Goals, Errors* [Output ?0 : A → Set (a ⊔ b), Output ?1 : A → Set a, Output ?2 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) → Set b, Output ?3 : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))), Output ?4 : Σ-syntax (proj₁ _x __552 ≡ proj₁ f) (λ p₁ → transport (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) p₁ (proj₂ _x __552 ) ≡ proj₂ f), Output ?5 : (p : x ≡ y) (f : Σ-syntax A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) → transport (λ v → Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u)))) p f ≡ (transport (λ v → A) p (proj₁ f) , __568 (p = p) (f = f))] [Output _x __552 : Σ A (λ x₁ → Σ-syntax (P x₁) (λ u → Q (x₁ , u))) /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-52, Output __565 : ?2 _x __552 /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109, Output __566 : ?2 _x __552 /Users/banacorn/agda/hott/src/Ch2-7.agda:108,102-109, Output __567 : Σ (P (transport (λ v → A) p (proj₁ f))) (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110, Output __568 : Σ (P (transport (λ v → A) p (proj₁ f))) (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) /Users/banacorn/agda/hott/src/Ch2-7.agda:108,43-110] [] [[Failed to solve the following constraints: _567 := λ {a} {b} {A} {P} {Q} {x} {y} p f → transport (?2 (p = p) (f = f)) (Definition-2-7-2-ii (_x_552 (p = p) (f = f)) f (?4 (p = p) (f = f))) (_566 (p = p) (f = f)) [blocked on problem 1034] [1034] ?2 f =< Σ (P (transport (λ v → A) p (proj₁ f))) (λ u → Q (transport (λ v → A) p (proj₁ f) , u)) : Set b _565 := λ {a} {b} {A} {P} {Q} {x} {y} p → proj₂ [blocked on problem 1033] [1033] Σ (P (proj₁ f)) (λ u → Q (proj₁ f , u)) =< ?2 _x_552 : Set b ]] ``` ``` InteractionPoints [0, 1, 2, 3, 4, 5] ```
error
Auto (Goal 3)
raw text
``` cannot read: IOTCM "/Users/banacorn/agda/hott/src/Ch2-7.agda" NonInteractive Indirect ( Cmd_auto 3 (intervalsToRange (Just (mkAbsolute "/Users/banacorn/agda/hott/src/Ch2-7.agda")) [Interval (Pn () 3554 108 84) (Pn () 3555 108 87)]) "" ) Agda2> ```
s-expression
``` "Agda2>" ```
response
error
``` Parse error code: S4 "cannot read: IOTCM "/Users/banacorn/agda/hott/src/Ch2-7.agda" NonInteractive Indirect ( Cmd_auto 3 (intervalsToRange (Just (mkAbsolute "/Users/banacorn/agda/hott/src/Ch2-7.agda")) [Interval (Pn () 3554 108 84) (Pn () 3555 108 87)]) "" )" ```