text:
module btls-certs where

open import Data.Word8 using (Word8) renaming (primWord8fromNat to to𝕎)
open import Data.ByteString using (ByteString; Strict; Lazy; pack)
open import Data.ByteString.Primitive using (∣List∣≡∣Strict∣)
open import Data.ByteVec using (ByteVec)
open import Data.Nat using (ℕ; zero; suc; _<_; z≤n; s≤s; _≤?_; _∸_)
open import Data.Nat.DivMod using (_divMod_; result)
open import Data.Fin using (Fin; toℕ)
open import Data.Vec using (Vec; toList; tabulate)
open import Data.List using (List; []; _∷_; length; _++_; take)
open import Data.Product using (Σ; _,_; proj₁)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
import Data.ByteString.IO as BSIO
open import IO
open import Function using (_∘_)

open import ASN1.Util using (base256)
import ASN1.BER as BER
import ASN1.X509

open import Bee2.Crypto.Belt using (beltHash)
open import Bee2.Crypto.Bign using (Pri; Pub; Sig; bignCalcPubkey; bignSign2)

b : ℕ → List Word8
b n = toList (tabulate {n} (to𝕎 ∘ toℕ))

b256 = b 256

x : (len : ℕ) → ℕ → Σ (List Word8) (λ l → len ≡ length l)
x zero n = [] , refl
x (suc len) n with n divMod 256
... | result q r _ with x len q
... | ns , refl = (to𝕎 (toℕ r) ∷ ns) , refl

mkPri : ℕ → Pri
mkPri n with x 32 n
... | (ns , prf) = (pack ns) , sym (trans (∣List∣≡∣Strict∣ ns (p prf 32<2³¹)) (sym prf)) where
  p : ∀ {u v k} → (u≡v : u ≡ v) → u < k → v < k
  p refl u<k = u<k
  32<2³¹ : 32 < _
  32<2³¹ =
    s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (
    s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (
    s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (
    s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (
    s≤s z≤n))))))))))))))))))))))))))))))))

ca-pri : Pri
ca-pri = mkPri 17

ca-pub : Pub
ca-pub = bignCalcPubkey ca-pri

sign : Pri → ByteString Strict → ByteString Strict
sign pri = proj₁ ∘ bignSign2 pri ∘ beltHash

ca-cert : ByteString Lazy
ca-cert = BER.encode′ cert where
  open ASN1.X509.mkCert "issuer" "subject" "20170101000000Z" "20190101000000Z" (proj₁ ca-pub) (sign ca-pri)

main = run (BSIO.writeBinaryFile "ca.pkc" ca-cert)


text:
module Functor where

open import Category as Cat

record Functor (ℂ ⅅ : Cat) : Set1 where
  field
    F          : Cat.Obj ℂ -> Cat.Obj ⅅ
    map        : {A B : Cat.Obj ℂ} -> Cat._─→_ ℂ A B -> Cat._─→_ ⅅ (F A) (F B)
    mapEq      : {A B : Cat.Obj ℂ}{f g : Cat._─→_ ℂ A B} -> Category._==_ ℂ f g ->
                 Category._==_ ⅅ (map f) (map g)
    mapId      : {A : Cat.Obj ℂ} -> Category._==_ ⅅ (map (Cat.id ℂ {A})) (Cat.id ⅅ)
    mapCompose : {A B C : Cat.Obj ℂ}{f : Cat._─→_ ℂ B C}{g : Cat._─→_ ℂ A B} ->
                 Category._==_ ⅅ (map (Cat._∘_ ℂ f g)) (Cat._∘_ ⅅ (map f) (map g))

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2015-07-22

-- {-# OPTIONS -v tc.term:20 -v tc.meta.assign:10 -v tc.conv.coerce:10 #-}

open import Common.Size

data Nat (i : Size) : Set where
  suc  : (j : Size< i) → Nat j → Nat i

min : ∀ i → Nat i → Nat i → Nat i
min i (suc j n) (suc k m) = suc i' (min i' n m)
  where i' = _

-- Size consistency check should not be circumvented
-- by putting the meta in a definition.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import FRP.JS.Nat using ( ℕ )
open import FRP.JS.String using ( String )

module FRP.JS.Geolocation.Angle where

postulate
  Angle : Set
  _° : ℕ → Angle
  _′ : ℕ → Angle
  _″ : ℕ → Angle
  _+_ : Angle → Angle → Angle
  toString : Angle → String

{-# COMPILED_JS _° function(x) { return ((x + 180) % 360) - 180; } #-}
{-# COMPILED_JS _′ function(x) { return (((x / 60) + 180) % 360) - 180; } #-}
{-# COMPILED_JS _″ function(x) { return (((x / 3600) + 180) % 360) - 180; } #-}
{-# COMPILED_JS _+_ function(x) { return function (y) { return x + y; }; } #-}
{-# COMPILED_JS toString function(x) { return x.toString(); } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- Andreas, 2018-11-03, issue #3361
--
-- Empty variable blocks should trigger warning rather than parse error.

variable

-- Expected warning:
-- Empty variable block.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Booleans
------------------------------------------------------------------------

module Data.Bool where

open import Function
open import Data.Unit using (⊤)
open import Data.Empty
open import Level
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)

infixr 6 _∧_
infixr 5 _∨_ _xor_
infix  0 if_then_else_

------------------------------------------------------------------------
-- The boolean type

data Bool : Set where
  true  : Bool
  false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

{-# COMPILED_DATA Bool Bool True False #-}

------------------------------------------------------------------------
-- Some operations

not : Bool → Bool
not true  = false
not false = true

-- A function mapping true to an inhabited type and false to an empty
-- type.

T : Bool → Set
T true  = ⊤
T false = ⊥

if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
if true  then t else f = t
if false then t else f = f

_∧_ : Bool → Bool → Bool
true  ∧ b = b
false ∧ b = false

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

_xor_ : Bool → Bool → Bool
true  xor b = not b
false xor b = b

------------------------------------------------------------------------
-- Queries

_≟_ : Decidable {A = Bool} _≡_
true  ≟ true  = yes refl
false ≟ false = yes refl
true  ≟ false = no λ()
false ≟ true  = no λ()

------------------------------------------------------------------------
-- Some properties

decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_


text:
{-# OPTIONS --safe #-}

module Definition.Typed.Consequences.Inversion where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties

open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Inversion of Universes
inversion-U : ∀ {Γ C rU lU r} → Γ ⊢ Univ rU lU ∷ C ^ r → Γ ⊢ C ≡ U ¹ ^ [ ! , next ¹ ] × r PE.≡ [ ! , next ¹ ] × lU PE.≡ ⁰
inversion-U (univ 0<1 x) = refl (Ugenⱼ x) , PE.refl , PE.refl
inversion-U (conv x x₁) with inversion-U x
... | [C≡U] , PE.refl , PE.refl  = trans (sym x₁) [C≡U] , PE.refl , PE.refl

-- Inversion of natural number type.
inversion-ℕ : ∀ {Γ C r} → Γ ⊢ ℕ ∷ C ^ r → Γ ⊢ C ≡ U ⁰ ^ r × r PE.≡ [ ! , next ⁰ ]
inversion-ℕ (ℕⱼ x) = refl (Ugenⱼ x) , PE.refl
inversion-ℕ (conv x x₁) with inversion-ℕ x
... | [C≡U] , PE.refl = trans (sym x₁) [C≡U] , PE.refl

-- Inversion of Π-types.
inversion-Π : ∀ {F rF G r Γ C lF lG lΠ}
            → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ  ∷ C ^ r
            → ∃ λ rG
            → lF ≤ lΠ
              × lG ≤ lΠ
              × Γ ⊢ F ∷ Univ rF lF ^ [ ! , next lF ]
              × Γ ∙ F ^ [ rF , ι lF ] ⊢ G ∷ Univ rG lG ^ [ ! , next lG ]
              × Γ ⊢ C ≡ Univ rG lΠ ^ [ ! , next lΠ ]
              × r PE.≡ [ ! , next lΠ ]
inversion-Π (Πⱼ_▹_▹_▹_ {rF = rF} {r = rG} l< l<' x x₁) = rG , l< , l<' , x , x₁ , refl (Ugenⱼ (wfTerm x)) , PE.refl
inversion-Π (conv x x₁) = let rG , l< , l<' , a , b , c , r≡! = inversion-Π x
                          in rG , l< , l<' , a , b
                            , trans (sym (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ rx) r≡! x₁)) c
                            , r≡!

-- Inversion of ∃-types.
inversion-∃ : ∀ {F G Γ C  r}
            → Γ ⊢ ∃ F ▹ G ∷ C ^ r
            → ∃ λ l∃
              → Γ ⊢ F ∷ Univ % l∃ ^ [ ! , next l∃ ]
              × Γ ∙ F ^ [ % , ι l∃ ] ⊢ G ∷ Univ % l∃ ^ [ ! , next l∃ ]
              × Γ ⊢ C ≡ Univ % l∃ ^ [ ! , next l∃ ]
              × r PE.≡ [ ! , next l∃ ]
inversion-∃ (∃ⱼ_▹_ {l = l∃} x x₁) = l∃ , x , x₁ , refl (Ugenⱼ (wfTerm x)) , PE.refl
inversion-∃ (conv x x₁) = let l∃ , a , b , c , r≡! = inversion-∃ x
                          in l∃ , a , b , trans (sym (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ rx) r≡! x₁)) c , r≡!

inversion-Empty : ∀ {Γ C r l} → Γ ⊢ Empty l ∷ C ^ r → Γ ⊢ C ≡ SProp l ^ r × r PE.≡ [ ! , next l ]
inversion-Empty (Emptyⱼ x) = refl (Ugenⱼ x) , PE.refl
inversion-Empty (conv x x₁) =
  let C≡SProp , r = inversion-Empty x
  in trans (sym x₁) C≡SProp , r

-- Inversion of zero.
inversion-zero : ∀ {Γ C r} → Γ ⊢ zero ∷ C ^ r → Γ ⊢ C ≡ ℕ ^ [ ! , ι ⁰ ] × r PE.≡ [ ! , ι ⁰ ]
inversion-zero (zeroⱼ x) = univ (refl (ℕⱼ x)) , PE.refl
inversion-zero (conv x x₁) with inversion-zero x
... | [C≡ℕ] , PE.refl = trans (sym x₁) [C≡ℕ] , PE.refl

-- Inversion of successor.
inversion-suc : ∀ {Γ t C r} → Γ ⊢ suc t ∷ C ^ r → Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ] × Γ ⊢ C ≡ ℕ ^ [ ! , ι ⁰ ] × r PE.≡ [ ! , ι ⁰ ]
inversion-suc (sucⱼ x) = x , refl (univ (ℕⱼ (wfTerm x))) , PE.refl
inversion-suc (conv x x₁) with inversion-suc x
... | a , b , PE.refl = a , trans (sym x₁) b , PE.refl

-- Inversion of natural recursion.
inversion-natrec : ∀ {Γ c g n A C rlC lC} → Γ ⊢ natrec lC C c g n ∷ A ^ rlC
  →  ∃ λ rC → (Γ ∙ ℕ ^ [ ! , ι ⁰ ]) ⊢ C ^ [ rC , ι lC ]
  × Γ ⊢ c ∷ C [ zero ] ^ [ rC , ι lC ]
  × Γ ⊢ g ∷ Π ℕ ^ ! ° ⁰ ▹ (C ^ rC ° lC ▹▹ C [ suc (var 0) ]↑ ° lC ° lC) ° lC ° lC ^ [ rC , ι lC ]
  × Γ ⊢ n ∷ ℕ ^ [ ! , ι ⁰ ]
  × Γ ⊢ A ≡ C [ n ] ^ [ rC , ι lC ]
  × rlC PE.≡ [ rC , ι lC ]
inversion-natrec (natrecⱼ x d d₁ n) = _ , x , d , d₁ , n , refl (substType x n) , PE.refl
inversion-natrec (conv d x) = let a' , a , b , c , d , e , e' = inversion-natrec d
                              in  a' , a , b , c , d , trans (sym (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ rx) e' x)) e , e'

inversion-Emptyrec : ∀ {Γ e A C rlC lEmpty lC} → Γ ⊢ Emptyrec lC lEmpty C e ∷ A ^ rlC
  → ∃ λ rC → Γ ⊢ C ^ [ rC , ι lC ]
  × Γ ⊢ e ∷ Empty lEmpty ^ [ % , ι lEmpty ]
  × Γ ⊢ A ≡ C ^ [ rC , ι lC ]
  × rlC PE.≡ [ rC , ι lC ]
inversion-Emptyrec (Emptyrecⱼ [C] [e]) = _ , [C] , [e] , refl [C] , PE.refl
inversion-Emptyrec (conv d x) = let r , a , b , c , e = inversion-Emptyrec d
                                in r , a , b , trans (sym (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ rx) e x)) c , e

-- Inversion of application.
inversion-app :  ∀ {Γ f a A r lΠ} → Γ ⊢ (f ∘ a ^ lΠ) ∷ A ^ r →
  ∃₂ λ F rF → ∃₂ λ lF G → ∃₂ λ lG rG → Γ ⊢ f ∷ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rG , ι lΠ ]
  × Γ ⊢ a ∷ F ^ [ rF , ι lF ]
  × Γ ⊢ A ≡ G [ a ] ^ [ rG , ι lG ]
  × r PE.≡ [ rG , ι lG ]
inversion-app (d ∘ⱼ d₁) = _ , _ , _ , _ , _ , _ , d , d₁ , refl (substTypeΠ (syntacticTerm d) d₁) , PE.refl
inversion-app (conv d x) = let a , b , c , d , e , f , g , h , i , j = inversion-app d
                           in  a , b , c , d , e , f , g , h , trans (sym (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ rx) j x)) i , j

-- Inversion of lambda.
inversion-lam : ∀ {t F A r lΠ Γ} → Γ ⊢ lam F ▹ t ^ lΠ ∷ A ^ r →
  ∃₂ λ rF lF → ∃₂ λ G rG → ∃ λ lG → Γ ⊢ F ^ [ rF , ι lF ]
  × Γ ∙ F ^ [ rF , ι lF ] ⊢ t ∷ G ^ [ rG , ι lG ]
  × Γ ⊢ A ≡ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rG , ι lΠ ]
  × r PE.≡ [ rG , ι lΠ ]
