Skip to content

Instantly share code, notes, and snippets.

View khibino's full-sized avatar

日比野 啓 (Kei Hibino) khibino

View GitHub Profile

有限体の性質

p を素数としたとき位数が pⁿ の有限体は同型を除いて一意. (Moore, E. H. (1896), "A doubly-infinite system of simple groups" section 3)

ここから位数が 2ⁿ の有限体 GF(2ⁿ) は一意.

@khibino
khibino / Monoid.agda
Created October 18, 2023 10:34
Monoid Sum
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
record Monoid (m : Set) : Set where
infixl 6 _⊕_
field
_⊕_ : m → m → m
associativity : ∀{a b c} → ((a ⊕ b) ⊕ c) ≡ (a ⊕ (b ⊕ c))
@khibino
khibino / YonedaHO.agda
Last active February 18, 2023 16:11
Yoneda Lemma Proof under Higher-Order types
module YonedaHO where
open import Agda.Primitive using (Level; lsuc; _⊔_)
open import Level using (lift)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; cong; cong-app)
open import Data.Product using (_×_; ∃; _,_; proj₂)
{- apply _≡_ for objects and morphisms for Locally Small Categories -}
{- morphism type definition -}
@khibino
khibino / Session10.agda
Last active February 27, 2023 05:41
Conceptual Mathematics, Session 10, exercises
{- Conceptual Mathematics, Session 10, exercises -}
module Session10 where
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; _≢_)
open import Data.Product using (∃; _,_; _×_)
open import Relation.Nullary using (¬_)
-- contraposition : ∀ {l} -> ∀ {A B : Set l} -> (A -> B) -> ¬ B -> ¬ A
-- contraposition f nb a = nb (f a)
@khibino
khibino / div.agda
Last active November 16, 2022 08:25
open import Agda.Builtin.Equality using (_≡_; refl)
open import Relation.Binary.PropositionalEquality.Core using (sym; trans; _≢_)
-- open import Data.Nat.Base
open import Data.Nat.Base
using (ℕ; zero; suc; _+_; _*_; s≤s; z≤n; _≤_; _<_; _>_;
Ordering; less; equal; greater; compare)
open import Data.Nat.Properties using (+-identityʳ; +-assoc; ≤-trans; m≤m+n; m≢1+m+n; *-cancelˡ-≡)
open import Data.Empty using (⊥)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; _,_)
{-# LANGUAGE DataKinds, KindSignatures, MultiParamTypeClasses,
FunctionalDependencies, FlexibleInstances, FlexibleContexts,
OverloadedLabels, ScopedTypeVariables #-}
import GHC.OverloadedLabels (IsLabel(..))
import GHC.TypeLits (Symbol)
data Label (l :: Symbol) = Put
class Belongs a l b | l b -> a where
-- printf like function, formatting package method
newtype Format r a = Format ((ShowS -> r) -> a)
string :: Format r (String -> r)
string = Format $ \k s -> k (s ++)
int :: Format r (Int -> r)
int = Format $ \k i -> k (show i ++)
open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
----------
-- List の定義
infixr 50 _∷_
data List (A : Set) : Set where
[] : List A
open import Agda.Primitive using (lsuc)
open import Data.Bool using (Bool)
Fix : ∀{l} -> (Set l → Set l) → Set (lsuc l)
Fix f = ∀ k → (f k → k) → k
T : ∀{l} → Set l → Set l
T a = (a → Bool) → Bool
X : Set1
Theorem plus_0_r : forall n:nat, n + 0 = n.
Proof.
intros n. induction n as [| n'].
(* Case "n = 0". *) + reflexivity.
(* Case "n = S n'". *) + simpl. rewrite -> IHn'. reflexivity. Qed.
(** 練習問題: ★★★★, recommended (binary) *)
(* (a) *)
Inductive bin : Type :=