Agda 표준 라이브러리

🐔 Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_
☘️ "_Preserves_⟶_가 뭔데"
🐔 f Preserves P ⟶ Q = P =[ f ]⇒ Q
☘️ "_=[_]⇒_가 뭔데"
🐔 P =[ f ]⇒ Q = P ⇒ (Q on f)
☘️ "_⇒_은 뭐고 on은 뭔데"
🐔 P ⇒ Q = ∀ {x y} → P x y → Q x y, _*_ on f = f -⟨ _*_ ⟩- f
☘️ "_-⟨_⟩-_이 뭔데"
🐔 f -⟨ _*_ ⟩- g = f -⟨ const ∣ -⟪ _*_ ⟫- ∣ constᵣ ⟩- g
☘️ "const랑 constᵣ은 아는데 _-⟨_∣이랑 ∣_⟩-_은 뭔데"
🐔 f -⟨ _*_ ∣ = f ∘₂ const -⟪ _*_ ∣, ∣ _*_ ⟩- g = ∣ _*_ ⟫- g ∘₂ constᵣ
☘️ "(f ∘₂ g) x y = f (g x y)일 거고 _-⟪_∣이랑 ∣_⟫-_은 또 뭔데"
🐔f -⟪ _*_ ∣ = f -⟪ _*_ ⟫- constᵣ, ∣ _*_ ⟫- g = const -⟪ _*_ ⟫- g
☘️ "_-⟪_⟫-_이 뭔데"
🐔 f -⟪ _*_ ⟫- g = λ x y → f x y * g x y
☘️ "애효 이게 다 뭐야;; eval해봐"
🐔 Monotonic₁ _≤_ _⊑_ f = ∀ {x y} → x ≤ y → f x _⊑_ f y
☘️ "............."

오랜 숙원이었던 개인 페이지를 제작했습니다. typst를 단일 신뢰의 원천으로 작동하고, 종이 인쇄에 최적화된 pdf와 svg(인쇄용)을 제공합니다.

https://gaebalgom.work