inversion-lam (lamⱼ l< l<' x x₁) = _ , _ , _ , _ , _ , x , x₁ ,
                                   refl (univ (Πⱼ l< ▹ l<' ▹ (un-univ x) ▹ un-univ (syntacticTerm x₁))) , PE.refl
inversion-lam (conv x x₁) = let a , b , c , d , e , f , g , h , i = inversion-lam x
                            in  a , b , c , d , e , f , g , trans (sym (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ rx) i x₁)) h , i

-- Inversion of Id-types.
inversion-Id : ∀ {A t u C r Γ}
            → Γ ⊢ Id A t u ∷ C ^ r
            → ∃ λ l
              → Γ ⊢ A ∷ U l ^ [ ! , next l ]
              × Γ ⊢ t ∷ A ^ [ ! , ι l ]
              × Γ ⊢ u ∷ A ^ [ ! , ι l ]
              × Γ ⊢ C ≡ SProp l ^ [ ! , next l ]
              × r PE.≡ [ ! , next l ]
inversion-Id (Idⱼ {l = l} A t u) = l , A , t , u , refl (Ugenⱼ (wfTerm A)) , PE.refl
inversion-Id (conv x x₁) = let l , a , b , c , d , r≡! = inversion-Id x
                           in l , a , b , c , trans (sym (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ rx) r≡! x₁)) d , r≡!

-- Inversion of cast-types.
inversion-cast : ∀ {A B e t l C r Γ}
            → Γ ⊢ cast l A B e t ∷ C ^ r
            → ∃ λ rA
              → Γ ⊢ A ∷ Univ rA l ^ [ ! , next ⁰ ]
              × Γ ⊢ B ∷ Univ rA l ^ [ ! , next ⁰ ]
              × Γ ⊢ e ∷ Id (Univ rA l) A B ^ [ % , next ⁰ ]
              × Γ ⊢ t ∷ A ^ [ rA , ι ⁰ ]
              × Γ ⊢ C ≡ B ^ [ rA , ι ⁰ ]
              × r PE.≡ [ rA , ι ⁰ ]
              × l PE.≡ ⁰
inversion-cast (castⱼ X X₁ X₂ X₃) = _ , X , X₁ , X₂ , X₃ , refl (univ X₁) , PE.refl , PE.refl
inversion-cast (conv x x₁) = let r , a , b , c , d , e , r≡! , el = inversion-cast x
                             in r , a , b , c , d , trans (sym (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ rx) r≡! x₁)) e , r≡! , el

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --without-K --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Unit {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Introductions.Universe
open import Definition.LogicalRelation.Irrelevance

open import Tools.Unit
open import Tools.Product

-- Validity of the Unit type.
Unitᵛ : ∀ {Γ l} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ l ⟩ Unit / [Γ]
Unitᵛ [Γ] ⊢Δ [σ] = Unitᵣ (idRed:*: (Unitⱼ ⊢Δ)) , λ _ x₂ → id (Unitⱼ ⊢Δ)

-- Validity of the Unit type as a term.
Unitᵗᵛ : ∀ {Γ} ([Γ] : ⊩ᵛ Γ)
    → Γ ⊩ᵛ⟨ ¹ ⟩ Unit ∷ U / [Γ] / Uᵛ [Γ]
Unitᵗᵛ [Γ] ⊢Δ [σ] = let ⊢Unit  = Unitⱼ ⊢Δ
                        [Unit] = Unitᵣ (idRed:*: (Unitⱼ ⊢Δ))
                    in  Uₜ Unit (idRedTerm:*: ⊢Unit) Unitₙ (≅ₜ-Unitrefl ⊢Δ) [Unit]
                    ,   (λ x x₁ → Uₜ₌ Unit Unit (idRedTerm:*: ⊢Unit) (idRedTerm:*: ⊢Unit) Unitₙ Unitₙ
                                      (≅ₜ-Unitrefl ⊢Δ) [Unit] [Unit] (id (Unitⱼ ⊢Δ)))

-- Validity of star.
starᵛ : ∀ {Γ l} ([Γ] : ⊩ᵛ Γ)
      → Γ ⊩ᵛ⟨ l ⟩ star ∷ Unit / [Γ] / Unitᵛ [Γ]
starᵛ [Γ] ⊢Δ [σ] =
  Unitₜ star (idRedTerm:*: (starⱼ ⊢Δ)) starₙ
    , (λ _ x₁ → Unitₜ₌ (starⱼ ⊢Δ) (starⱼ ⊢Δ))

-- Validity of η-unit.
η-unitᵛ : ∀ {Γ l e e'} ([Γ] : ⊩ᵛ Γ)
  ([Unit] : Γ ⊩ᵛ⟨ l ⟩ Unit / [Γ])
  ([e] : Γ ⊩ᵛ⟨ l ⟩ e ∷ Unit / [Γ] / [Unit])
  ([e'] : Γ ⊩ᵛ⟨ l ⟩ e' ∷ Unit / [Γ] / [Unit])
  → Γ ⊩ᵛ⟨ l ⟩ e ≡ e' ∷ Unit / [Γ] / [Unit]
η-unitᵛ {Γ} {l} {e} {e'} [Γ] [Unit] [e] [e'] {Δ} {σ} ⊢Δ [σ] =
  let J = proj₁ ([Unit] ⊢Δ [σ])
      [σe] = proj₁ ([e] ⊢Δ [σ])
      [σe'] = proj₁ ([e'] ⊢Δ [σ])
      UnitJ : Δ ⊩⟨ l ⟩ Unit
      UnitJ = Unitᵣ (idRed:*: (Unitⱼ ⊢Δ))
      [σe] = irrelevanceTerm J UnitJ [σe]
      [σe'] = irrelevanceTerm J UnitJ [σe']
      ⊢σe = escapeTerm UnitJ [σe]
      ⊢σe' = escapeTerm UnitJ [σe']
  in  irrelevanceEqTerm UnitJ J (Unitₜ₌ ⊢σe ⊢σe')


text:
module z03-natural-numbers where

open import bool
open import bool-thms using (𝔹-contra)
open import eq
open import level

-- p 50

data ℕ : Set where
  zero :     ℕ
  suc  : ℕ → ℕ

-- p 51

{-# BUILTIN NATURAL ℕ #-}

-------------------------
_+_ : ℕ → ℕ → ℕ
zero  + n =          n
suc m + n = suc (m + n) -- recursive call on structurally smaller left side 'm' -- termination

-- p 53

-------------------------
0+ : ∀ (x : ℕ)
   → 0 + x ≡ x
0+ _ = refl -- via definitional equality

{- fails because _+_ defined in terms of pattern matching on left arg
+0 : ∀ (x : ℕ)
    → x + 0 ≡ x
+0 _ = refl

-- p 55

solution is for proof to call itself recursively:
-------------------------
-}
+0 : ∀ (x : ℕ)
   → x + 0 ≡ x

-- BASE
+0  zero                = refl -- via definitional equality

-- INDUCTIVE
-- note: name of 'y' variable, if renamed to 'x', is not same as 'x' in signature
+0 (suc y) rewrite +0 y = refl
{-    ^
      |
'x' in sig instantiated to 'suc y'

so trying to prove (the goal) : suc y + 0 ≡ suc y

goal can be simplified by inductive case of def of _+_

so goal definitionally equal to : suc (y + 0) ≡ suc y

       rewrite recursive call proves   y + 0  ≡     y

  type of proof is x + 0 ≡ x
  so Agda with replace occurrences of x + 0 with x

                       leaving  : suc  y      ≡ suc y

-- p 57

PROOF BY INDUCTION: recursive proofs

------------------------------------------------------------------------------
+ ASSOCIATIVITY

When theorem has multiple variables, must decide which one to use for induction.
Generally: var used where a recursive fun will patten match on it.
If several vars are pattern matched, prefer the one that is matched the most.

Since _+_ matches on 1st arg, then do induction here on 1st arg.
Here 'x' is matched twice but 'y' only once -- so use 'x'.
-}

-------------------------
+assoc : ∀ (x y z : ℕ)
       →  x + (y  + z)
       ≡ (x +  y) + z
{-
BASE case
  goal: zero + (y + z) ≡ (zero + y) + z
  via def/eq
-}
+assoc  zero   y z                      = refl

{-
INDUCTIVE case
  goal          : suc (x + (y + z)) ≡ suc ((x + y) + z)
  need proof of :     (x + (y + z)) ≡     ((x + y) + z)
    that is exactly the inductive hypotheses
    so use rewrite to recursively apply the proof
-}
+assoc (suc x) y z rewrite +assoc x y z = refl

------------------------------------------------------------------------------
-- p 60 + COMMUTATIVITY (rewrite with multiple equations)

-------------------------
+suc : ∀ (x y : ℕ) → x + (suc y) ≡ suc (x + y)
+suc  zero   y                  = refl
+suc (suc x) y rewrite +suc x y = refl

-------------------------
+comm : ∀ (x y : ℕ) → x + y ≡ y + x
{-
BASE
 Goal:         : y ≡ (y + zero)
 so rewrite right hand side using +0 proof
 simplifies to : y ≡  y
-}
+comm  zero   y rewrite +0 y = refl
{-
INDUCTIVE
 Goal : suc (x + y) ≡ (y + suc x)
-}
+comm (suc x) y rewrite +suc y x | +comm x y = refl

------------------------------------------------------------------------------
-- p 62 MULTIPLICATION

-------------------------
_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)

-------------------------
-- p 63 - right distributivity of * over +

-- variable counts x : 2; y : 1; z : 0 : so use x

*distribr : ∀ (x y z : ℕ)
          → (x + y) * z ≡ (x * z) + (y * z)

-- BASE
*distribr  zero   y z = refl

{-
INDUCTIVE
Goal:  ((suc x + y) * z)   ≡ ((suc x * z)  + (y * z))
Goal: (z + ((x + y) * z)) ≡ ((z + (x * z)) + (y * z))

*distribr (suc x) y z rewrite *distribr x y z = {!!}
Goal: (z + ((x * z) + (y * z))) ≡ ((z + (x * z)) + (y * z))
      right-associated                left-associated
so reassociate: to prove
A + (B + C) ≡ (A + B) + C
^    ^   ^
|    |   |
z    |   |
   x * z |
       y * z
-}
*distribr (suc x) y z
  rewrite
    *distribr x y z
  = +assoc z (x * z) (y * z)

------------------------------------------------------------------------------
-- p 65 * COMMUTATIVITY

-------------------------
*0 : ∀ (x : ℕ)
   → x * 0 ≡ 0

-- BASE
*0 zero = refl -- def/eq : (zero * 0) ≡ 0
{-
INDUCTIVE
(suc x * 0) ≡ 0
    (x * 0) ≡ 0 -- IH
rewrite
         0  ≡ 0
-}
*0 (suc y) rewrite *0 y = refl

-------------------------

*suc : ∀ (x y : ℕ) → x * (suc y) ≡ x + (x * y)
{-
BASE
         (zero * suc y) ≡ (zero + (zero * y))
def/eq    zero          ≡  zero
-}
*suc zero y = refl
{-
INDUCTIVE
                (suc x *   suc y)   ≡ (suc   x +   (suc x * y))
def/eq    suc  (y + (x *   suc y))  ≡  suc  (x + (y  + (x * y)))
rw *suc   suc  (y + (x  + (x * y))) ≡  suc  (x + (y  + (x * y)))
rw +assoc suc ((y +  x) + (x * y))  ≡  suc  (x + (y  + (x * y)))
rw +assoc suc ((y +  x) + (x * y))  ≡  suc ((x +  y) + (x * y))
rw +comm  suc ((x +  y) + (x * y))  ≡  suc ((x +  y) + (x * y))
-}
*suc (suc x) y
  rewrite
    *suc   x y
  | +assoc y x (x * y)
  | +assoc x y (x * y)
  | +comm  y x = refl

-------------------------

*comm : ∀ (x y : ℕ) → x * y ≡ y * x
{-
BASE
             (zero * y) ≡ (y * zero)
def/eq        zero      ≡ (y * zero)
rs *0         zero      ≡      zero
-}
*comm zero y rewrite *0 y = refl
{-
INDUCTIVE
           (suc x * y)  ≡ (y *  suc x)
def/eq    (y + (x * y)) ≡ (y *  suc x)
rw *suc   (y + (x * y)) ≡ (y + (y * x))
rw *comm  (y + (y * x)) ≡ (y + (y * x))
-}
*comm (suc x) y
  rewrite
    *suc  y x
  | *comm x y = refl

------------------------------------------------------------------------------
-- p 66 * ASSOCIATIVITY

*assoc : ∀ (x y z : ℕ) → x * (y * z) ≡ (x * y) * z
{-
BASE
        (zero * (y * z)) ≡ ((zero * y) * z)
def/eq   zero            ≡   zero
-}
*assoc  zero   y z = refl
{-
INDUCTIVE

                      (suc x *  (y  * z))  ≡        ((suc x * y)  * z)
def/eq        ((y * z) +  (x *  (y  * z))) ≡ ((y      +  (x * y)) * z)
rw *distribr  ((y * z) +  (x *  (y  * z))) ≡ ((y * z) + ((x * y)  * z))
rw *assoc     ((y * z) + ((x *   y) * z))  ≡ ((y * z) + ((x * y)  * z))
-}
*assoc (suc x) y z
  rewrite
    *distribr y (x * y) z
  | *assoc x y z = refl

------------------------------------------------------------------------------
-- p 67 LESS-THEN <

_<_ : ℕ → ℕ → 𝔹
0       <      0  = ff
0       < (suc y) = tt
(suc x) < (suc y) = x < y
(suc x) <      0  = ff

-------------------------
-- < is TRANSITIVE

{-
xx : ∀ {x y z : ℕ}
   → x < y
   → y < z
   → x < z

Above will not type check because _<_ returns 𝔹 VALUE, not a type
Types have type Set in Agda -- 𝔹 is not the same as Set.
Could define _<_ as a relation: ℕ → ℕ → Set.
But then _<_ could not be used computationally.
Expressions with type Set describe code -- they are NOT code themselves
- e.g., cannot pattern-match on expressions of type Set
        cannot compute with them
Transitivity theorem is statement about behavior of the PROGRAM _<_.
-}

-- p 69

-------------------------
<-0 : ∀ (x : ℕ) → x < 0 ≡ ff
<-0      0  = refl --  (zero < 0) ≡ ff; ff ≡ ff
<-0 (suc y) = refl -- (suc y < 0) ≡ ff; ff ≡ ff

-------------------------
<-trans : ∀ {x y z : ℕ}
        → x < y ≡ tt
        → y < z ≡ tt
        → x < z ≡ tt
{-
       p1 : (x < zero) ≡ tt    ; p2 : (zero < z) ≡ tt      = Goal: (x < z) ≡ tt
rw <-0 p1 : ff         ≡ tt    ; p2 : (0    < z) ≡ tt      = Goal: (x < z) ≡ tt
-}
<-trans     {x}     {0}         p1 p2 rewrite <-0 x = 𝔹-contra p1

-- can't be called like this so no proof needed
<-trans     {0} {suc y}     {0} p1 ()

--     p1 : (zero < suc y) ≡ tt ; p2 : (suc y < suc z) ≡ tt = Goal: (zero < suc z) ≡ tt
<-trans     {0} {suc y} {suc z} p1 p2 = refl

-- can't be called like this so no proof needed
<-trans {suc x} {suc y}     {0} p1 ()

--     p1 : (suc x < suc y) ≡ tt; p2 : (suc y < suc z) ≡ tt = Goal: (suc x < suc z) ≡ tt
<-trans {suc x} {suc y} {suc z} p1 p2 = <-trans {x} {y} {z} p1 p2 -- uses IH via recursive call

------------------------------------------------------------------------------
-- p 71 EQUALITY TEST for ℕ
{-
so far, rely on
- def/eq : done automatically during type checking
- ≡      : express, as a TYPE, a proposition that two VALUES are equal

there are other kinds of equality, e,g.,

COMPUTATIONAL EQUALITY : tests VALUE equality
-}

_=ℕ_ : ℕ → ℕ → 𝔹
0     =ℕ     0 = tt
suc x =ℕ suc y = x =ℕ y
_     =ℕ     _ = ff

_≤_  : ℕ → ℕ → 𝔹
x ≤ y = (x < y) || x =ℕ y

-------------------------

=ℕ-refl : ∀ (x : ℕ) → (x =ℕ x) ≡ tt
=ℕ-refl 0 = refl
=ℕ-refl (suc x) = (=ℕ-refl x)

-------------------------

-- SOUNDNESS property: things indicated to be true really are true
=ℕ-to-≡ : ∀ {x y : ℕ} → x =ℕ y ≡ tt → x ≡ y
=ℕ-to-≡     {0}     {0} _ = refl
=ℕ-to-≡ {suc x}     {0} ()
=ℕ-to-≡     {0} {suc y} ()
=ℕ-to-≡ {suc x} {suc y} p
  rewrite
    =ℕ-to-≡ {x} {y} p = refl

-------------------------

=ℕ-from-≡ : ∀ {x y : ℕ}
          → x ≡ y
          → x =ℕ y ≡ tt
=ℕ-from-≡ {x} refl = =ℕ-refl x

------------------------------------------------------------------------------
-- p 73 EXERCISES

-- 1 nat-thms

--------------------------------------------------
-- properties of addition
--------------------------------------------------

+1 : ∀ (x : ℕ) → x + 1 ≡ suc x
+1 zero = refl
+1 (suc n) rewrite +1 n = refl

+perm : ∀ (x y z : ℕ) → x + (y + z) ≡ y + (x + z)
+perm zero y z = refl
+perm (suc x) y z -- (suc  x + (y + z)) ≡ (y + (suc  x + z))
                  --  suc (x + (y + z)) ≡ (y +  suc (x + z))
  rewrite
    +suc y (x + z) -- suc (x + (y + z)) ≡ suc (y + (x + z))
  | +assoc x y z   -- suc ((x + y) + z) ≡ suc (y + (x + z))
  | +comm x y      -- suc ((y + x) + z) ≡ suc (y + (x + z))
  | +assoc y x z   -- suc ((y + x) + z) ≡ suc ((y + x) + z)
  = refl

--------------------------------------------------
-- properties of multiplication
--------------------------------------------------

*1 : ∀ {n : ℕ} → n * 1 ≡ n
*1 {zero} = refl
*1 {suc n}    -- (suc n * 1) ≡ suc n
              -- suc (n * 1) ≡ suc n
  rewrite
    *comm n 1 -- suc (n + 0) ≡ suc n
  | +0 n      -- suc  n      ≡ suc n
  = refl

--------------------------------------------------
-- properties of <, ≤, and =ℕ, iszero
--------------------------------------------------

0-≤ : ∀ (x : ℕ) → 0 ≤ x ≡ tt
0-≤ zero = refl
0-≤ (suc n)      -- (0 ≤ suc n) ≡ tt
  rewrite 0-≤ n  --          tt ≡ tt
  = refl

=ℕ-sym : ∀ (x y : ℕ) → (x =ℕ y) ≡ (y =ℕ x)
=ℕ-sym zero zero  = refl
=ℕ-sym (suc x) zero = refl -- (suc x =ℕ zero) ≡ (zero =ℕ suc x);  ff ≡ ff
=ℕ-sym zero (suc y) = refl -- (zero =ℕ suc y) ≡ (suc y =ℕ zero);  ff ≡ ff
=ℕ-sym (suc x) (suc y) rewrite =ℕ-sym x y = refl

=ℕ-suc : ∀ (x : ℕ) → suc x =ℕ x ≡ ff
=ℕ-suc zero = refl
=ℕ-suc (suc n) rewrite =ℕ-suc n = refl

<-suc : ∀ (n : ℕ) → n < suc n ≡ tt
<-suc zero = refl
<-suc (suc n) rewrite <-suc n = refl

-- TODO: understand
suc-inj : ∀ {n m : ℕ} → suc n ≡ suc m → n ≡ m
suc-inj         {0}  {0} _ = refl
suc-inj {m = suc m} refl   = refl

<=ℕff : ∀ (x : ℕ) → 0 < x ≡ tt → x =ℕ 0 ≡ ff
<=ℕff (suc x) _ = refl

<≤ : ∀ {n m : ℕ} → n < m ≡ tt → n ≤ m ≡ tt
<≤     {0}     {0} _ = refl
<≤ {suc _}     {0} ()
<≤     {0} {suc _} _ = refl
<≤ {suc n} {suc m} p rewrite <≤ {n} {m} p = refl

--------------------------------------------------
-- ordering properties of < and ≤ℕ
--------------------------------------------------

<-irrefl : ∀ (n : ℕ) → n < n ≡ ff
<-irrefl zero = refl
<-irrefl (suc n) rewrite <-irrefl n = refl

<-asym : ∀ {x y : ℕ}
       → x < y ≡ tt
       → y < x ≡ ff
<-asym {0}         {0} _ = refl
<-asym {0}     {suc _} _ = refl
<-asym {suc _}     {0}     ()
<-asym {suc x} {suc y} p = <-asym {x} {y} p

ℕ-trichotomy𝔹 : ∀ (n m : ℕ) → n < m || n =ℕ m || m < n ≡ tt
ℕ-trichotomy𝔹      0       0  = refl
ℕ-trichotomy𝔹      0  (suc m) = refl
ℕ-trichotomy𝔹 (suc n)      0  = refl
ℕ-trichotomy𝔹 (suc n) (suc m) = ℕ-trichotomy𝔹 n m

<≤-trans : ∀ {x y z : ℕ}
         → x < y ≡ tt
         → y ≤ z ≡ tt
         → x < z ≡ tt
<≤-trans     {x}     {0}         p1 _  rewrite <-0 x = 𝔹-contra p1
<≤-trans     {0} {suc y}     {0} _  ()
<≤-trans     {0} {suc y} {suc z} _  _  = refl
<≤-trans {suc x} {suc y}     {0} _  ()
<≤-trans {suc x} {suc y} {suc z} p1 p2 = <≤-trans {x} {y} {z} p1 p2

≤-refl : ∀ (x : ℕ) → x ≤ x ≡ tt
≤-refl zero = refl
≤-refl (suc x) rewrite ≤-refl x = refl

--------------------------------------------------
-- injectivity properties of addition
--------------------------------------------------

+inj1 : ∀ {x y z : ℕ}
      → x + y ≡ x + z
      →     y ≡     z
+inj1 {0} {y} {z} p = p
+inj1 {suc x} {y} {z} p = +inj1 {x} {y} {z} (suc-inj p)

+inj2 : ∀ {x y z : ℕ}
      → x + z ≡ y + z
      → x     ≡ y
+inj2 {x} {y} {z} p        -- p : (x + z) ≡ (y + z); Goal: x ≡ y
  rewrite
    +comm x z              -- p : (z + x) ≡ (y + z); Goal: x ≡ y
  | +comm y z              -- p : (z + x) ≡ (z + y); Goal: x ≡ y
  = +inj1 {z} {x} {y} p    -- NOTE: '+inj1'

------------------------------------------------------------------------------

-- 2

{- TODO
nat.agda

>, >= : defined in terms of < and <=

Prove versions of theorems like <-trans and <+
- modified to use _>_ instead of _<_

for practice writing out formulas in Agda
since the proofs can be written just to invoke the theorems dealing with _<_
-}

_>_ : ℕ → ℕ → 𝔹
a > b = b < a

_≥_ : ℕ → ℕ → 𝔹
a ≥ b = b ≤ a

<-trans2 : ∀ {x y z : ℕ}
         → y > x ≡ tt
         → z > y ≡ tt
         → z > x ≡ tt
<-trans2 {x} {y} {z} = <-trans {x} {y} {z}

------------------------------------------------------------------------------

-- 3a

f : (n : ℕ) → ℕ
f      0  = 1
f (suc x) = (suc x) * (f x)

f-is-factorial : f 5 ≡ 120
f-is-factorial = refl

-- 3b

f' : ℕ → 𝔹
fb : ℕ → 𝔹

-- is-odd
f'      0  = ff
f' (suc x) = fb x

-- is-even
fb      0  = tt
fb (suc x) = f' x

f'-is-odd : f' (suc 0) ≡ tt
f'-is-odd = refl

fb-is-even : fb (suc (suc 0)) ≡ tt
fb-is-even = refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{- Denotational semantics of the contexts in the category of temporal types. -}
module Semantics.Context where

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.Comonad
open import CategoryTheory.NatTrans
open import TemporalOps.Box
open import TemporalOps.Diamond
open import Syntax.Context
open import Semantics.Types

open import Data.Product renaming (_,_ to _,,_)
open import Relation.Binary.PropositionalEquality

open Comonad W-□
private module F-□ = Functor F-□

-- | Denotation of judgements and contexts

-- Denotation of judgements
⟦_⟧ⱼ : Judgement -> τ
⟦ A now ⟧ⱼ = ⟦ A ⟧ₜ
⟦ A always ⟧ⱼ = □ ⟦ A ⟧ₜ
infix 50 ⟦_⟧ⱼ

-- Denotation of contexts as a finite product of temporal types.
⟦_⟧ₓ : Context -> τ
⟦ ∙ ⟧ₓ = ⊤
⟦ Γ , A ⟧ₓ = ⟦ Γ ⟧ₓ ⊗ ⟦ A ⟧ⱼ
infix 50 ⟦_⟧ₓ

-- Denotation of context to denotation of stabilised context
-- Standard morphism arising from Γ ˢ ⊆ Γ
⟦_ˢ⟧ : ∀ Γ -> ⟦ Γ ⟧ₓ ⇴ ⟦ Γ ˢ ⟧ₓ
⟦ ∙            ˢ⟧ = !
⟦ Γ , A now    ˢ⟧ = ⟦ Γ ˢ⟧ ∘ π₁
⟦ Γ , A always ˢ⟧ = ⟦ Γ ˢ⟧ * id

-- Denotation of context to stable denotation of stabilised context
-- Uses the Cartesian functor property of the □ comonad
⟦_ˢ⟧□ : ∀ Γ -> ⟦ Γ ⟧ₓ ⇴ □ ⟦ Γ ˢ ⟧ₓ
⟦ ∙            ˢ⟧□ = u
⟦ Γ , A now    ˢ⟧□ = ⟦ Γ ˢ⟧□ ∘ π₁
⟦ Γ , A always ˢ⟧□ = m (⟦ Γ ˢ ⟧ₓ) (□ ⟦ A ⟧ₜ) ∘ (⟦ Γ ˢ⟧□ * δ.at ⟦ A ⟧ₜ)

-- The normal stabilisation transformation factors through
-- the comonadic one via ε
⟦ˢ⟧-factor : ∀ Γ -> ⟦ Γ ˢ⟧ ≈ ε.at ⟦ Γ ˢ ⟧ₓ ∘ ⟦ Γ ˢ⟧□
⟦ˢ⟧-factor ∙ = refl
⟦ˢ⟧-factor (Γ , A now) {n} {x ,, y} = ⟦ˢ⟧-factor Γ
⟦ˢ⟧-factor (Γ , A always) {n} {x ,, y} rewrite ⟦ˢ⟧-factor Γ {n} {x} = refl

-- Applying ⟦ˢ⟧□ twice can be replaced with one ⟦ˢ⟧□ and duplication
⟦ˢ⟧□-twice : ∀ Δ -> F-□.fmap ⟦ Δ ˢ ˢ⟧□ ∘ ⟦ Δ ˢ⟧□ ≈ δ.at ⟦ Δ ˢ ˢ ⟧ₓ ∘ ⟦ Δ ˢ ˢ⟧□ ∘ ⟦ Δ ˢ⟧
⟦ˢ⟧□-twice ∙ = refl
⟦ˢ⟧□-twice (Δ , A now) = ⟦ˢ⟧□-twice Δ
⟦ˢ⟧□-twice (Δ , A always) {n} {⟦Δ⟧ ,, □⟦A⟧} = ext λ k → ext λ l → cong (_,, □⟦A⟧) (lemma k l)
    where lemma : ∀ k l -> ⟦ Δ ˢ ˢ⟧□ k (⟦ Δ ˢ⟧□ n ⟦Δ⟧ k) l
                         ≡ ⟦ Δ ˢ ˢ⟧□ n (⟦ Δ ˢ⟧ n ⟦Δ⟧) l
          lemma k l = □-≡ k l (□-≡ n k (⟦ˢ⟧□-twice Δ {n} {⟦Δ⟧}) k) l

-- Applying ⟦ˢ⟧□ and ⟦ˢ⟧ can be commuted
⟦ˢ⟧-comm : ∀ Δ -> ⟦ Δ ˢ ˢ⟧□ ∘ ⟦ Δ ˢ⟧ ≈ F-□.fmap ⟦ Δ ˢ ˢ⟧ ∘ ⟦ Δ ˢ⟧□
⟦ˢ⟧-comm Δ {n} {⟦Δ⟧} = ext (lemma Δ ⟦Δ⟧)
    where
    lemma : ∀ Δ ⟦Δ⟧ l -> (⟦ Δ ˢ ˢ⟧□ ∘ ⟦ Δ ˢ⟧) n ⟦Δ⟧ l ≡ (F-□.fmap ⟦ Δ ˢ ˢ⟧ ∘ ⟦ Δ ˢ⟧□) n ⟦Δ⟧ l
    lemma ∙ ⟦Δ⟧ l = refl
    lemma (Δ , A now) (⟦Δ⟧ ,, ⟦A⟧) l = lemma Δ ⟦Δ⟧ l
    lemma (Δ , A always) (⟦Δ⟧ ,, □⟦A⟧) l = cong (_,, □⟦A⟧) (lemma Δ ⟦Δ⟧ l)

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Examples where

open import Prelude
open import Star
open import Modal

El : Set -> Rel True
El A _ _ = A

List : Set -> Set
List A = Star (El A) _ _

Nat = List True

zero : Nat
zero = ε

suc : Nat -> Nat
suc n = _ • n

-- Vectors

Vec : Set -> Nat -> Set
Vec A = All (\_ -> A)

infixr 40 _::_
_::_ : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (suc n)
x :: xs = check x • xs

-- Fin

Fin : Nat -> Set
Fin = Any (\_ -> True)

-- Turning a vector to a list

vecToList : {A : Set}{n : Nat} -> Vec A n -> List A
vecToList {A} = map ! uncheck

listToVec : {A : Set}(xs : List A) -> Vec A (length xs)
listToVec  ε       = ε
listToVec (x • xs) = x :: listToVec xs

-- span

test : Vec Nat (suc (suc (suc zero)))
test = zero :: suc zero :: suc (suc zero) :: ε


text:
module Control.Monad.Maybe where

open import Prelude
open import Control.Monad.Zero
open import Control.Monad.Transformer

record MaybeT {a} (M : Set a → Set a) (A : Set a) : Set a where
  no-eta-equality
  constructor maybeT
  field runMaybeT : M (Maybe A)

open MaybeT public

module _ {a} {M : Set a → Set a} where

  instance
    FunctorMaybeT : {{_ : Functor M}} → Functor {a = a} (MaybeT M)
    runMaybeT (fmap {{FunctorMaybeT}} f m) = fmap f <$> runMaybeT m

    FunctorZeroMaybeT : {{_ : Monad M}} → FunctorZero {a = a} (MaybeT M)
    runMaybeT (empty {{FunctorZeroMaybeT}}) = return nothing

    AlternativeMaybeT : {{_ : Monad M}} → Alternative {a = a} (MaybeT M)
    runMaybeT (_<|>_ {{AlternativeMaybeT {{monadM}}}} mx my) = do
      just x ← runMaybeT mx
        where nothing → runMaybeT my
      return (just x)

  module _ {{_ : Monad M}} where

    private
      bindMaybeT : ∀ {A B} → MaybeT M A → (A → MaybeT M B) → MaybeT M B
      runMaybeT (bindMaybeT m f) = do
        just x ← runMaybeT m
          where nothing → return nothing
        runMaybeT (f x)

    instance
      ApplicativeMaybeT : Applicative {a = a} (MaybeT M)
      runMaybeT (pure {{ApplicativeMaybeT}} x) = pure (just x)
      _<*>_ {{ApplicativeMaybeT}} = monadAp bindMaybeT

      MonadMaybeT : Monad {a = a} (MaybeT M)
      _>>=_  {{MonadMaybeT}} = bindMaybeT

    liftMaybeT : {A : Set a} → M A → MaybeT M A
    runMaybeT (liftMaybeT m) = just <$> m

instance
  TransformerMaybeT : ∀ {a} → Transformer {a} MaybeT
  lift {{TransformerMaybeT}} = liftMaybeT

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Data.Nat
open import Data.Maybe
open import Data.Char
open import Data.String
open import Data.List hiding (product)
open import Relation.Binary.PropositionalEquality
import      Relation.Binary.PropositionalEquality as PE
  using (_≡_; refl)
import      Relation.Binary.Definitions as BD
import      Relation.Binary             as RB

------------------------------------------------------------------------------

open import Function

open import Optics.All

module Optics.Example where

 infixl 1 _&_
 _&_ = Function._|>_

 -- First we declare a record; which must be EXACTLY
 -- like the record 'Person' below.
 -- that is; must contain a constructor and
 -- a number of /simple/ fields (of type Set; no proofs please!)
 record Person : Set where
   constructor person
   field
     pName : String
     pAge  : ℕ

 -- Then, we do some template agda:
 -- Yes,I know it looks weird; but it says:
 -- Put 'pName' and 'pAge' into scope as
 -- new identifiers; and run the metacomputation mkLens
 -- passing this newly created identifiers; the mkLens
 -- will then bind these identifiers to their respective
 -- generated lenses for the record Person
 --
 -- IMPORTANT: Note how I did NOT /open Person/; otherwise, we'd
 -- have to give different names to the lenses.
 --
 -- IMPORTANT: the list of names passed to unquoteDecl must come
 -- in the same order as the fields of Person.
 unquoteDecl pName pAge = mkLens (quote Person) (pName ∷ pAge ∷ [])

 -- Ok; lets do more recors for fun
 record Store : Set where
   constructor store
   field
     sId      : ℕ
     sManager : Person
 unquoteDecl sId sManager = mkLens (quote Store) (sId ∷ sManager ∷ [])

 record Product : Set where
   constructor product
   field
     pId    : ℕ
     pTag   : String
     pStore : Store

 unquoteDecl pId pTag pStore = mkLens (quote Product)
   (pId ∷ pTag ∷ pStore ∷ [])

 -- Let's now do a simple example:

 mary : Person
 mary = person "Mary" 41

 compilers-from-mary : Store
 compilers-from-mary = store 0 mary

 ghc : Product
 ghc = product 13 "v8.0.0" compilers-from-mary

 -- Now say mary turns 42 years old;

 ghc-from-older-mary : Product
 ghc-from-older-mary = ghc & pStore ∙ sManager ∙ pAge ∙~ 42

 same-ghc-from-mary : Product
 same-ghc-from-mary = ghc & pStore ∙ sManager ∙ pAge %~ suc

 all-is-fine : ghc-from-older-mary ≡ same-ghc-from-mary
 all-is-fine = refl

 mary's-age-was-updated : ghc-from-older-mary ^∙ pStore ∙ sManager ∙ pAge ≡ 42
 mary's-age-was-updated = refl


text:
{-# OPTIONS --without-K --safe #-}

module Categories.Category.Equivalence where

-- Strong equivalence of categories.  Same as ordinary equivalence in Cat.
-- May not include everything we'd like to think of as equivalences, namely
-- the full, faithful functors that are essentially surjective on objects.

open import Level
open import Relation.Binary using (IsEquivalence; Setoid)

open import Categories.Category.Core using (Category)
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃
  using (NaturalIsomorphism ; unitorˡ; unitorʳ; associator; _ⓘᵥ_; _ⓘˡ_; _ⓘʳ_)

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

record WeakInverse (F : Functor C D) (G : Functor D C) : Set (levelOfTerm F ⊔ levelOfTerm G) where
  field
    F∘G≈id : NaturalIsomorphism (F ∘F G) idF
    G∘F≈id : NaturalIsomorphism (G ∘F F) idF

  module F∘G≈id = NaturalIsomorphism F∘G≈id
  module G∘F≈id = NaturalIsomorphism G∘F≈id

record StrongEquivalence {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    F            : Functor C D
    G            : Functor D C
    weak-inverse : WeakInverse F G

  open WeakInverse weak-inverse public

refl : StrongEquivalence C C
refl = record
  { F            = idF
  ; G            = idF
  ; weak-inverse = record
    { F∘G≈id = unitorˡ
    ; G∘F≈id = unitorˡ
    }
  }

sym : StrongEquivalence C D → StrongEquivalence D C
sym e = record
  { F            = G
  ; G            = F
  ; weak-inverse = record
    { F∘G≈id     = G∘F≈id
    ; G∘F≈id     = F∘G≈id
    }
  }
  where open StrongEquivalence e

trans : StrongEquivalence C D → StrongEquivalence D E → StrongEquivalence C E
trans {C = C} {D = D} {E = E} e e′ = record
  { F            = e′.F ∘F e.F
  ; G            = e.G ∘F e′.G
  ; weak-inverse = record
    { F∘G≈id = let module S = Setoid (≃.Functor-NI-setoid E E)
               in S.trans (S.trans (associator (e.G ∘F e′.G) e.F e′.F)
                                   (e′.F ⓘˡ (unitorˡ ⓘᵥ (e.F∘G≈id ⓘʳ e′.G) ⓘᵥ ≃.sym (associator e′.G e.G e.F))))
                          e′.F∘G≈id
    ; G∘F≈id = let module S = Setoid (≃.Functor-NI-setoid C C)
               in S.trans (S.trans (associator (e′.F ∘F e.F) e′.G e.G)
                                   (e.G ⓘˡ (unitorˡ ⓘᵥ (e′.G∘F≈id ⓘʳ e.F) ⓘᵥ ≃.sym (associator e.F e′.F e′.G))))
                          e.G∘F≈id
    }
  }
  where module e  = StrongEquivalence e
        module e′ = StrongEquivalence e′

isEquivalence : ∀ {o ℓ e} → IsEquivalence (StrongEquivalence {o} {ℓ} {e})
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

setoid : ∀ o ℓ e → Setoid _ _
setoid o ℓ e = record
  { Carrier       = Category o ℓ e
  ; _≈_           = StrongEquivalence
  ; isEquivalence = isEquivalence
  }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module Numeral.Natural.Oper.Modulo.Proofs where

import Lvl
open import Data
open import Data.Boolean.Stmt
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Modulo.Proofs.Algorithm
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Existence using ([≤]-equivalence)
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Implication
open import Syntax.Transitivity
open import Syntax.Type
open import Type
open import Numeral.Natural.Oper.DivMod.Proofs
-- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- mod₀ and mod

mod₀-mod : ∀{a b} → ((a mod₀ 𝐒(b)) ≡ (a mod 𝐒(b)))
mod₀-mod = [≡]-intro

-- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- mod

open import Numeral.Natural.Inductions
open import Structure.Relator
open import Structure.Relator.Ordering

{-
mod-elim : ∀{ℓ} → (P : {ℕ} → ℕ → Type{ℓ}) → ∀{b} ⦃ _ : IsTrue(positive?(b)) ⦄ → (∀{a} → (a < b) → P{a}(a)) → (∀{a} → (a ≥ b) → P{a −₀ b}((a −₀ b) mod b) → P{a}(a mod b)) → (∀{a} → P{a}(a mod b))
mod-elim P {𝐒 b} base step {a} = Strict.Properties.wellfounded-recursion(_<_) {P = a ↦ P(a mod 𝐒(b))} p a where
  ord : ∀{a b} → (b < a) → (a −₀ 𝐒(b) < a)
  ord {𝐒 a} {b} _ = succ ([−₀]-lesser {a}{b})

  p : (a : ℕ) → ((prev : ℕ) ⦃ _ : prev < a ⦄ → P(prev mod 𝐒(b))) → P(a mod 𝐒(b))
  p a prev with [<][≥]-dichotomy {a}{𝐒 b}
  ... | [∨]-introₗ lt = substitute₁ₗ(P) (mod'-lesser-dividend ([≤]-without-[𝐒] lt)) (base{a} lt)
  ... | [∨]-introᵣ ge = step ge (prev(a −₀ 𝐒(b)) ⦃ ord{a}{b} ge ⦄)
-}

-- 0 is 0 in every modulus.
mod-of-0 : ∀{b} → (0 mod 𝐒(b) ≡ 0)
mod-of-0 = [≡]-intro

-- There is only one value when the modulus is 1, and that is 0.
mod-of-1 : ∀{a} → (a mod 1 ≡ 0)
mod-of-1 {a} = mod'-zero-all-except-dividend {a}

-- When the dividend is lesser than the modulus, the result is unchanged.
mod-lesser-than-modulus : ∀{a b} → ⦃ _ : a ≤ b ⦄ → (a mod 𝐒(b) ≡ a)
mod-lesser-than-modulus {a} {b} ⦃ ab ⦄ = mod'-lesser-dividend ab

-- The value of the modulo operation is always strictly less than the modulus.
-- This is because the value loops around at the end by definition.
mod-maxᵣ : ∀{a b} → ⦃ _ : IsTrue(positive?(b)) ⦄ → (a mod b < b)
mod-maxᵣ {𝟎}   {𝐒 𝟎}    = [≤]-with-[𝐒]
mod-maxᵣ {𝟎}   {𝐒(𝐒 b)} = [≤]-with-[𝐒]
mod-maxᵣ {𝐒 a} {𝐒 𝟎}    = mod-maxᵣ {a}{𝐒 𝟎}
mod-maxᵣ {𝐒 a} {𝐒(𝐒 b)} = [≤]-with-[𝐒] ⦃ mod'-maxᵣ {1}{b}{a}{b} ⦃ reflexivity(_≤_)⦄ ⦄

-- When proving properties about the modulo operation, only proofs about numbers lesser than the modulus is necessary.
mod-intro : ∀{ℓ} → (P : {ℕ} → ℕ → Type{ℓ}) → ∀{b} ⦃ _ : IsTrue(positive?(b)) ⦄ → (∀{a n} → (a < b) → P{a + (n ⋅ b)}(a)) → (∀{a} → P{a}(a mod b))
mod-intro P {𝐒 b} proof {a} with [<][≥]-dichotomy {a}{𝐒 b}
... | [∨]-introₗ lt = substitute₂(\x y → P{x}(y))
  (reflexivity(_≡_))
  (symmetry(_≡_) (mod-lesser-than-modulus ⦃ [≤]-without-[𝐒] lt ⦄))
  (proof{a}{0} lt)
... | [∨]-introᵣ ge = substitute₂(\x y → P{x}(y))
  ([↔]-to-[→] ([−₀][+]-nullify2ᵣ {(a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b)}{a}) (subtransitivityᵣ(_≤_)(_≡_) ([≤]-of-[+]ₗ {(a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b)}{a mod 𝐒(b)}) ([⌊/⌋][mod]-is-division-with-remainder {a}{b})))
  (symmetry(_≡_) ([⌊/⌋][⋅]-inverseOperatorᵣ-error {a}{b}))
  (proof{a −₀ ((a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b))}{a ⌊/⌋ 𝐒(b)} (subtransitivityₗ(_<_)(_≡_) (symmetry(_≡_) ([⌊/⌋][⋅]-inverseOperatorᵣ-error {a}{b})) (mod-maxᵣ{a}{𝐒 b})))

mod-intro₂ : ∀{ℓ} → (P : {ℕ} → {ℕ} → ℕ → ℕ → Type{ℓ}) → ∀{m} ⦃ _ : IsTrue(positive?(m)) ⦄ → (∀{a b n₁ n₂} → (a < m) → (b < m) → P{a + (n₁ ⋅ m)}{b + (n₂ ⋅ m)}(a)(b)) → (∀{a b} → P{a}{b}(a mod m)(b mod m))
mod-intro₂ P {m} p {a}{b} = mod-intro(\{a} am → P{a}{b}(am)(b mod m)) {m} (\{a}{n₁} an₁ → mod-intro(\{b} bm → P{a + (n₁ ⋅ m)}{b}(a)(bm)) {m} (\{b}{n₂} bn₂ → p {a}{b}{n₁}{n₂} an₁ bn₂) {b}) {a}

-- The modulus is the loop point of the dividend.
mod-of-modulus : ∀{b} → (𝐒(b) mod 𝐒(b) ≡ 𝟎)
mod-of-modulus {b} = mod'-equal-dividend {𝟎}{b}{b}

-- Adding the modulus to the dividend does not alter the result.
mod-of-modulus-add : ∀{a b} → ((𝐒(b) + a) mod 𝐒(b) ≡ a mod 𝐒(b))
mod-of-modulus-add {a}{b} = mod'-sumₗ-modulo {𝟎}{b}{a}{b}

mod-of-modulus-addᵣ : ∀{a b} → ((a + 𝐒(b)) mod 𝐒(b) ≡ a mod 𝐒(b))
mod-of-modulus-addᵣ {a}{b} = mod'-sumᵣ-modulo {𝟎}{b}{a}{b}

-- A multiple of the modulus in the dividend is always 0.
mod-of-modulus-multiple : ∀{a b} → ((𝐒(b) ⋅ a) mod 𝐒(b) ≡ 𝟎)
mod-of-modulus-multiple {𝟎}   {b} = [≡]-intro
mod-of-modulus-multiple {𝐒 a} {b} = mod-of-modulus-add {𝐒(b) ⋅ a}{b} 🝖 mod-of-modulus-multiple {a} {b}

mod-of-modulus-sum-multiple : ∀{a b c} ⦃ _ : IsTrue(positive?(b)) ⦄ → ((a + (b ⋅ c)) mod b ≡ a mod b)
mod-of-modulus-sum-multiple {a} {𝐒 b} {𝟎} = [≡]-intro
mod-of-modulus-sum-multiple {a} {𝐒 b} {𝐒 c} =
  (a + (𝐒(b) ⋅ 𝐒(c))) mod 𝐒(b)       🝖[ _≡_ ]-[]
  (a + (𝐒(b) + (𝐒(b) ⋅ c))) mod 𝐒(b) 🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(b)) (associativity(_+_) {a}{𝐒(b)}{𝐒(b) ⋅ c}) ]-sym
  ((a + 𝐒(b)) + (𝐒(b) ⋅ c)) mod 𝐒(b) 🝖[ _≡_ ]-[ mod-of-modulus-sum-multiple {a + 𝐒(b)} {𝐒 b} {c} ]
  (a + 𝐒(b)) mod 𝐒(b)                🝖[ _≡_ ]-[ mod-of-modulus-addᵣ {a}{b} ]
  a mod 𝐒(b)                         🝖-end

mod-of-modulus-sum-multiple-commuted : ∀{a b c} ⦃ _ : IsTrue(positive?(b)) ⦄ → ((a + (c ⋅ b)) mod b ≡ a mod b)
mod-of-modulus-sum-multiple-commuted {a}{𝐒 b}{c} = congruence₁(_mod 𝐒(b)) (congruence₂ᵣ(_+_)(a) (commutativity(_⋅_) {c}{𝐒 b})) 🝖 mod-of-modulus-sum-multiple{a}{𝐒 b}{c}

-- When the dividend is greater than the modulus, the modulus can be subtracted from the dividend without altering the result.
mod-greater-than-modulus : ∀{a b} → ⦃ _ : (a > b) ⦄ → (a mod 𝐒(b) ≡ (a −₀ 𝐒(b)) mod 𝐒(b))
mod-greater-than-modulus {a}{b} ⦃ a>b ⦄ =
  symmetry(_≡_) ([≡]-with(_mod 𝐒(b)) ([↔]-to-[→] [−₀][+]-nullify2 a>b))
  🝖 mod-of-modulus-add {a −₀ 𝐒(b)} {b}

mod-cases : ∀{a b} → (a mod 𝐒(b) ≡ a) ∨ (a mod 𝐒(b) ≡ (a −₀ 𝐒(b)) mod 𝐒(b))
mod-cases {a}{b} with [≤][>]-dichotomy {a}{b}
mod-cases {a}{b} | [∨]-introₗ a≤b = [∨]-introₗ (mod-lesser-than-modulus  ⦃ a≤b ⦄)
mod-cases {a}{b} | [∨]-introᵣ b>a = [∨]-introᵣ (mod-greater-than-modulus ⦃ b>a ⦄)

mod-nested : ∀{a b c} → ⦃ b ≤ c ⦄ → ((a mod 𝐒(b)) mod 𝐒(c) ≡ a mod 𝐒(b))
mod-nested {a} {b} {c} ⦃ bc ⦄ = mod-lesser-than-modulus {a mod 𝐒(b)} ⦃ [≤]-without-[𝐒] (mod-maxᵣ {a}) 🝖 bc ⦄

mod-maxₗ : ∀{a b} → ⦃ _ : IsTrue(positive?(b)) ⦄ → (a mod b ≤ a)
mod-maxₗ{a}{𝐒 b} = mod'-maxₗ{0}{b}{a}{b}

-- Alternative proof:
-- • Using [mod][∣ᵣₑₘ]-remainder-equality and that (_∣ᵣₑₘ_) using (r = 0) is equivalent to (_∣_).
-- • A special case of: mod-congruence-[𝄩].
mod-divisibility : ∀{a b} → ⦃ _ : IsTrue(positive?(b)) ⦄ → (a mod b ≡ 𝟎) ↔ (b ∣ a)
mod-divisibility {a}{𝐒(b)} = [↔]-intro l r where
  l : ∀{a b} → (a mod 𝐒(b) ≡ 𝟎) ← (𝐒(b) ∣ a)
  l {.0}           {b} Div𝟎              = [≡]-intro
  l {.(𝐒 (b + a))} {b} (Div𝐒 {x = a} ba) = mod-of-modulus-add {a}{b} 🝖 l ba

  r : ∀{a b} → (a mod 𝐒(b) ≡ 𝟎) → (𝐒(b) ∣ a)
  r{a}{b} = Strict.Properties.wellfounded-recursion(_<_) {P = a ↦ ((a mod 𝐒(b) ≡ 𝟎) → (𝐒(b) ∣ a))} p a where
    p : (a : ℕ) → ((prev : ℕ) ⦃ _ : prev < a ⦄ → (prev mod 𝐒(b) ≡ 𝟎) → (𝐒(b) ∣ prev)) → (a mod 𝐒(b) ≡ 𝟎) → (𝐒(b) ∣ a)
    p a prev ab0 with [≤][>]-dichotomy {a}{b}
    ... | [∨]-introₗ ab rewrite symmetry(_≡_) (mod-lesser-than-modulus ⦃ ab ⦄) 🝖 ab0 = Div𝟎
    ... | [∨]-introᵣ ba with [↔]-to-[←] [≤]-equivalence ba
    ... |    [∃]-intro p ⦃ [≡]-intro ⦄ =
      divides-with-[+]
        divides-reflexivity
        (prev p ⦃ succ ([≤]-of-[+]ᵣ {b}{p}) ⦄ (
          p mod 𝐒(b)          🝖-[ symmetry(_≡_) (mod-of-modulus-add {p}{b}) ]
          (𝐒(b) + p) mod 𝐒(b) 🝖-[ ab0 ]
          𝟎                   🝖-end
        ))

mod-of-𝐒 : ∀{a b} → ⦃ pos : IsTrue(positive?(b)) ⦄ → (𝐒(a) mod b ≡ 𝐒(a mod b) mod b)
mod-of-𝐒 {a} {𝐒 b} = mod-intro(\{a} → expr ↦ 𝐒(a) mod 𝐒(b) ≡ 𝐒(expr) mod 𝐒(b)) {𝐒(b)} (\{a}{n} → p{a}{n}) {a} where
  p : ∀{a n} → (a < 𝐒(b)) → (𝐒(a + (n ⋅ 𝐒(b))) mod 𝐒(b)) ≡ (𝐒(a) mod 𝐒(b))
  p {a}{n} ab =
    𝐒(a + (n ⋅ 𝐒(b))) mod 𝐒(b)   🝖[ _≡_ ]-[]
    (𝐒(a) + (n ⋅ 𝐒(b))) mod 𝐒(b) 🝖[ _≡_ ]-[ mod-of-modulus-sum-multiple-commuted {𝐒(a)}{𝐒(b)}{n} ]
    𝐒(a) mod 𝐒(b)                🝖-end

mod-of-[+] : ∀{a b m} → ⦃ pos : IsTrue(positive?(m)) ⦄ → ((a + b) mod m ≡ ((a mod m) + (b mod m)) mod m)
mod-of-[+] {a}{b}{𝐒 m} =
  (a + b) mod 𝐒(m)                                                                           🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (congruence₂(_+_) ([⌊/⌋][mod]-is-division-with-remainder{a}{m}) ([⌊/⌋][mod]-is-division-with-remainder{b}{m})) ]-sym
  ((((a ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)) + (a mod 𝐒(m))) + (((b ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)) + (b mod 𝐒(m)))) mod 𝐒(m) 🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (One.associate-commute4-c {_▫_ = _+_} {a = (a ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)}{a mod 𝐒(m)}{(b ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)}{b mod 𝐒(m)}) ]
  ((((a ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)) + ((b ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m))) + ((a mod 𝐒(m)) + (b mod 𝐒(m)))) mod 𝐒(m) 🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (commutativity(_+_) {((a ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)) + ((b ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m))}{(a mod 𝐒(m)) + (b mod 𝐒(m))}) ]
  (((a mod 𝐒(m)) + (b mod 𝐒(m))) + (((a ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)) + ((b ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)))) mod 𝐒(m) 🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (congruence₂ᵣ(_+_)((a mod 𝐒(m)) + (b mod 𝐒(m))) (distributivityᵣ(_⋅_)(_+_) {a ⌊/⌋ 𝐒(m)}{b ⌊/⌋ 𝐒(m)}{𝐒(m)})) ]-sym
  (((a mod 𝐒(m)) + (b mod 𝐒(m))) + (((a ⌊/⌋ 𝐒(m)) + (b ⌊/⌋ 𝐒(m))) ⋅ 𝐒(m))) mod 𝐒(m)          🝖[ _≡_ ]-[ mod-of-modulus-sum-multiple-commuted{(a mod 𝐒(m)) + (b mod 𝐒(m))}{𝐒(m)}{(a ⌊/⌋ 𝐒(m)) + (b ⌊/⌋ 𝐒(m))} ]
  ((a mod 𝐒(m)) + (b mod 𝐒(m))) mod 𝐒(m)                                                     🝖-end

