khibino

---

有限体の性質

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

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

khibino

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

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

{- 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

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 (_×_; _,_)

khibino

{-# 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

khibino

-- 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 ++)

khibino

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

khibino

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

khibino

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 :=