{-
open import Functional
open import Structure.Function
open import Structure.Function.Domain
{-# TERMINATING #-}
mod-of-𝐒 : ∀{a b} → ⦃ pos : IsTrue(positive?(b)) ⦄ → (𝐒(a) mod b ≡ 𝐒(a mod b)) ∨ (𝐒(a) mod b ≡ 𝟎)
mod-of-𝐒 {𝟎} {𝐒 𝟎}     = [∨]-introᵣ [≡]-intro
mod-of-𝐒 {𝟎} {𝐒 (𝐒 b)} = [∨]-introₗ [≡]-intro
mod-of-𝐒 {a} {𝐒 b} with [<]-trichotomy {a}{b}
... | [∨]-introₗ([∨]-introₗ lt) = [∨]-introₗ $
  𝐒(a) mod 𝐒(b) 🝖[ _≡_ ]-[ mod-lesser-than-modulus ⦃ lt ⦄ ]
  𝐒(a)          🝖[ _≡_ ]-[ congruence₁(𝐒) (mod-lesser-than-modulus ⦃ [≤]-predecessor lt ⦄) ]-sym
  𝐒(a mod 𝐒(b)) 🝖-end
... | [∨]-introₗ([∨]-introᵣ [≡]-intro) = [∨]-introᵣ(mod-of-modulus{b})
... | [∨]-introᵣ gt with mod-of-𝐒 {a −₀ 𝐒(b)}{𝐒 b}
... |   [∨]-introₗ q = [∨]-introₗ ∘ injective(𝐒) $
  𝐒(𝐒(a) mod 𝐒(b))              🝖[ _≡_ ]-[ congruence₁(𝐒) (mod-greater-than-modulus ⦃ [≤]-successor gt ⦄) ]
  𝐒((𝐒(a) −₀ 𝐒(b)) mod 𝐒(b))    🝖[ _≡_ ]-[ congruence₁(𝐒) (congruence₁(_mod 𝐒(b)) ([↔]-to-[→] [−₀][𝐒]ₗ-equality gt)) ]
  𝐒(𝐒(a −₀ 𝐒(b)) mod 𝐒(b))      🝖[ _≡_ ]-[ congruence₁(𝐒) q ]
  𝐒(𝐒((a −₀ 𝐒(b)) mod 𝐒(b)))    🝖[ _≡_ ]-[ congruence₁(𝐒) (congruence₁(𝐒) (mod-greater-than-modulus ⦃ gt ⦄)) ]-sym
  𝐒(𝐒(a mod 𝐒(b)))              🝖-end
... |   [∨]-introᵣ q = [∨]-introᵣ $
  (𝐒(a) mod 𝐒(b))           🝖[ _≡_ ]-[ mod-greater-than-modulus ⦃ [≤]-successor gt ⦄ ]
  ((𝐒(a) −₀ 𝐒(b)) mod 𝐒(b)) 🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(b)) ([↔]-to-[→] [−₀][𝐒]ₗ-equality gt) ]
  (𝐒(a −₀ 𝐒(b)) mod 𝐒(b))   🝖[ _≡_ ]-[ q ]
  0                         🝖-end
-}

{-mod-congruence-with-𝐒 {a}{b}{𝐒 m} p with mod-of-𝐒 {a}{𝐒 m} | mod-of-𝐒 {b}{𝐒 m}
... | [∨]-introₗ pa | [∨]-introₗ pb = pa 🝖 congruence₁(𝐒) p 🝖 symmetry(_≡_) pb
... | [∨]-introₗ pa | [∨]-introᵣ pb = {!pa 🝖 congruence₁(𝐒) p!}
... | [∨]-introᵣ pa | [∨]-introₗ pb = pa 🝖 {!!} 🝖 symmetry(_≡_) pb
... | [∨]-introᵣ pa | [∨]-introᵣ pb = pa 🝖 symmetry(_≡_) pb-}
{-mod-congruence-with-𝐒 {𝟎} {𝟎} {𝐒 m} p = [≡]-intro
mod-congruence-with-𝐒 {𝟎} {𝐒 b} {𝐒 m} p = {!!}
mod-congruence-with-𝐒 {𝐒 a} {𝟎} {𝐒 m} p = {!!}
mod-congruence-with-𝐒 {𝐒 a} {𝐒 b} {𝐒 m} p = {!!}-}
{-mod-congruence-without-𝐒 {𝟎}   {𝟎}   {𝐒 m} p = [≡]-intro
mod-congruence-without-𝐒 {𝟎}   {𝐒 b} {𝐒 m} p = {!!}
mod-congruence-without-𝐒 {𝐒 a} {𝟎}   {𝐒 m} p = {!!}
mod-congruence-without-𝐒 {𝐒 a} {𝐒 b} {𝐒 m} p = {!!}-}

{-
-- TODO: Use Structure.Arithmetic instead of the actual ℕ (without the induction principle). Then ℕ with (𝟎 , 𝐒) fulfills such a structure (hom is id), but also ℕ with (a , 𝐒) for any a (hom is (a +_)). Or maybe ℕ with (𝟎 , (a +_)) (hom is (a ⋅_)), or ℕ with (1 , (a ⋅_)). Though this will not help mod-congruence-linear because addition and modulo for example in this new structure also changes.
record Homomorphism(f : ℕ → ℕ) : Type{Lvl.𝟎} where
  field
    preserves-𝟎 : (f(𝟎) ≡ 𝟎)
    preserves-𝐒 : ∀{n} → (f(𝐒(n)) ≡ 𝐒(f(n)))

  preserves-[+] : ∀{a b} → (f(a + b) ≡ f(a) + f(b))
  preserves-[+] {a} {𝟎} = symmetry(_≡_) (congruence₂ᵣ(_+_)(f(a)) preserves-𝟎)
  preserves-[+] {a} {𝐒 b} = preserves-𝐒 🝖 congruence₁(𝐒) (preserves-[+] {a} {b}) 🝖 congruence₂ᵣ(_+_)(f(a)) (symmetry(_≡_) preserves-𝐒)

  preserves-[⋅]ₗ : ∀{a b} → (f(a ⋅ b) ≡ f(a) ⋅ b)
  preserves-[⋅]ₗ {a} {𝟎} = preserves-𝟎
  preserves-[⋅]ₗ {a} {𝐒 b} = preserves-[+] {a}{a ⋅ b} 🝖 congruence₂ᵣ(_+_)(f(a)) (preserves-[⋅]ₗ {a}{b})

  preserves-[−₀] : ∀{a b} → (f(a −₀ b) ≡ f(a) −₀ f(b))
  preserves-[−₀] {𝟎} {b} = preserves-𝟎 🝖 congruence₂ₗ(_−₀_)(f(b)) (symmetry(_≡_) preserves-𝟎)
  preserves-[−₀] {𝐒 a} {𝟎} = congruence₂ᵣ(_−₀_)(f(𝐒(a))) (symmetry(_≡_) preserves-𝟎)
  preserves-[−₀] {𝐒 a} {𝐒 b} = preserves-[−₀] {a} {b} 🝖 symmetry(_≡_) (congruence₂(_−₀_) (preserves-𝐒{a}) (preserves-𝐒{b}))

  -- TODO: But we also need to prove that floored division is a function without mentioning modulo (otherwise, circle argument). Below is the proof of modulo being a function depending on floored division being a function

open import Syntax.Implication
mod-congruence-linear : ∀{a b m} ⦃ pos : IsTrue(positive?(m)) ⦄ {f : ℕ → ℕ} ⦃ hom-f : Homomorphism(f) ⦄ → (a mod m ≡ b mod m) → (f(a) mod m ≡ f(b) mod m)
mod-congruence-linear {a}{b}{𝐒 m}{f} ⦃ hom-f ⦄ =
  a mod 𝐒(m) ≡ b mod 𝐒(m)                                         ⇒-[ (p ↦ symmetry(_≡_) ([⌊/⌋][⋅]-inverseOperatorᵣ-error{a}{m}) 🝖 p 🝖 [⌊/⌋][⋅]-inverseOperatorᵣ-error{b}{m}) ]
  a −₀ (a ⌊/⌋ 𝐒(m) ⋅ 𝐒(m)) ≡ b −₀ (b ⌊/⌋ 𝐒(m) ⋅ 𝐒(m))             ⇒-[ congruence₁(f) ]
  f(a −₀ (a ⌊/⌋ 𝐒(m) ⋅ 𝐒(m))) ≡ f(b −₀ (b ⌊/⌋ 𝐒(m) ⋅ 𝐒(m)))       ⇒-[ {!!} ]
  f(a) −₀ f(a ⌊/⌋ 𝐒(m) ⋅ 𝐒(m)) ≡ f(b) −₀ f(b ⌊/⌋ 𝐒(m) ⋅ 𝐒(m))     ⇒-[ {!!} ]
  f(a) −₀ (f(a ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)) ≡ f(b) −₀ (f(b ⌊/⌋ 𝐒(m)) ⋅ 𝐒(m)) ⇒-[ {!!} ]
  f(a) −₀ (f(a) ⌊/⌋ 𝐒(m) ⋅ 𝐒(m)) ≡ f(b) −₀ (f(b) ⌊/⌋ 𝐒(m) ⋅ 𝐒(m)) ⇒-[ {!!} ]
  f(a) mod 𝐒(m) ≡ f(b) mod 𝐒(m)                                   ⇒-end
  where
    open Homomorphism(hom-f)
-}

postulate [⋅][mod]-distributivityₗ : ∀{a b c} → (c ⋅ (a mod₀ b) ≡ ((c ⋅ a) mod₀ (c ⋅ b)))
{-[⋅][mod]-distributivityₗ {𝟎}   {𝟎}   {𝟎}   = [≡]-intro
[⋅][mod]-distributivityₗ {𝟎}   {𝟎}   {𝐒 c} = [≡]-intro
[⋅][mod]-distributivityₗ {𝟎}   {𝐒 b} {𝟎}   = [≡]-intro
[⋅][mod]-distributivityₗ {𝟎}   {𝐒 b} {𝐒 c} = [≡]-intro
[⋅][mod]-distributivityₗ {𝐒 a} {𝟎}   {𝟎}   = [≡]-intro
[⋅][mod]-distributivityₗ {𝐒 a} {𝟎}   {𝐒 c} = [≡]-intro
[⋅][mod]-distributivityₗ {𝐒 a} {𝐒 b} {𝟎}   = [≡]-intro
[⋅][mod]-distributivityₗ {𝐒 a} {𝐒 b} {𝐒 c} = ?-}
{- TODO: Above is true. Prove using the division theorem
(((c ⋅ a) / (c ⋅ b)) ⋅ (c ⋅ b)) + ((c ⋅ a) mod₀ (c ⋅ b)) ≡ c ⋅ a //Division theorem on (c ⋅ a)
  (((c ⋅ a) / (c ⋅ b)) ⋅ (c ⋅ b)) + (c ⋅ (a mod₀ b)) ≡
  ((a / b) ⋅ (c ⋅ b)) + (c ⋅ (a mod₀ b)) ≡ //a/b = (c⋅a)/(c⋅b)
  (c ⋅ ((a / b) ⋅ b)) + (c ⋅ (a mod₀ b)) ≡ //Commuting and associating ⋅
  c ⋅ ((a / b) ⋅ b) + (a mod₀ b) ≡ c ⋅ a //...equal to LHS here by distributivity of (_⋅_) over (_+_), and this identity is division theorem on a with congruenced (c ⋅_)
  ((a / b) ⋅ b) + (a mod₀ b) ≡ a-}

{-
mod-equality-diff : ∀{a b m} → (a mod 𝐒(m) ≡ b mod 𝐒(m)) → ((a 𝄩 b) mod 𝐒(m) ≡ 𝟎)
mod-equality-diff {𝟎}   {𝟎}   {m} ab = [≡]-intro
mod-equality-diff {𝟎}   {𝐒 b} {m} ab = symmetry(_≡_) ab
mod-equality-diff {𝐒 a} {𝟎}   {m} ab = ab
mod-equality-diff {𝐒 a} {𝐒 b} {m} ab = mod-equality-diff {a} {b} {m} {!!}
-}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- mod₀

{-
-- mod₀-eq-predecessor : ∀{a b} → ((𝐒(a) mod₀ b) ≡ 𝐒(c)) → ((a mod₀ b) ≡ c)

postulate mod₀-of-𝐒 : ∀{a b} → (𝐒(a) mod₀ b ≡ 𝟎) ∨ (𝐒(a) mod₀ b ≡ 𝐒(a mod₀ b))

-- TODO: Should also be satisfied for b, not just 𝐒(b)
-- mod₀-of-modulus-pre-eq : ∀{a b} → (𝐒(a) mod₀ 𝐒(b) ≡ 𝟎) → (a mod₀ 𝐒(b) ≡ b)
-- mod₀-of-modulus-pre-eq : ∀{a b} → (𝐒(a) mod₀ 𝐒(b) ≡ 𝐒(c)) → (a mod₀ 𝐒(b) ≡ c)

postulate mod₀-[⋅]ₗ-equality : ∀{a b k c} → ((a mod₀ c) ≡ (b mod₀ c)) → (((k ⋅ a) mod₀ c) ≡ ((k ⋅ b) mod₀ c))
postulate mod₀-[⋅]ᵣ-equality : ∀{a b k c} → ((a mod₀ c) ≡ (b mod₀ c)) → (((a ⋅ k) mod₀ c) ≡ ((b ⋅ k) mod₀ c))
postulate mod₀-[⋅]-equality : ∀{a₁ b₁ a₂ b₂ c} → ((a₁ mod₀ c) ≡ (b₁ mod₀ c)) → ((a₂ mod₀ c) ≡ (b₂ mod₀ c)) → (((a₁ ⋅ a₂) mod₀ c) ≡ ((b₁ ⋅ b₂) mod₀ c))

-- postulate mod₀-[^]ᵣ-equality : ∀{a b k c} → ((a mod₀ c) ≡ (b mod₀ c)) → (((a ^ k) mod₀ c) ≡ ((b ^ k) mod₀ c))

-- postulate mod₀-[/]ₗ-equality : ∀{a b k c} → ((a mod₀ c) ≡ (b mod₀ c)) → (k ∣ a) → (k ∣ b) → (((k / a) mod₀ c) ≡ ((k / b) mod₀ c))
-- postulate mod₀-[/]ᵣ-equality : ∀{a b k c} → ((a mod₀ c) ≡ (b mod₀ c)) ∧ (k ∣ a) ∧ (k ∣ b) ← (((a / k) mod₀ c) ≡ ((b / k) mod₀ c))

-- postulate modulo-multiplication : ∀{a₁ a₂ b} → (((a₁ ⋅ a₂) mod₀ b) ≡ (((a₁ mod₀ b) ⋅ (a₂ mod₀ b)) mod₀ b))

-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Category where

open import Level
open import Relation.Binary using (Rel; IsEquivalence; module IsEquivalence; Reflexive; Symmetric; Transitive) renaming (_⇒_ to _⊆_)
open import Function using (flip)

open import Categories.Support.PropositionalEquality
open import Categories.Support.Equivalence
open import Categories.Support.EqReasoning
open import Data.Product

postulate
  .irr : ∀ {a} {A : Set a} → .A → A

record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  eta-equality
  infix  4 _≡_ _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : Rel Obj ℓ
    {_≡_} : ∀ {A B} → Rel (A ⇒ B) e

    {id}  : ∀ {A} → (A ⇒ A)
    {_∘_} : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  field
    .{assoc}     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)
    .{identityˡ} : ∀ {A B} {f : A ⇒ B} → id ∘ f ≡ f
    .{identityʳ} : ∀ {A B} {f : A ⇒ B} → f ∘ id ≡ f
    .{equiv}     : ∀ {A B} → IsEquivalence (_≡_ {A} {B})
    .{∘-resp-≡}  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≡ h → g ≡ i → f ∘ g ≡ h ∘ i

  -- with irrelevant modules this would be:
  -- module .Equiv {A B : Obj} = IsEquivalence (equiv {A} {B})
  module Equiv {A B : Obj} where
    module e = IsEquivalence
    private
      .q : IsEquivalence _≡_
      q = equiv {A} {B}

    .refl : Reflexive _≡_
    refl = e.refl q
    .trans : Transitive _≡_
    trans = e.trans q
    .sym : Symmetric _≡_
    sym = e.sym q
    .reflexive : _≣_ ⊆ _≡_
    reflexive = e.reflexive q

  open Equiv

  domain : ∀ {A B} → (A ⇒ B) → Obj
  domain {A} _ = A

  codomain : ∀ {A B} → (A ⇒ B) → Obj
  codomain {B = B} _ = B

  .∘-resp-≡ˡ : ∀ {A B C} {f h : B ⇒ C} {g : A ⇒ B} → f ≡ h → f ∘ g ≡ h ∘ g
  ∘-resp-≡ˡ pf = ∘-resp-≡ pf refl

  .∘-resp-≡ʳ : ∀ {A B C} {f h : A ⇒ B} {g : B ⇒ C} → f ≡ h → g ∘ f ≡ g ∘ h
  ∘-resp-≡ʳ pf = ∘-resp-≡ refl pf

  hom-setoid : ∀ {A B} → Setoid _ _
  hom-setoid {A} {B} = record
    { Carrier = A ⇒ B
    ; _≈_ = _≡_
    ; isEquivalence = equiv
    }

  module HomReasoning {A B : Obj} where
    open SetoidReasoning (hom-setoid {A} {B}) public

    infixr 4 _⟩∘⟨_
    ._⟩∘⟨_ : ∀ {M} {f h : M ⇒ B} {g i : A ⇒ M} → f ≡ h → g ≡ i → f ∘ g ≡ h ∘ i
    _⟩∘⟨_ = ∘-resp-≡

  op : Category o ℓ e
  op = record
    { Obj = Obj
    ; _⇒_ = flip _⇒_
    ; _≡_ = _≡_
    ; _∘_ = flip _∘_
    ; id = id
    ; assoc = sym assoc
    ; identityˡ = identityʳ
    ; identityʳ = identityˡ
    ; equiv = record
      { refl = refl
      ; sym = sym
      ; trans = trans
      }
    ; ∘-resp-≡ = flip ∘-resp-≡
    }

  CommutativeSquare : ∀ {A B C D} → (f : A ⇒ B) (g : A ⇒ C) (h : B ⇒ D) (i : C ⇒ D) → Set _
  CommutativeSquare f g h i = h ∘ f ≡ i ∘ g

  .id-unique : ∀ {o} {f : o ⇒ o} → (∀ g → g ∘ f ≡ g) → f ≡ id
  id-unique g∘f≡g = trans (sym identityˡ) (g∘f≡g id)

  .id-comm : ∀ {a b} {f : a ⇒ b} → f ∘ id ≡ id ∘ f
  id-comm = trans identityʳ (sym identityˡ)

infix 10  _[_,_] _[_≡_] _[_∘_]

_[_,_] : ∀ {o ℓ e} → (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ
_[_,_] = Category._⇒_

_[_≡_] : ∀ {o ℓ e} → (C : Category o ℓ e) → ∀ {X Y} (f g : C [ X , Y ]) → Set e
_[_≡_] = Category._≡_

_[_∘_] : ∀ {o ℓ e} → (C : Category o ℓ e) → ∀ {X Y Z} (f : C [ Y , Z ]) → (g : C [ X , Y ]) → C [ X , Z ]
_[_∘_] = Category._∘_

-- Should this live in the Category record itself? It doesn't seem terribly useful for most situations
module Heterogeneous {o ℓ e} (C : Category o ℓ e) where
  open Category C
  open Equiv renaming (refl to refl′; sym to sym′; trans to trans′; reflexive to reflexive′)

  infix 4 _∼_

  data _∼_ {A B} (f : A ⇒ B) : ∀ {X Y} → (X ⇒ Y) → Set (ℓ ⊔ e) where
    ≡⇒∼ : {g : A ⇒ B} → .(f ≡ g) → f ∼ g

  refl : ∀ {A B} {f : A ⇒ B} → f ∼ f
  refl = ≡⇒∼ refl′

  sym : ∀ {A B} {f : A ⇒ B} {D E} {g : D ⇒ E} → f ∼ g → g ∼ f
  sym (≡⇒∼ f≡g) = ≡⇒∼ (sym′ f≡g)

  trans : ∀ {A B} {f : A ⇒ B}
             {D E} {g : D ⇒ E}
             {F G} {h : F ⇒ G}
          → f ∼ g → g ∼ h → f ∼ h
  trans (≡⇒∼ f≡g) (≡⇒∼ g≡h) = ≡⇒∼ (trans′ f≡g g≡h)

  reflexive : ∀ {A B} {f g : A ⇒ B} → f ≣ g → f ∼ g
  reflexive f≣g = ≡⇒∼ (reflexive′ f≣g)

  ∘-resp-∼ : ∀ {A B C A′ B′ C′} {f : B ⇒ C} {h : B′ ⇒ C′} {g : A ⇒ B} {i : A′ ⇒ B′} → f ∼ h → g ∼ i → (f ∘ g) ∼ (h ∘ i)
  ∘-resp-∼ (≡⇒∼ f≡h) (≡⇒∼ g≡i) = ≡⇒∼ (∘-resp-≡ f≡h g≡i)

  ∘-resp-∼ˡ : ∀ {A B C C′} {f : B ⇒ C} {h : B ⇒ C′} {g : A ⇒ B} → f ∼ h → (f ∘ g) ∼ (h ∘ g)
  ∘-resp-∼ˡ (≡⇒∼ f≡h) = ≡⇒∼ (∘-resp-≡ˡ f≡h)

  ∘-resp-∼ʳ : ∀ {A A′ B C} {f : A ⇒ B} {h : A′ ⇒ B} {g : B ⇒ C} → f ∼ h → (g ∘ f) ∼ (g ∘ h)
  ∘-resp-∼ʳ (≡⇒∼ f≡h) = ≡⇒∼ (∘-resp-≡ʳ f≡h)

  .∼⇒≡ : ∀ {A B} {f g : A ⇒ B} → f ∼ g → f ≡ g
  ∼⇒≡ (≡⇒∼ f≡g) = irr f≡g

  domain-≣ : ∀ {A A′ B B′} {f : A ⇒ B} {f′ : A′ ⇒ B′} → f ∼ f′ → A ≣ A′
  domain-≣ (≡⇒∼ _) = ≣-refl

  codomain-≣ : ∀ {A A′ B B′} {f : A ⇒ B} {f′ : A′ ⇒ B′} → f ∼ f′ → B ≣ B′
  codomain-≣ (≡⇒∼ _) = ≣-refl

  ∼-cong : ∀ {t : Level} {T : Set t} {dom cod : T → Obj} (f : (x : T) → dom x ⇒ cod x) → ∀ {i j} (eq : i ≣ j) → f i ∼ f j
  ∼-cong f ≣-refl = refl

  -- floating morphisms on ≣
  float₂ : ∀ {A A′ B B′} → A ≣ A′ → B ≣ B′ → A ⇒ B → A′ ⇒ B′
  float₂ = ≣-subst₂ _⇒_

  relaxed : ∀ {A B} {f : A ⇒ B} {X Y} {g : X ⇒ Y} -> (A≣X : A ≣ X) (B≣Y : B ≣ Y) -> float₂ A≣X B≣Y f ≡ g -> f ∼ g
  relaxed ≣-refl ≣-refl f≡g = ≡⇒∼ f≡g

  floatˡ : ∀ {A B B′} → B ≣ B′ → A ⇒ B → A ⇒ B′
  floatˡ {A} = ≣-subst (_⇒_ A)

  floatˡ-resp-trans : ∀ {A B B′ B″} (B≣B′ : B ≣ B′) (B′≣B″ : B′ ≣ B″) (f : A ⇒ B) → floatˡ (≣-trans B≣B′ B′≣B″) f ≣ floatˡ B′≣B″ (floatˡ B≣B′ f)
  floatˡ-resp-trans {A} = ≣-subst-trans (_⇒_ A)

  floatʳ : ∀ {A A′ B} → A ≣ A′ → A ⇒ B → A′ ⇒ B
  floatʳ {B = B} = ≣-subst (λ X → X ⇒ B)

  float₂-breakdown-lr : ∀ {A A′} (A≣A′ : A ≣ A′) {B B′} (B≣B′ : B ≣ B′) (f : A ⇒ B) → float₂ A≣A′ B≣B′ f ≣ floatˡ B≣B′ (floatʳ A≣A′ f)
  float₂-breakdown-lr = ≣-subst₂-breakdown-lr _⇒_

  float₂-breakdown-rl : ∀ {A A′} (A≣A′ : A ≣ A′) {B B′} (B≣B′ : B ≣ B′) (f : A ⇒ B) → float₂ A≣A′ B≣B′ f ≣ floatʳ A≣A′ (floatˡ B≣B′ f)
  float₂-breakdown-rl = ≣-subst₂-breakdown-rl _⇒_

  -- henry ford versions
  .∼⇒≡₂ : ∀ {A A′ B B′} {f : A ⇒ B} {f′ : A′ ⇒ B′} → f ∼ f′ → (A≣A′ : A ≣ A′) (B≣B′ : B ≣ B′) → float₂ A≣A′ B≣B′ f ≡ f′
  ∼⇒≡₂ pf ≣-refl ≣-refl = ∼⇒≡ pf

  .∼⇒≡ˡ : ∀ {A B B′} {f : A ⇒ B} {f′ : A ⇒ B′} → f ∼ f′ → (B≣B′ : B ≣ B′) → floatˡ B≣B′ f ≡ f′
  ∼⇒≡ˡ pf ≣-refl = ∼⇒≡ pf

  .∼⇒≡ʳ : ∀ {A A′ B} {f : A ⇒ B} {f′ : A′ ⇒ B} → f ∼ f′ → (A≣A′ : A ≣ A′) → floatʳ A≣A′ f ≡ f′
  ∼⇒≡ʳ pf ≣-refl = ∼⇒≡ pf

  ≡⇒∼ʳ : ∀ {A A′ B} {f : A ⇒ B} {f′ : A′ ⇒ B} → (A≣A′ : A ≣ A′) → .(floatʳ A≣A′ f ≡ f′) → f ∼ f′
  ≡⇒∼ʳ ≣-refl pf = ≡⇒∼ pf

  float₂-resp-∼ : ∀ {A A′ B B′} (A≣A′ : A ≣ A′) (B≣B′ : B ≣ B′) {f : C [ A , B ]} → f ∼ float₂ A≣A′ B≣B′ f
  float₂-resp-∼ ≣-refl ≣-refl = refl

  floatˡ-resp-∼ : ∀ {A B B′} (B≣B′ : B ≣ B′) {f : C [ A , B ]} → f ∼ floatˡ B≣B′ f
  floatˡ-resp-∼ ≣-refl = refl

  floatʳ-resp-∼ : ∀ {A A′ B} (A≣A′ : A ≣ A′) {f : C [ A , B ]} → f ∼ floatʳ A≣A′ f
  floatʳ-resp-∼ ≣-refl = refl

_[_∼_] : ∀ {o ℓ e} (C : Category o ℓ e) {A B} (f : C [ A , B ]) {X Y} (g : C [ X , Y ]) → Set (ℓ ⊔ e)
C [ f ∼ g ] = Heterogeneous._∼_ C f g

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2016-07-20

-- With clauses should follow the parent clause
-- what copattern style (prefix/postfix) concerns.

record R : Set₂ where
  field f : Set₁

test : R
test .R.f with R    -- post-fix here
R.f test | _ = Set  -- pre-fix there

-- That's not nice, thus, it is an error.


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Definition07d where

infixl 6 _+_
infix  4 _≡_

postulate
  D    : Set
  zero : D
  succ : D → D
  _≡_  : D → D → Set

data N : D → Set where
  nzero : N zero
  nsucc : ∀ {n} → N n → N (succ n)

N-ind : (A : D → Set) →
        A zero →
        (∀ {n} → A n → A (succ n)) →
        ∀ {n} → N n → A n
N-ind A A0 h nzero      = A0
N-ind A A0 h (nsucc Nn) = h (N-ind A A0 h Nn)

postulate
  _+_  : D → D → D
  +-0x : ∀ n → zero + n     ≡ n
  +-Sx : ∀ m n → succ m + n ≡ succ (m + n)
{-# ATP axioms +-0x +-Sx #-}

-- We test the translation of a definition where we need to erase
-- proof terms.
+-rightIdentity : ∀ {n} → N n → n + zero ≡ n
+-rightIdentity Nn = N-ind A A0 is Nn
  where
  A : D → Set
  A i = i + zero ≡ i
  {-# ATP definition A #-}

  postulate A0 : A zero
  {-# ATP prove A0 #-}

  postulate is : ∀ {i} → A i → A (succ i)
  {-# ATP prove is #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
open import Level                                 using (_⊔_)
open import Algebra                               using (module CommutativeSemiring; module DistributiveLattice)
open import Function                              using (id; const; _∘_; _$_)
open import Coinduction                           using (∞; ♯_; ♭)
open import Data.Fin        as Fin                using (Fin; suc; zero)
open import Data.List       as List               using (List; _∷_; []; [_]; _++_; length; concat; foldr; concatMap)
open import Data.Maybe                            using (Maybe; just; nothing)
open import Data.Nat                              using (ℕ; suc; zero; _≤_; z≤n; s≤s)
open import Data.Nat.Properties                   using (commutativeSemiring; distributiveLattice; ≤-decTotalOrder)
open import Data.Product                          using (∃; _×_; _,_)
open import Data.Sum                              using (_⊎_; inj₁; inj₂)
open import Data.Vec        as Vec                using (Vec; _∷_; []; fromList)
open import Relation.Nullary                      using (Dec; yes; no)
open import Relation.Binary                       using (module DecTotalOrder)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; subst)

module ProofSearch
  (RuleName : Set)
  (TermName : Set) (_≟-TermName_ : (x y : TermName) → Dec (x ≡ y))
  (Literal  : Set) (_≟-Literal_  : (x y : Literal)  → Dec (x ≡ y))
  where

  open import Unification TermName _≟-TermName_ Literal _≟-Literal_ public hiding (_++_)

  ----------------------------------------------------------------------------
  -- * define rules and utility functions                                 * --
  ----------------------------------------------------------------------------

  private
    ∃-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (b ⊔ a)
    ∃-syntax = ∃
    syntax ∃-syntax (λ x → B) = ∃[ x ] B

  -- introduce rules
  record Rule (n : ℕ) : Set where
    constructor rule
    field
      name        : RuleName
      conclusion  : Term n
      premises    : List (Term n)

  open Rule using (name; conclusion; premises)

  -- alias for list of rules
  Rules : Set
  Rules = List (∃ Rule)

  -- compute the arity of a rule
  arity : ∀ {n} (r : Rule n) → ℕ
  arity = length ∘ premises

  -- open instances relevant to definitions of difference, inject and raise
  open CommutativeSemiring commutativeSemiring using (_+_; +-comm)
  open DistributiveLattice distributiveLattice using (_∧_; ∧-comm)
  open DecTotalOrder       ≤-decTotalOrder       using (total)

  -- compute the difference between two natural numbers, given an
  -- ordering between them.
  Δ_ : ∀ {m n} → m ≤ n → ℕ
  Δ z≤n {k} = k
  Δ s≤s  p  = Δ p

  -- correctness proof of the difference operator Δ.
  Δ-correct : ∀ {m n} (p : m ≤ n) → n ≡ m + Δ p
  Δ-correct  z≤n    = refl
  Δ-correct (s≤s p) = cong suc (Δ-correct p)

  -- type class for injections in the fashion of Fin.inject+
  record Inject (T : ℕ → Set) : Set where
    field
      inject : ∀ {m} n → T m → T (m + n)

    inject≤ : ∀ {m n} → m ≤ n → T m → T n
    inject≤ {m} {n} p t = subst T (sym (Δ-correct p)) (inject (Δ p) t)

  open Inject {{...}} using (inject; inject≤)

  -- type class for raising in the fashion of Fin.raise
  record Raise (T : ℕ → Set) : Set where
    field
      raise : ∀ {m} n → T m → T (n + m)

    raise≤ : ∀ {m n} → m ≤ n → T m → T n
    raise≤ {m} {n} p t = subst T (sym (trans (Δ-correct p) (+-comm m (Δ p)))) (raise (Δ p) t)

  open Raise {{...}} using (raise; raise≤)

  -- instances for inject/raise for all used data types
  instance
    InjectFin   : Inject Fin
    InjectFin   = record { inject = Fin.inject+ }
    RaiseFin    : Raise  Fin
    RaiseFin    = record { raise  = Fin.raise }
    InjectTerm  : Inject Term
    InjectTerm  = record { inject = λ n → replace (var ∘ inject n) }
    RaiseTerm   : Raise  Term
    RaiseTerm   = record { raise  = λ m → replace (var ∘ raise m) }
    InjectTerms : Inject (List ∘ Term)
    InjectTerms = record { inject = λ n → List.map (inject n) }
    RaiseTerms  : Raise  (List ∘ Term)
    RaiseTerms  = record { raise  = λ m → List.map (raise m) }
    InjectGoals : ∀ {k} → Inject (λ n → Vec (Term n) k)
    InjectGoals = record { inject = λ n → Vec.map (inject n) }
    RaiseGoals  : ∀ {k} → Raise (λ n → Vec (Term n) k)
    RaiseGoals  = record { raise  = λ m → Vec.map (raise m) }
    InjectRule  : Inject Rule
    InjectRule  = record { inject = λ n → λ { (rule nm c p) → rule nm (inject n c) (inject n p) } }
    RaiseRule   : Raise Rule
    RaiseRule   = record { raise  = λ m → λ { (rule nm c p) → rule nm (raise m c) (raise m p) } }

  -- could rephrase inject/raise in terms of allowing modification by
  -- a function ℕ → ℕ, but really... why would I... it makes all the
  -- other instances much, much more obtuse
  injectSubst : ∀ {m n} (δ : ℕ) → Subst m n → Subst (m + δ) (n + δ)
  injectSubst _ nil = nil
  injectSubst δ (snoc s t x) = snoc (injectSubst δ s) (inject δ t) (inject δ x)

  private
    m≤n→m⊔n=n : ∀ {m n} → m ≤ n → m ∧ n ≡ n
    m≤n→m⊔n=n  z≤n    = refl
    m≤n→m⊔n=n (s≤s p) = cong suc (m≤n→m⊔n=n p)

  -- match indices of injectable data types
  match : ∀ {m n} {I J} {{i : Inject I}} {{j : Inject J}}
        → I m → J n → I (m ∧ n) × J (m ∧ n)
  match {m} {n} i j with total m n
  ... | inj₁ p rewrite              m≤n→m⊔n=n p = (inject≤ p i , j)
  ... | inj₂ p rewrite ∧-comm m n | m≤n→m⊔n=n p = (i , inject≤ p j)

  ----------------------------------------------------------------------------
  -- * define hint databases                                              * --
  ----------------------------------------------------------------------------

  record IsHintDB : Set₁ where
    field
      HintDB   : Set
      Hint     : ℕ → Set

    Hints : Set
    Hints = List (∃ Hint)

    field
      getHints   : HintDB → Hints
      getRule    : ∀ {k} → Hint k → Rule k
      getTr      : ∀ {k} → Hint k → (HintDB → HintDB)
      ε          : HintDB
      _∙_        : HintDB → HintDB → HintDB
      return     : ∀ {k} → Rule k → HintDB

    fromRules : Rules → HintDB
    fromRules []             = ε
    fromRules ((k , r) ∷ rs) = return r ∙ fromRules rs

  ----------------------------------------------------------------------------
  -- * define simple hint databases                                       * --
  ----------------------------------------------------------------------------

  simpleHintDB : IsHintDB
  simpleHintDB = record
    { HintDB   = Rules
    ; Hint     = Rule
    ; getHints = id
    ; getRule  = id
    ; getTr    = const id
    ; ε        = []
    ; _∙_      = _++_
    ; return   = λ r → [ _ , r ]
    }

  ----------------------------------------------------------------------------
  -- * define search trees, proofs and partial proofs                     * --
  ----------------------------------------------------------------------------

  -- simple alias to set apart the goal term
  Goal = Term

  -- search trees
  data SearchTree (A : Set) : Set where
    leaf : A → SearchTree A
    node : List (∞ (SearchTree A)) → SearchTree A

  -- representation of a failed branch
  fail : ∀ {A} → SearchTree A
  fail = node []

  data Proof : Set where
     con : (name : RuleName) (args : List Proof) → Proof

  -- representation of an incomplete proof
  Proof′ : ℕ → Set
  Proof′ m = ∃[ k ] (Vec (Goal m) k × (Vec Proof k → Proof))

  con′ : ∀ {n k} (r : Rule n) → Vec Proof (arity r + k) → Vec Proof (suc k)
  con′ {n} {k} r xs = head ∷ rest
    where
      head : Proof
      head = con (name r) (Vec.toList $ Vec.take (arity r) xs)
      rest : Vec Proof k
      rest = Vec.drop (arity r) xs

  ----------------------------------------------------------------------------
  -- * define proof search function                                       * --
  ----------------------------------------------------------------------------

  module Extensible (isHintDB : IsHintDB) where

    open IsHintDB isHintDB

    solve : ∀ {m} → Goal m → HintDB → SearchTree Proof
    solve {m} g = solveAcc {m} (1 , g ∷ [] , Vec.head)
      where
        solveAcc : ∀ {m} → Proof′ m → HintDB → SearchTree Proof
        solveAcc {m} (0     ,     [] , p) _  = leaf (p [])
        solveAcc {m} (suc k , g ∷ gs , p) db = node (steps (getHints db))
          where
            step : ∃[ δ ] (Hint δ) → ∞ (SearchTree Proof)
            step (δ , h) with unify (inject δ g) (raise m (conclusion (getRule h)))
            ... | nothing        = ♯ node [] -- fail
            ... | just (n , mgu) = ♯ solveAcc {n} prf (getTr h db)
              where
                prf : Proof′ n
                prf = arity (getRule h) + k , gs′ , (p ∘ con′ (getRule h))
                  where
                    prm′ = raise m (Vec.fromList (premises (getRule h)))
                    gs′  = Vec.map (replace (sub mgu)) (prm′ Vec.++ inject δ gs)

            -- equivalent to `map step` due to termination checker
            steps : List (∃ Hint) → List (∞ (SearchTree Proof))
            steps []       = []
            steps (h ∷ hs) = step h ∷ steps hs

  ----------------------------------------------------------------------------
  -- * define various search strategies                                   * --
  ----------------------------------------------------------------------------

  Strategy : Set₁
  Strategy = ∀ {A} (depth : ℕ) → SearchTree A → List A

  dfs : Strategy
  dfs  zero    _        = []
  dfs (suc k) (leaf x)  = x ∷ []
  dfs (suc k) (node xs) = concatMap (λ x → dfs k (♭ x)) xs

  bfs : Strategy
  bfs depth t = concat (Vec.toList (bfsAcc depth t))
    where
      merge : ∀ {A : Set} {k} → (xs ys : Vec (List A) k) → Vec (List A) k
      merge [] [] = []
      merge (x ∷ xs) (y ∷ ys) = (x ++ y) ∷ merge xs ys

      empty : ∀ {A : Set} {k} → Vec (List A) k
      empty {k = zero}  = []
      empty {k = suc k} = [] ∷ empty

      bfsAcc : ∀ {A} (depth : ℕ) → SearchTree A → Vec (List A) depth
      bfsAcc  zero   _         = []
      bfsAcc (suc k) (leaf x)  = (x ∷ []) ∷ empty
      bfsAcc (suc k) (node xs) = [] ∷ foldr merge empty (List.map (λ x → bfsAcc k (♭ x)) xs)

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.HomotopyGroup.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
import Cubical.Foundations.GroupoidLaws as GL

open import Cubical.Data.Nat
open import Cubical.Data.Group.Base

open import Cubical.HITs.SetTruncation

Pointed : ∀ {ℓ} → Type (ℓ-suc ℓ)
Pointed {ℓ} = Σ[ A ∈ Type ℓ ] A

Ω : ∀ {ℓ} → Pointed {ℓ} → Pointed {ℓ}
Ω (A , a ) = ( (a ≡ a) , refl)

Ω^_ : ∀ {ℓ} → ℕ → Pointed {ℓ} → Pointed {ℓ}
(Ω^ 0) p = p
(Ω^ (suc n)) p = Ω ((Ω^ n) p)

π^_ : ∀ {ℓ} → ℕ → Pointed {ℓ} → Group {ℓ}
π^_ {ℓ} n p = group ∥ A ∥₀  squash₀ g
  where
    n' : ℕ
    n' = suc n

    A : Type ℓ
    A = (Ω^ n') p .fst

    g : isGroup ∥ A ∥₀
    g = group-struct e _⁻¹ _⊙_ lUnit rUnit assoc lCancel rCancel
      where
        e : ∥ A ∥₀
        e = ∣ (Ω^ n') p .snd ∣₀

        _⁻¹ : ∥ A ∥₀ → ∥ A ∥₀
        _⁻¹ = elimSetTrunc {B = λ _ → ∥ A ∥₀} (λ x → squash₀) λ a → ∣  sym a ∣₀

        _⊙_ : ∥ A ∥₀ → ∥ A ∥₀ → ∥ A ∥₀
        _⊙_ = elimSetTrunc2 (λ _ _ → squash₀) λ a₀ a₁ → ∣ a₀ ∙ a₁ ∣₀

        lUnit : (a : ∥ A ∥₀) → (e ⊙ a) ≡ a
        lUnit = elimSetTrunc (λ _ → isProp→isSet (squash₀ _ _))
                (λ a → cong ∣_∣₀ (sym (GL.lUnit a) ))

        rUnit : (a : ∥ A ∥₀) → a ⊙ e ≡ a
        rUnit = elimSetTrunc (λ _ → isProp→isSet (squash₀ _ _))
                (λ a → cong ∣_∣₀ (sym (GL.rUnit a) ))

        assoc : (a b c : ∥ A ∥₀) → ((a ⊙ b) ⊙ c) ≡ (a ⊙ (b ⊙ c))
        assoc = elimSetTrunc3 (λ _ _ _ → isProp→isSet (squash₀ _ _))
                (λ a b c → cong ∣_∣₀ (sym (GL.assoc _ _ _)))

        lCancel : (a : ∥ A ∥₀) → ((a ⁻¹) ⊙ a) ≡ e
        lCancel = elimSetTrunc (λ _ → isProp→isSet (squash₀ _ _))
                  λ a → cong ∣_∣₀ (GL.lCancel _)

        rCancel : (a : ∥ A ∥₀) → (a ⊙ (a ⁻¹)) ≡ e
        rCancel = elimSetTrunc (λ _ → isProp→isSet (squash₀ _ _))
                  λ a → cong ∣_∣₀ (GL.rCancel _)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.types.Bool
open import lib.types.FunctionSeq
open import lib.types.Pointed
open import lib.types.Suspension.Core
open import lib.types.Suspension.Flip
open import lib.types.Suspension.Iterated
open import lib.types.Suspension.IteratedEquivs
open import lib.types.Suspension.IteratedTrunc
open import lib.types.Suspension.Trunc
open import lib.types.TLevel
open import lib.types.Truncation

module lib.types.Suspension.IteratedFlip where

module _ {i} {A : Type i} where
  maybe-Susp^-flip : ∀ (n : ℕ)
    → Bool
    → Susp^ n A → Susp^ n A
  maybe-Susp^-flip 0 _ = idf _
  maybe-Susp^-flip (S _) b = maybe-Susp-flip b

  Susp-fmap-maybe-Susp^-flip : ∀ (n : ℕ) (b : Bool)
    → (n == 0 → b == false)
    → maybe-Susp^-flip (S n) b ∼ Susp-fmap (maybe-Susp^-flip n b)
  Susp-fmap-maybe-Susp^-flip O b h x =
    maybe-Susp^-flip 1 b x
      =⟨ ap (λ c → maybe-Susp^-flip 1 c x) (h idp) ⟩
    x
      =⟨ ! (Susp-fmap-idf A x) ⟩
    Susp-fmap (idf A) x =∎
  Susp-fmap-maybe-Susp^-flip (S n) true h x = ! (Susp-fmap-flip x)
  Susp-fmap-maybe-Susp^-flip (S n) false h x = ! (Susp-fmap-idf (Susp^ (S n) A) x)

module _ {i} {X : Ptd i} where

  ⊙maybe-Susp^-flip : ∀ (n : ℕ)
    → Bool
    → ⊙Susp^ n X ⊙→ ⊙Susp^ n X
  ⊙maybe-Susp^-flip 0 _ = ⊙idf _
  ⊙maybe-Susp^-flip (S n) b = ⊙maybe-Susp-flip (⊙Susp^ n X) b

  de⊙-⊙maybe-Susp^-flip : ∀ (n : ℕ) (b : Bool)
    → fst (⊙maybe-Susp^-flip n b) == maybe-Susp^-flip n b
  de⊙-⊙maybe-Susp^-flip O b = idp
  de⊙-⊙maybe-Susp^-flip (S n) b = de⊙-⊙maybe-Susp-flip _ b

  ⊙maybe-Susp^-flip-false : ∀ (n : ℕ)
    → ⊙maybe-Susp^-flip n false == ⊙idf _
  ⊙maybe-Susp^-flip-false O = idp
  ⊙maybe-Susp^-flip-false (S n) = idp

  ⊙maybe-Susp^-flip-flip : ∀ (n : ℕ) (b c : Bool)
    → ⊙maybe-Susp^-flip n b ◃⊙∘ ⊙maybe-Susp^-flip n c ◃⊙idf
      =⊙∘
      ⊙maybe-Susp^-flip n (xor b c) ◃⊙idf
  ⊙maybe-Susp^-flip-flip 0     _ _ = =⊙∘-in idp
  ⊙maybe-Susp^-flip-flip (S n) b c = ⊙maybe-Susp-flip-flip (⊙Susp^ n X) b c

  ⊙Susp-fmap-maybe-Susp^-flip : ∀ (n : ℕ) (b : Bool)
    → (n == 0 → b == false)
    → ⊙Susp-fmap (maybe-Susp^-flip n b) == ⊙maybe-Susp^-flip (S n) b
  ⊙Susp-fmap-maybe-Susp^-flip 0 b h =
    ⊙Susp-fmap (idf (de⊙ X))
      =⟨ =⊙∘-out (⊙Susp-fmap-idf _) ⟩
    ⊙idf _
      =⟨ ap (⊙maybe-Susp^-flip 1) (! (h idp)) ⟩
    ⊙maybe-Susp^-flip 1 b =∎
  ⊙Susp-fmap-maybe-Susp^-flip (S n) b h = ⊙Susp-fmap-maybe-Susp-flip b

Susp^-fmap-Susp-flip : ∀ {i} (m : ℕ) {A : Type i} (s : Susp^ (S m) (Susp A))
  → Susp^-fmap (S m) Susp-flip s == Susp-flip s
Susp^-fmap-Susp-flip O {A} s = Susp-fmap-flip s
Susp^-fmap-Susp-flip (S m) {A} s =
  Susp^-fmap (S (S m)) Susp-flip s
    =⟨ ap (λ f → Susp-fmap f s) (λ= (Susp^-fmap-Susp-flip m)) ⟩
  Susp-fmap Susp-flip s
    =⟨ Susp-fmap-flip s ⟩
  Susp-flip s =∎

abstract
  ⊙Susp^-fmap-⊙Susp-flip : ∀ {i} (m : ℕ) {X : Ptd i}
    → ⊙Susp^-fmap (S m) (⊙Susp-flip X) == ⊙Susp-flip (⊙Susp^ m (⊙Susp (de⊙ X)))
  ⊙Susp^-fmap-⊙Susp-flip 0 {X} = ⊙Susp-fmap-Susp-flip
  ⊙Susp^-fmap-⊙Susp-flip (S m) {X} =
    ⊙Susp^-fmap (S (S m)) (⊙Susp-flip X)
      =⟨ ap ⊙Susp-fmap (λ= (Susp^-fmap-Susp-flip m)) ⟩
    ⊙Susp-fmap Susp-flip
      =⟨ ⊙Susp-fmap-Susp-flip ⟩
    ⊙Susp-flip (⊙Susp^ (S m) (⊙Susp (de⊙ X))) =∎

  ⊙maybe-Susp^-flip-natural : ∀ {i} {j} {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
    (n : ℕ) (b : Bool)
    → ⊙Susp^-fmap n f ⊙∘ ⊙maybe-Susp^-flip n b ==
      ⊙maybe-Susp^-flip n b ⊙∘ ⊙Susp^-fmap n f
  ⊙maybe-Susp^-flip-natural f O b = ! (⊙λ= (⊙∘-unit-l f))
  ⊙maybe-Susp^-flip-natural f (S n) b = ⊙maybe-Susp-flip-natural (⊙Susp^-fmap n f) b

  ⊙maybe-Susp^-flip-natural-=⊙∘ : ∀ {i} {X Y : Ptd i} (f : X ⊙→ Y)
    (n : ℕ) (b : Bool)
    → ⊙Susp^-fmap n f ◃⊙∘
      ⊙maybe-Susp^-flip n b ◃⊙idf
      =⊙∘
      ⊙maybe-Susp^-flip n b ◃⊙∘
      ⊙Susp^-fmap n f ◃⊙idf
  ⊙maybe-Susp^-flip-natural-=⊙∘ f n b =
    =⊙∘-in (⊙maybe-Susp^-flip-natural f n b)

abstract
  ⊙Susp^-comm-flip : ∀ {i} (m n : ℕ) (X : Ptd i)
    → ⊙Susp^-fmap n (⊙Susp-flip (⊙Susp^ m X)) ◃⊙∘
      ⊙coe (⊙Susp^-comm (S m) n {X}) ◃⊙idf
      =⊙∘
      ⊙coe (⊙Susp^-comm (S m) n {X}) ◃⊙∘
      ⊙Susp-flip (⊙Susp^ m (⊙Susp^ n X)) ◃⊙idf
  ⊙Susp^-comm-flip m O X =
    ⊙Susp-flip (⊙Susp^ m X) ◃⊙∘
    ⊙coe (⊙Susp^-comm (S m) 0) ◃⊙idf
      =⊙∘⟨ 1 & 1 & =⊙∘-in {gs = ⊙idf-seq} $ ap ⊙coe (⊙Susp^-comm-0-r (S m) X) ⟩
    ⊙Susp-flip (⊙Susp^ m X) ◃⊙idf
      =⊙∘⟨ 0 & 0 & =⊙∘-in {gs = ⊙coe (⊙Susp^-comm (S m) O) ◃⊙idf} $
                   ! $ ap ⊙coe (⊙Susp^-comm-0-r (S m) X) ⟩
    ⊙coe (⊙Susp^-comm (S m) O) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ m (⊙Susp^ O X)) ◃⊙idf ∎⊙∘
  ⊙Susp^-comm-flip m (S n) X =
    ⊙Susp^-fmap (S n) (⊙Susp-flip (⊙Susp^ m X)) ◃⊙∘
    ⊙coe (⊙Susp^-comm (S m) (S n)) ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ⊙Susp^-fmap-⊙Susp-flip n {⊙Susp^ m X} ⟩
    ⊙Susp-flip (⊙Susp^ n (⊙Susp (Susp^ m (de⊙ X)))) ◃⊙∘
    ⊙coe (⊙Susp^-comm (S m) (S n)) ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & p ⟩
    ⊙Susp-flip (⊙Susp^ n (⊙Susp (Susp^ m (de⊙ X)))) ◃⊙∘
    ⊙Susp-fmap (fst (⊙coe (⊙Susp^-comm m (S n) ∙ ⊙Susp^-comm 1 n))) ◃⊙idf
      =⊙∘⟨ =⊙∘-in {gs = ⊙Susp-fmap (fst (⊙coe (⊙Susp^-comm m (S n) {X} ∙ ⊙Susp^-comm 1 n {⊙Susp^ m X}))) ◃⊙∘
                        ⊙Susp-flip (⊙Susp^ m (⊙Susp (Susp^ n (de⊙ X)))) ◃⊙idf} $
           ⊙Susp-flip-natural (⊙coe (⊙Susp^-comm m (S n) ∙ ⊙Susp^-comm 1 n)) ⟩
    ⊙Susp-fmap (fst (⊙coe (⊙Susp^-comm m (S n) {X} ∙ ⊙Susp^-comm 1 n {⊙Susp^ m X}))) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ m (⊙Susp (Susp^ n (de⊙ X)))) ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ! p ⟩
    ⊙coe (⊙Susp^-comm (S m) (S n)) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ m (⊙Susp^ (S n) X)) ◃⊙idf ∎⊙∘
    where
    p : ⊙coe (⊙Susp^-comm (S m) (S n) {X}) ==
        ⊙Susp-fmap (fst (⊙coe (⊙Susp^-comm m (S n) {X} ∙ ⊙Susp^-comm 1 n {⊙Susp^ m X})))
    p =
      ap ⊙coe (⊙Susp^-comm-S-S m n) ∙
      ! (⊙transport-⊙coe ⊙Susp (Susp^-comm m (S n) ∙ Susp^-comm 1 n)) ∙
      ⊙transport-⊙Susp (Susp^-comm m (S n) ∙ Susp^-comm 1 n) ∙
      ap (⊙Susp-fmap ∘ coe) (ap2 _∙_ (! (de⊙-⊙Susp^-comm m (S n) {X}))
                                     (! (de⊙-⊙Susp^-comm 1 n {⊙Susp^ m X}))) ∙
      ap (⊙Susp-fmap ∘ coe) (∙-ap de⊙ (⊙Susp^-comm m (S n)) (⊙Susp^-comm 1 n))

  ⊙maybe-Susp^-flip-⊙Susp^-comm : ∀ {i} (X : Ptd i) (m n : ℕ) (b : Bool)
    → ⊙Susp^-fmap n (⊙maybe-Susp^-flip m b) ◃⊙∘
      ⊙coe (⊙Susp^-comm m n {X}) ◃⊙idf
      =⊙∘
      ⊙coe (⊙Susp^-comm m n {X}) ◃⊙∘
      ⊙maybe-Susp^-flip m b ◃⊙idf
  ⊙maybe-Susp^-flip-⊙Susp^-comm X O n b =
    ⊙Susp^-fmap n (⊙idf X) ◃⊙∘
    ⊙coe (⊙Susp^-comm 0 n) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙Susp^-fmap-idf n X ⟩
    ⊙coe (⊙Susp^-comm 0 n) ◃⊙idf
      =⊙∘⟨ 1 & 0 & ⊙contract ⟩
    ⊙coe (⊙Susp^-comm 0 n) ◃⊙∘
    ⊙idf (⊙Susp^ n X) ◃⊙idf ∎⊙∘
  ⊙maybe-Susp^-flip-⊙Susp^-comm X (S m) n true = ⊙Susp^-comm-flip m n X
  ⊙maybe-Susp^-flip-⊙Susp^-comm X (S m) n false =
    ⊙Susp^-fmap n (⊙idf (⊙Susp^ (S m) X)) ◃⊙∘
    ⊙coe (⊙Susp^-comm (S m) n) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙Susp^-fmap-idf n (⊙Susp^ (S m) X) ⟩
    ⊙coe (⊙Susp^-comm (S m) n) ◃⊙idf
      =⊙∘⟨ 1 & 0 & ⊙contract ⟩
    ⊙coe (⊙Susp^-comm (S m) n) ◃⊙∘
    ⊙idf (⊙Susp^ (S m) (⊙Susp^ n X)) ◃⊙idf ∎⊙∘

module _ {i} (X : Ptd i) (m : ℕ₋₂) where

  ⊙Susp^-Trunc-swap-⊙maybe-Susp^-flip : ∀ (n : ℕ) (b : Bool)
    → ⊙Susp^-Trunc-swap X m n ◃⊙∘
      ⊙maybe-Susp^-flip n b ◃⊙idf
      =⊙∘
      ⊙Trunc-fmap (⊙maybe-Susp^-flip n b) ◃⊙∘
      ⊙Susp^-Trunc-swap X m n ◃⊙idf
  ⊙Susp^-Trunc-swap-⊙maybe-Susp^-flip O b =
    =⊙∘-in (! (⊙λ= ⊙Trunc-fmap-⊙idf))
  ⊙Susp^-Trunc-swap-⊙maybe-Susp^-flip (S n) true =
    ⊙Susp^-Trunc-swap X m (S n) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ n (⊙Trunc m X)) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙expand $
           ⊙Susp-Trunc-swap (Susp^ n (de⊙ X)) (⟨ n ⟩₋₂ +2+ m) ◃⊙∘
           ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ X) m n) ◃⊙idf ⟩
    ⊙Susp-Trunc-swap (Susp^ n (de⊙ X)) (⟨ n ⟩₋₂ +2+ m) ◃⊙∘
    ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ X) m n) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ n (⊙Trunc m X)) ◃⊙idf
      =⊙∘⟨ 1 & 2 & =⊙∘-in
           {gs = ⊙Susp-flip (⊙Trunc (⟨ n ⟩₋₂ +2+ m) (⊙Susp^ n X)) ◃⊙∘
                 ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ X) m n) ◃⊙idf} $
           ! $ ⊙Susp-flip-natural (⊙Susp^-Trunc-swap X m n) ⟩
    ⊙Susp-Trunc-swap (Susp^ n (de⊙ X)) (⟨ n ⟩₋₂ +2+ m) ◃⊙∘
    ⊙Susp-flip (⊙Trunc (⟨ n ⟩₋₂ +2+ m) (⊙Susp^ n X)) ◃⊙∘
    ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ X) m n) ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙Susp-Trunc-swap-⊙Susp-flip (⟨ n ⟩₋₂ +2+ m) ⟩
    ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n X)) ◃⊙∘
    ⊙Susp-Trunc-swap (Susp^ n (de⊙ X)) (⟨ n ⟩₋₂ +2+ m) ◃⊙∘
    ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ X) m n) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙contract ⟩
    ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n X)) ◃⊙∘
    ⊙Susp^-Trunc-swap X m (S n) ◃⊙idf ∎⊙∘
  ⊙Susp^-Trunc-swap-⊙maybe-Susp^-flip (S n) false =
    ⊙Susp^-Trunc-swap X m (S n) ◃⊙∘
    ⊙idf _ ◃⊙idf
      =⊙∘⟨ 1 & 1 & ⊙expand ⊙idf-seq ⟩
    ⊙Susp^-Trunc-swap X m (S n) ◃⊙idf
      =⊙∘₁⟨ 0 & 0 & ! (⊙λ= ⊙Trunc-fmap-⊙idf) ⟩
    ⊙Trunc-fmap (⊙idf (⊙Susp (de⊙ (⊙Susp^ n X)))) ◃⊙∘
    ⊙Susp^-Trunc-swap X m (S n) ◃⊙idf ∎⊙∘

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Float

NaN : Float
NaN = primFloatDiv 0.0 0.0

-NaN : Float
-NaN = primFloatNegate NaN

NaN≮NaN : primFloatNumericalLess NaN NaN ≡ false
NaN≮NaN = refl

-NaN≮-NaN : primFloatNumericalLess -NaN -NaN ≡ false
-NaN≮-NaN = refl

NaN≮-NaN : primFloatNumericalLess NaN -NaN ≡ false
NaN≮-NaN = refl

-NaN<NaN : primFloatNumericalLess -NaN NaN ≡ false
-NaN<NaN = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Monoid.Submonoid where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open import Cubical.Algebra
open import Cubical.Algebra.Monoid.Morphism
open import Cubical.Algebra.Semigroup.Subsemigroup

open import Cubical.Relation.Unary
open import Cubical.Relation.Unary.Subtype

open import Cubical.HITs.PropositionalTruncation

record IsSubmonoid {c ℓ} (M : Monoid c) (Member : Pred ⟨ M ⟩ ℓ) : Type (ℓ-max c ℓ) where
  constructor issubmonoid

  private module M = Monoid M

  field
    preservesOp : M._•_ Preserves₂ Member
    preservesId : M.ε ∈ Member

  isSubsemigroup : IsSubsemigroup M.semigroup Member
  isSubsemigroup = record { closed = preservesOp }

  open IsSubsemigroup isSubsemigroup hiding (closed; _^_) public

  ε : Carrier
  ε = M.ε , preservesId

  identityˡ : LeftIdentity ε _•_
  identityˡ _ = ΣPathTransport→PathΣ _ _ (M.identityˡ _ , isProp[ Member ] _ _ _)

  identityʳ : RightIdentity ε _•_
  identityʳ _ = ΣPathTransport→PathΣ _ _ (M.identityʳ _ , isProp[ Member ] _ _ _)

  identity : Identity ε _•_
  identity = identityˡ , identityʳ

  isMonoid : IsMonoid Carrier _•_ ε
  isMonoid = record
    { isSemigroup = isSemigroup
    ; identity = identity
    }

  monoid : Monoid _
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid using (ε-uniqueˡ; ε-uniqueʳ; _^_) public

record Submonoid {c} (M : Monoid c) ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  constructor mksubmonoid

  private module M = Monoid M

  field
    Member : Pred ⟨ M ⟩ ℓ
    isSubmonoid : IsSubmonoid M Member

  open IsSubmonoid isSubmonoid public

  subsemigroup : Subsemigroup M.semigroup ℓ
  subsemigroup = record { isSubsemigroup = isSubsemigroup }

  open Subsemigroup subsemigroup public using (submagma)

instance
  SubmonoidCarrier : ∀ {c ℓ} {M : Monoid c} → HasCarrier (Submonoid M ℓ) _
  SubmonoidCarrier = record { ⟨_⟩ = Submonoid.Carrier }

module _ {ℓ} (M : Monoid ℓ) where
  open Monoid M

  ε-isSubmonoid : IsSubmonoid M ｛ ε ｝
  ε-isSubmonoid = record
    { preservesOp = map2 λ p q → cong₂ _•_ p q ∙ identityʳ ε
    ; preservesId = ∣ refl ∣
    }

  ε-submonoid : Submonoid M _
  ε-submonoid = record { isSubmonoid = ε-isSubmonoid }

  U-isSubmonoid : IsSubmonoid M U
  U-isSubmonoid = record {} -- trivial

  U-submonoid : Submonoid M _
  U-submonoid = record { isSubmonoid = U-isSubmonoid }


text:
open import Preliminaries
open import Source-lang

module Examples-Source where

----- examples

  nexp = [] |- nat

  dbl-test4 : nexp
  dbl-test4 = app dbl (suc (suc z))
  four : nexp
  four = suc (suc (suc (suc z)))
  eqs4 : evals dbl-test4 four ((0c +c 0c) +c (0c +c (1c +c (0c +c (0c +c (1c +c (0c +c (0c +c (1c +c 0c)))))))))
  eqs4 = app-evals lam-evals (s-evals (s-evals z-evals)) (rec-evals (s-evals (s-evals z-evals)) (evals-rec-s (s-evals (s-evals (force-evals delay-evals (rec-evals (s-evals z-evals) (evals-rec-s (s-evals (s-evals (force-evals delay-evals (rec-evals z-evals (evals-rec-z z-evals))))))))))))

  dbl-test0 : nexp
  dbl-test0 = app dbl z
  zero : nexp
  zero = z
  eqs0 : evals dbl-test0 zero ((0c +c 0c) +c (0c +c (1c +c 0c)))
  eqs0 = app-evals lam-evals z-evals (rec-evals z-evals (evals-rec-z z-evals))

  add-test0 : nexp
  add-test0 = app (app add z) z
  eqs01 : evals add-test0 zero ((((0c +c 0c) +c 0c) +c 0c) +c (0c +c (1c +c 0c)))
  eqs01 = app-evals (app-evals lam-evals z-evals lam-evals) z-evals (rec-evals z-evals (evals-rec-z z-evals))

  one : nexp
  one = suc z
  two : nexp
  two = suc (suc z)

  add-test1 : nexp
  add-test1 = app (app add (suc z)) z
  eqs11 : evals add-test1 one ((((0c +c 0c) +c 0c) +c 0c) +c
                                (0c +c (1c +c (0c +c (0c +c (1c +c 0c))))))
  eqs11 = app-evals (app-evals lam-evals (s-evals z-evals) lam-evals) z-evals (rec-evals (s-evals z-evals) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals z-evals (evals-rec-z z-evals))))))

  add-test1' : nexp
  add-test1' = app (app add z) (suc z)
  eqs11' : evals add-test1' one ((((0c +c 0c) +c 0c) +c 0c) +c (0c +c (1c +c 0c)))
  eqs11' = app-evals (app-evals lam-evals z-evals lam-evals) (s-evals z-evals) (rec-evals z-evals (evals-rec-z (s-evals z-evals)))

  add-test2 : nexp
  add-test2 = app (app add z) four
  eqs12 : evals add-test2 four ((((0c +c 0c) +c 0c) +c 0c) +c (0c +c (1c +c 0c)))
  eqs12 = app-evals (app-evals lam-evals z-evals lam-evals) (s-evals (s-evals (s-evals (s-evals z-evals)))) (rec-evals z-evals (evals-rec-z (s-evals (s-evals (s-evals (s-evals z-evals))))))

  add-test2' : nexp
  add-test2' = app (app add four) z
  eqs12' : evals add-test2' four ((((0c +c 0c) +c 0c) +c 0c) +c
                                   (0c +c
                                    (1c +c
                                     (0c +c
                                      (0c +c
                                       (1c +c
                                        (0c +c
                                         (0c +c
                                          (1c +c (0c +c (0c +c (1c +c (0c +c (0c +c (1c +c 0c)))))))))))))))
  eqs12' = app-evals (app-evals lam-evals (s-evals (s-evals (s-evals (s-evals z-evals)))) lam-evals) z-evals (rec-evals (s-evals (s-evals (s-evals (s-evals z-evals)))) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals (s-evals (s-evals (s-evals z-evals))) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals (s-evals (s-evals z-evals)) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals (s-evals z-evals) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals z-evals (evals-rec-z z-evals))))))))))))))))))

  mult-test1 : nexp
  mult-test1 = app (app mult two) two
  eqs111 : evals mult-test1 four ((((0c +c 0c) +c 0c) +c 0c) +c
                                   (0c +c
                                    (1c +c
                                     ((((0c +c 0c) +c 0c) +c
                                       (0c +c
                                        (0c +c
                                         (1c +c
                                          ((((0c +c 0c) +c 0c) +c (0c +c (0c +c (1c +c 0c)))) +c
                                           (0c +c
                                            (1c +c (0c +c (0c +c (1c +c (0c +c (0c +c (1c +c 0c)))))))))))))
                                      +c
                                      (0c +c
                                       (1c +c (0c +c (0c +c (1c +c (0c +c (0c +c (1c +c 0c))))))))))))
  eqs111 = app-evals (app-evals lam-evals (s-evals (s-evals z-evals)) lam-evals) (s-evals (s-evals z-evals)) (rec-evals (s-evals (s-evals z-evals)) (evals-rec-s (app-evals (app-evals lam-evals (s-evals (s-evals z-evals)) lam-evals) (force-evals delay-evals (rec-evals (s-evals z-evals) (evals-rec-s (app-evals (app-evals lam-evals (s-evals (s-evals z-evals)) lam-evals) (force-evals delay-evals (rec-evals z-evals (evals-rec-z z-evals))) (rec-evals (s-evals (s-evals z-evals)) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals (s-evals z-evals) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals z-evals (evals-rec-z z-evals)))))))))))))) (rec-evals (s-evals (s-evals z-evals)) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals (s-evals z-evals) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals z-evals (evals-rec-z (s-evals (s-evals z-evals)))))))))))))))

  mult-test2 : nexp
  mult-test2 = app (app mult one) one
  eqs112 : evals mult-test2 one ((((0c +c 0c) +c 0c) +c 0c) +c
                                  (0c +c
                                   (1c +c
                                    ((((0c +c 0c) +c 0c) +c (0c +c (0c +c (1c +c 0c)))) +c
                                     (0c +c (1c +c (0c +c (0c +c (1c +c 0c)))))))))
  eqs112 = app-evals (app-evals lam-evals (s-evals z-evals) lam-evals) (s-evals z-evals) (rec-evals (s-evals z-evals) (evals-rec-s (app-evals (app-evals lam-evals (s-evals z-evals) lam-evals) (force-evals delay-evals (rec-evals z-evals (evals-rec-z z-evals))) (rec-evals (s-evals z-evals) (evals-rec-s (s-evals (force-evals delay-evals (rec-evals z-evals (evals-rec-z z-evals)))))))))

  mult-test0 : nexp
  mult-test0 = app (app mult zero) zero
  eqs00 : evals mult-test0 zero ((((0c +c 0c) +c 0c) +c 0c) +c (0c +c (1c +c 0c)))
  eqs00 = app-evals (app-evals lam-evals z-evals lam-evals) z-evals (rec-evals z-evals (evals-rec-z z-evals))

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda