text:
module Tactic.Nat.Subtract.By where

open import Prelude hiding (abs)
open import Builtin.Reflection
open import Tactic.Reflection.Quote
open import Tactic.Reflection.DeBruijn
open import Tactic.Reflection.Substitute
open import Tactic.Reflection
open import Control.Monad.State

open import Tactic.Nat.Reflect
open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Tactic.Nat.Auto
open import Tactic.Nat.Auto.Lemmas
open import Tactic.Nat.Simpl.Lemmas
open import Tactic.Nat.Simpl
open import Tactic.Nat.Refute
open import Tactic.Nat.Reflect

open import Tactic.Nat.Subtract.Exp
open import Tactic.Nat.Subtract.Reflect
open import Tactic.Nat.Subtract.Lemmas
open import Tactic.Nat.Less.Lemmas

private
  NFGoal : (R₁ R₂ : Nat → Nat → Set) (a b c d : SubNF) → Env Var → Set
  NFGoal _R₁_ _R₂_ a b c d ρ = ⟦ a ⟧ns (atomEnvS ρ) R₁ ⟦ b ⟧ns (atomEnvS ρ) → ⟦ c ⟧ns (atomEnvS ρ) R₂ ⟦ d ⟧ns (atomEnvS ρ)

  follows-diff-prf : {a b c d : Nat} → a ≤ b → b < c → c ≤ d → d ≡ suc (d - suc a) + a
  follows-diff-prf {a} (diff! i) (diff! j) (diff! k) =
    sym $ (λ z → suc z + a) $≡ lem-sub-zero (k + suc (j + (i + a))) (suc a) (i + j + k) auto ʳ⟨≡⟩
          auto

  decide-leq : ∀ u v ρ → Maybe (⟦ u ⟧ns (atomEnvS ρ) ≤ ⟦ v ⟧ns (atomEnvS ρ))
  decide-leq u v ρ with cancel u v | λ a b → cancel-sound-s′ a b u v (atomEnvS ρ)
  ... | [] , d | sound =
    let eval x = ⟦ x ⟧ns (atomEnvS ρ) in
    just (diff (eval d) $ sym (sound (suc (eval d)) 1 auto))
  ... | _  , _ | _     = nothing

  by-proof-less-nf : ∀ u u₁ v v₁ ρ → Maybe (NFGoal _<_ _<_ u u₁ v v₁ ρ)
  by-proof-less-nf u u₁ v v₁ ρ = do
    v≤u   ← decide-leq v  u  ρ
    u₁≤v₁ ← decide-leq u₁ v₁ ρ
    pure λ u<u₁ →
         diff (⟦ v₁ ⟧ns (atomEnvS ρ) - suc (⟦ v ⟧ns (atomEnvS ρ)))
              (follows-diff-prf v≤u u<u₁ u₁≤v₁)

  by-proof-less : ∀ a a₁ b b₁ ρ → Maybe (SubExpLess a a₁ ρ → SubExpLess b b₁ ρ)
  by-proof-less a a₁ b b₁ ρ with cancel (normSub a) (normSub a₁)
                               | cancel (normSub b) (normSub b₁)
                               | complicateSubLess a a₁ ρ
                               | simplifySubLess b b₁ ρ
  ... | u , u₁ | v , v₁ | compl | simpl = do
    prf ← by-proof-less-nf u u₁ v v₁ ρ
    pure (simpl ∘ prf ∘ compl)

  lem-plus-zero-r : (a b : Nat) → a + b ≡ 0 → b ≡ 0
  lem-plus-zero-r  zero   b eq = eq
  lem-plus-zero-r (suc a) b ()

  lem-leq-zero : {a b : Nat} → a ≤ b → b ≡ 0 → a ≡ 0
  lem-leq-zero (diff k eq) refl = lem-plus-zero-r k _ (follows-from (sym eq))

  ⟨+⟩-sound-ns : ∀ {Atom} {{_ : Ord Atom}} u v (ρ : Env Atom) → ⟦ u +nf v ⟧ns ρ ≡ ⟦ u ⟧ns ρ + ⟦ v ⟧ns ρ
  ⟨+⟩-sound-ns u v ρ =
    ns-sound (u +nf v) ρ ⟨≡⟩
    ⟨+⟩-sound u v ρ ⟨≡⟩ʳ
    _+_ $≡ ns-sound u ρ *≡ ns-sound v ρ

  by-proof-eq-nf : Nat → ∀ u u₁ v v₁ ρ → Maybe (NFGoal _≡_ _≡_ u u₁ v v₁ ρ)

  by-proof-eq-sub : Nat → ∀ u u₁ v v₁ v₂ ρ → Maybe (NFGoal _≡_ _≡_ u u₁ [ 1 , [ v ⟨-⟩ v₁ ] ] v₂ ρ)
  by-proof-eq-sub n u u₁ v v₁ v₂ ρ = do
    let eval  x = ⟦ x ⟧ns (atomEnvS ρ)
        evals x = ⟦ x ⟧sns ρ
    prf ← by-proof-eq-nf n u u₁ v (v₁ +nf v₂) ρ
    pure (λ u=u₁ →
      sym $ lem-sub-zero (evals v) (evals v₁) (eval v₂) $ sym $
        lem-eval-sns-ns v ρ ⟨≡⟩
        prf u=u₁ ⟨≡⟩
        ⟨+⟩-sound-ns v₁ v₂ (atomEnvS ρ) ⟨≡⟩ʳ
        (_+ eval v₂) $≡ (lem-eval-sns-ns v₁ ρ))

  by-proof-eq-sub₂ : Nat → ∀ u u₁ v v₁ v₂ v₃ ρ → Maybe (NFGoal _≡_ _≡_ u u₁ [ 1 , [ v ⟨-⟩ v₁ ] ] [ 1 , [ v₂ ⟨-⟩ v₃ ] ] ρ)
  by-proof-eq-sub₂ n u u₁ v v₁ v₂ v₃ ρ = do
    let eval  x = ⟦ x ⟧ns (atomEnvS ρ)
        evals x = ⟦ x ⟧sns ρ
    prf ← by-proof-eq-nf n u u₁ (v₃ +nf v) (v₂ +nf v₁) ρ
    pure λ u=u₁ →
      lem-sub (evals v₂) (evals v₃) (evals v) (evals v₁) $
        _+_ $≡ lem-eval-sns-ns v₃ ρ *≡ lem-eval-sns-ns v ρ ⟨≡⟩
        ⟨+⟩-sound-ns v₃ v (atomEnvS ρ) ʳ⟨≡⟩
        prf u=u₁ ⟨≡⟩ ⟨+⟩-sound-ns v₂ v₁ (atomEnvS ρ) ⟨≡⟩ʳ
        _+_ $≡ lem-eval-sns-ns v₂ ρ *≡ lem-eval-sns-ns v₁ ρ

  -- More advanced tactics for equalities
  --   a + b ≡ 0 → a ≡ 0
  by-proof-eq-adv : Nat → ∀ u u₁ v v₁ ρ → Maybe (NFGoal _≡_ _≡_ u u₁ v v₁ ρ)
  by-proof-eq-adv _ u  [] v  [] ρ = do leq ← decide-leq v  u  ρ; pure (lem-leq-zero leq)
  by-proof-eq-adv _ [] u₁ v  [] ρ = do leq ← decide-leq v  u₁ ρ; pure (lem-leq-zero leq ∘ sym)
  by-proof-eq-adv _ u  [] [] v₁ ρ = do leq ← decide-leq v₁ u  ρ; pure (sym ∘ lem-leq-zero leq)
  by-proof-eq-adv _ [] u₁ [] v₁ ρ = do leq ← decide-leq v₁ u₁ ρ; pure (sym ∘ lem-leq-zero leq ∘ sym)
  by-proof-eq-adv (suc n) u  u₁ [ 1 , [ v ⟨-⟩ v₁ ] ] [ 1 , [ v₂ ⟨-⟩ v₃ ] ] ρ = by-proof-eq-sub₂ n u u₁ v v₁ v₂ v₃ ρ
  by-proof-eq-adv n u  u₁ [ 1 , [ v ⟨-⟩ v₁ ] ] v₂ ρ = by-proof-eq-sub n u u₁ v v₁ v₂ ρ
  by-proof-eq-adv (suc n) u u₁ v₂ [ 1 , [ v ⟨-⟩ v₁ ] ] ρ = do
    prf ← by-proof-eq-sub n u u₁ v v₁ v₂ ρ
    pure (sym ∘ prf)
  by-proof-eq-adv _ u  u₁ v  v₁ ρ = nothing

  by-proof-eq-nf n u u₁  v  v₁ ρ with u == v | u₁ == v₁
  by-proof-eq-nf n u u₁ .u .u₁ ρ | yes refl | yes refl = just id
  ... | _ | _ with u == v₁ | u₁ == v -- try sym
  by-proof-eq-nf n u u₁ .u₁ .u ρ | _ | _ | yes refl | yes refl = just sym
  ... | _ | _ = by-proof-eq-adv n u u₁ v v₁ ρ -- try advanced stuff

  by-proof-eq : ∀ a a₁ b b₁ ρ → Maybe (SubExpEq a a₁ ρ → SubExpEq b b₁ ρ)
  by-proof-eq a a₁ b b₁ ρ with cancel (normSub a) (normSub a₁)
                             | cancel (normSub b) (normSub b₁)
                             | complicateSubEq a a₁ ρ
                             | simplifySubEq b b₁ ρ
  ... | u , u₁ |  v ,  v₁ | compl | simpl = do
    prf ← by-proof-eq-nf 10 u u₁ v v₁ ρ
    pure (simpl ∘ prf ∘ compl)

  not-less-zero′ : {n : Nat} → n < 0 → ⊥
  not-less-zero′ (diff _ ())

  not-less-zero : {A : Set} {n : Nat} → n < 0 → A
  not-less-zero n<0 = ⊥-elim (erase-⊥ (not-less-zero′ n<0))

  less-one-is-zero : {n : Nat} → n < 1 → n ≡ 0
  less-one-is-zero {zero} _ = refl
  less-one-is-zero {suc n} (diff k eq) = refute eq

  by-proof-less-eq-nf : ∀ u u₁ v v₁ ρ → Maybe (NFGoal _<_ _≡_ u u₁ v v₁ ρ)
  by-proof-less-eq-nf u [] v v₁ ρ = just not-less-zero  -- could've used refute, but we'll take it
  by-proof-less-eq-nf u [ 1 , [] ] v v₁ ρ = do
    prf ← by-proof-eq-nf 10 u [] v v₁ ρ
    pure (prf ∘ less-one-is-zero)
  by-proof-less-eq-nf u u₁ v v₁ ρ = nothing

  by-proof-less-eq : ∀ a a₁ b b₁ ρ → Maybe (SubExpLess a a₁ ρ → SubExpEq b b₁ ρ)
  by-proof-less-eq a a₁ b b₁ ρ with cancel (normSub a) (normSub a₁)
                                  | cancel (normSub b) (normSub b₁)
                                  | complicateSubLess a a₁ ρ
                                  | simplifySubEq b b₁ ρ
  ... | u , u₁ | v , v₁ | compl | simpl = do
    prf ← by-proof-less-eq-nf u u₁ v v₁ ρ
    pure (simpl ∘ prf ∘ compl)

  by-proof : ∀ hyp goal ρ → Maybe (⟦ hyp ⟧eqn ρ → ⟦ goal ⟧eqn ρ)
  by-proof (a :≡ a₁) (b :≡ b₁) ρ = by-proof-eq a a₁ b b₁ ρ
  by-proof (a :< a₁) (b :≡ b₁) ρ = by-proof-less-eq a a₁ b b₁ ρ
  by-proof (a :< a₁) (b :< b₁) ρ = by-proof-less a a₁ b b₁ ρ
  by-proof (a :≡ a₁) (b :< b₁) ρ = do
    prf ← by-proof-less a (lit 1 ⟨+⟩ a₁) b b₁ ρ
    pure λ eq → prf (diff 0 (cong suc (sym eq)))

by-tactic : Term → Type → TC Term
by-tactic prf g = do
  ensureNoMetas prf
  h ← inferNormalisedType prf
  let t = pi (vArg h) (abs "_" (weaken 1 g))
  just (hyp ∷ goal ∷ [] , Γ) ← termToSubHyps t
    where _ → typeError $ strErr "Invalid goal:" ∷ termErr t ∷ []
  pure $
    applyTerm (safe
      (getProof (quote cantProve) t $
       def (quote by-proof)
           ( vArg (` hyp)
           ∷ vArg (` goal)
           ∷ vArg (quotedEnv Γ)
           ∷ [])) _) (vArg prf ∷ [])

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:
{-# OPTIONS --without-K --safe --erased-cubical --no-import-sorts #-}

module Prelude where

open import Agda.Primitive renaming (Set to Type) public
open import Agda.Builtin.Reflection hiding (Type) renaming (primQNameEquality to _==_) public
open import Reflection using (_>>=_) public

open import Agda.Builtin.String public
open import Agda.Builtin.Sigma public

open import Data.Bool using (Bool; not; true; false; if_then_else_) public
open import Data.List using (List; []; _∷_; map; concat; concatMap; _++_; foldr; zip; length; take) public
open import Data.Maybe using (Maybe; just; nothing) public
open import Data.Fin.Base using (Fin; toℕ) renaming (zero to fz) public
open import Data.Integer.Base using (ℤ; +_; -[1+_]) public
open import Data.Nat.Base using (ℕ; zero; suc; _^_) public
open import Data.Nat.DivMod using (_%_; _mod_) public
open import Data.Product using (_×_; _,_) public
open import Data.Unit using (⊤) public
open import Data.Vec using (Vec; []; _∷_; updateAt) public

open import Function using (id; _∘_; flip) public

open import Definition.Conversion.Soundness public

open import Interval public
open import Note public
open import Pitch using (Pitch; a; b; b♭; c; c♯; d; d♯; e; f; f♯; g; g♯) public
open import Transformation public

open import MidiEvent using (InstrumentNumber-1; maxChannels; MidiTrack) public

open import FarmCanon using () renaming (subject to canonsubject) public
open import FarmFugue using (b1; b2; b3; b4; b5; b6; b7; b8; b9; b10; b11; b12; b13; subject; countersubject; extra) public

ext: agda

max_stars_repo_name: halfaya/Music

max_issues_repo_name: halfaya/Music

max_forks_repo_name: halfaya/Music


text:
------------------------------------------------------------------------------
-- Totality properties respect to ListN
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.ListN-I where

open import FOTC.Base
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.List.PropertiesI
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- The function flatten generates a ListN.
flatten-ListN : ∀ {t} → Tree t → ListN (flatten t)
flatten-ListN tnil = subst ListN (sym flatten-nil) lnnil
flatten-ListN (ttip {i} Ni) =
  subst ListN (sym (flatten-tip i)) (lncons Ni lnnil)
flatten-ListN (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂)
  = subst ListN
          (sym (flatten-node t₁ i t₂))
          (++-ListN (flatten-ListN Tt₁)
                    (flatten-ListN Tt₂))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module FSM where
open import Sec4
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Bool
-- open import Data.Rational
-- open import Data.Integer
-- open import Relation.Nullary.Decidable

data Loc : Set where
  A : Loc
  DONE : Loc

record Values : Set where
  field
    x : ℕ
    δ : ℕ
    k : ℕ

data _Π_ (A B : Set) : Set where
  <_,_> : (a : Loc) → (b : Values) →  A Π B

-- The computation of x in the state
-- The state machine step function
step : (Loc Π Values) → (Loc Π Values)
step < A , b > =
  if (X >= 10)
  then
    < DONE , record { x = X; δ = Values.δ b ; k = Values.k b Data.Nat.+ 1 } >
  else
    < A , record { x = X; δ = Values.δ b ; k = Values.k b Data.Nat.+ 1 } >
 where
 funₓ : ℕ → ℕ → ℕ → ℕ           -- slope = 1 here!
 funₓ x k δ = x Data.Nat.+ δ Data.Nat.* k

 _>=_ : ℕ → ℕ → Bool
 zero >= zero = true
 zero >= suc y = false
 suc x >= zero = false
 suc x >= suc y = x >= y

 _==_ : ℕ → ℕ → Bool
 zero == zero = true
 zero == suc y = false
 suc x == zero = false
 suc x == suc y = x == y

 X : ℕ
 X = funₓ (Values.x b) (Values.k b) (Values.δ b)

step < DONE , b > = < DONE , b > -- Just remain in this state forever

runFSM : (n : ℕ) → (st : (Loc Π Values)) → (Loc Π Values)
runFSM zero st = st
runFSM (suc n) st = runFSM n (step st)

theorem : runFSM 10 (< A , (record { x = zero ; δ = 1 ; k = zero }) >) ≡ < DONE ,
                           record { x = 10 ; δ = 1 ; k = 5 } >
theorem  = refl

-- invariant when in DONE state, X ≥ 10
invariant : (Loc Π Values) → Prop
invariant < A , record { x = x ; δ = δ ; k = k } > = ⊥
invariant < DONE , record { x = x ; δ = δ ; k = k } > =  x ≥ 10

thm : invariant (runFSM 5 (< A , (record { x = zero ; δ = 1 ; k = zero }) >))
thm = s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))))

-- Example of state machine as a relation
data State : Set where
  A : ∀ (n : ℕ) → State
  D : ∀ (n : ℕ) → State

private funₓ : ℕ → ℕ → ℕ → ℕ
        funₓ x δ slope = x Data.Nat.+ δ Data.Nat.* slope

data _↓_ : State → State → Prop where
  S1 : ∀ (n : ℕ) → (n < 10) → (A n) ↓ (A (funₓ n 1 1))
  S2 : ∀ (n : ℕ) → (n ≥ 10) → (A n) ↓ (D n)

data fState : State → Prop where
  F : ∀ (n : ℕ) →  (n ≥ 10) →  fState (D n)

data oState : State → Prop where
  O : oState (A 0)

y : ∀ (n : ℕ) → (p : n < 10) → (A n) ↓ (A (ℕ.suc n))
y .0 (s≤s z≤n) = S1 zero (s≤s z≤n)
y .1 (s≤s (s≤s z≤n)) = S1 (suc zero) (s≤s (s≤s z≤n))
y .2 (s≤s (s≤s (s≤s z≤n))) = S1 (suc (suc zero)) (s≤s (s≤s (s≤s z≤n)))
y .3 (s≤s (s≤s (s≤s (s≤s z≤n)))) = S1 (suc (suc (suc zero))) (s≤s (s≤s (s≤s (s≤s z≤n))))
y .4 (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))) = S1 (suc (suc (suc (suc zero)))) (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))
y .5 (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))) = S1 (suc (suc (suc (suc (suc zero)))))
                                                 (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))
y .6 (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))) = S1 (suc (suc (suc (suc (suc (suc zero))))))
                                                       (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))
y .7 (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))) = S1 (suc (suc (suc (suc (suc (suc (suc zero)))))))
                                                             (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))
y .8 (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))) = S1 (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))
                                                                   (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))))
y .9 (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))))) = S1 (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))
                                                                         (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))))

y1 : ∀ (n : ℕ) → (p : n ≥ 10) → (A n) ↓ (D n)
y1 n p = S2 n p

-- Example of arithexpr as a relation
data aexp : Set where
  ANum : ∀ (n : ℕ) → aexp
  APlus : aexp → aexp → aexp
  AMult : aexp → aexp → aexp

aeval : aexp → ℕ
aeval (ANum n) = n
aeval (APlus a₁ a₂) = (aeval a₁) + (aeval a₂)
aeval (AMult n₁ n₂) = (aeval n₁) * (aeval n₂)

_==_ : ℕ → ℕ → Bool
zero == zero = true
zero == suc y = false
suc x == zero = false
suc x == suc y = x == y

-- compiler optimization
aexp-opt1 : aexp → aexp
aexp-opt1 (ANum n) = ANum n
aexp-opt1 (APlus (ANum n) (ANum n₁)) with (n == 0) Data.Bool.∧ (n₁ == n)
aexp-opt1 (APlus (ANum n) (ANum n₁)) | false = (APlus (ANum n) (ANum n₁))
aexp-opt1 (APlus (ANum n) (ANum n₁)) | true = (ANum 0)
aexp-opt1 (APlus x x₁) = APlus x x₁
aexp-opt1 (AMult (ANum n) (ANum n₁)) with (n == 0) Data.Bool.∨ (n₁ == 0)
aexp-opt1 (AMult (ANum n) (ANum n₁)) | true = ANum 0
aexp-opt1 (AMult (ANum n) (ANum n₁)) | false = (AMult (ANum n) (ANum n₁))
aexp-opt1 (AMult x x₁) = (AMult x x₁)

-- Theorem that the optimization is correct!
thm-opt1 : ∀ (a : aexp) → ∀ (n : ℕ)
           → (aeval a ≡ n)
           → aeval (aexp-opt1 a) ≡ n
thm-opt1 (ANum n) .n refl = refl
thm-opt1 (APlus (ANum zero) (ANum zero)) .0 refl = refl
thm-opt1 (APlus (ANum zero) (ANum (suc n))) .(suc n) refl = refl
thm-opt1 (APlus (ANum (suc n)) (ANum n₁)) .(suc (n + n₁)) refl = refl
thm-opt1 (APlus (ANum n) (APlus b b₁)) .(n + (aeval b + aeval b₁)) refl = refl
thm-opt1 (APlus (ANum n) (AMult b b₁)) .(n + aeval b * aeval b₁) refl = refl
thm-opt1 (APlus (APlus a a₁) b) .(aeval a + aeval a₁ + aeval b) refl = refl
thm-opt1 (APlus (AMult a a₁) b) .(aeval a * aeval a₁ + aeval b) refl = refl
thm-opt1 (AMult (ANum zero) (ANum n₁)) .0 refl = refl
thm-opt1 (AMult (ANum (suc n)) (ANum zero)) .(n * 0) refl = cc n
  where
  cc : ∀ (n : ℕ) → (0 ≡ n * 0)
  cc zero = refl
  cc (suc n) = cc n
thm-opt1 (AMult (ANum (suc n)) (ANum (suc p))) .(suc (p + n * suc p)) refl = refl
thm-opt1 (AMult (ANum n) (APlus b b₁)) .(n * (aeval b + aeval b₁)) refl = refl
thm-opt1 (AMult (ANum n) (AMult b b₁)) .(n * (aeval b * aeval b₁)) refl = refl
thm-opt1 (AMult (APlus a a₁) b) .((aeval a + aeval a₁) * aeval b) refl = refl
thm-opt1 (AMult (AMult a a₁) b) .(aeval a * aeval a₁ * aeval b) refl = refl

-- Now as a relation
data _⇓_ : aexp → ℕ → Set where
  ANumR : ∀ (n : ℕ) → ANum n ⇓ n
  APlusR : ∀ (n₁ n₂ : ℕ) → ∀ (a₁ a₂ : aexp)
           → (a₁ ⇓ n₁) → (a₂ ⇓ n₂)
           → (APlus a₁ a₂) ⇓ (n₁ + n₂)
  AMultR : ∀ (n₁ n₂ : ℕ) → ∀ (a₁ a₂ : aexp)
           → (a₁ ⇓ n₁) → (a₂ ⇓ n₂)
           → (AMult a₁ a₂) ⇓ (n₁ * n₂)

∧-Zero : ∀ (x y : ℕ) → ((x ≡ 0) Sec4.∧ (y ≡ 0)) Sec4.∨ ⊤
∧-Zero zero zero = ora (and refl refl)
∧-Zero zero (suc y) = orb ⋆
∧-Zero (suc x) y = orb ⋆

∨-Zero : ∀ (x y : ℕ) → ((x ≡ 0) Sec4.∨ (y ≡ 0)) Sec4.∨ ⊤
∨-Zero zero _ = ora (ora refl)
∨-Zero (suc x) zero = ora (orb refl)
∨-Zero (suc x) (suc y) = orb ⋆

-- compiler optimization
aexp-opt2 : aexp → aexp
aexp-opt2 (ANum n) = ANum n
aexp-opt2 (APlus (ANum n) (ANum n₁)) with ∧-Zero n n₁
aexp-opt2 (APlus (ANum .0) (ANum .0)) | ora (and refl refl) = ANum zero
aexp-opt2 (APlus (ANum n) (ANum n₁)) | orb _ = (APlus (ANum n) (ANum n₁))
aexp-opt2 (APlus x x₁) = APlus x x₁
aexp-opt2 (AMult (ANum n) (ANum n₁)) with ∨-Zero n n₁
aexp-opt2 (AMult (ANum .0) (ANum n₁)) | ora (ora refl) = ANum 0
aexp-opt2 (AMult (ANum n) (ANum .0)) | ora (orb refl) = ANum 0
aexp-opt2 (AMult (ANum n) (ANum n₁)) | orb x = (AMult (ANum n) (ANum n₁))
aexp-opt2 (AMult x x₁) = (AMult x x₁)

yy : ∀ (n : ℕ) → (n * 0) ≡ 0
yy zero = refl
yy (suc n) = yy n

-- Theorem that the optimization is correct in relations
thm-rel-opt2 : ∀ (a : aexp) → ∀ (p : ℕ) → (a ⇓ p) → ((aexp-opt2 a) ⇓ p)
thm-rel-opt2 (ANum n) p e = e
thm-rel-opt2 (APlus (ANum n) (ANum n₁)) p e with ∧-Zero n n₁
thm-rel-opt2 (APlus (ANum .0) (ANum .0)) .0 (APlusR .0 .0 .(ANum 0) .(ANum 0) (ANumR .0) (ANumR .0)) | ora (and refl refl) = ANumR zero
thm-rel-opt2 (APlus (ANum n) (ANum n₁)) p e | orb x = e
thm-rel-opt2 (APlus (ANum n) (APlus a a₁)) p e = e
thm-rel-opt2 (APlus (ANum n) (AMult a a₁)) p e = e
thm-rel-opt2 (APlus (APlus a a₁) a₂) p e = e
thm-rel-opt2 (APlus (AMult a a₁) a₂) p e = e
thm-rel-opt2 (AMult (ANum n) (ANum n₁)) p e with ∨-Zero n n₁
thm-rel-opt2 (AMult (ANum .0) (ANum n₃)) .0 (AMultR .0 .n₃ .(ANum 0) .(ANum n₃) (ANumR .0) (ANumR .n₃)) | ora (ora refl) = ANumR zero
-- The below is rewrite
thm-rel-opt2 (AMult (ANum n₁) (ANum .0)) .(n₁ * 0) (AMultR .n₁ .0 .(ANum n₁) .(ANum 0) (ANumR .n₁) (ANumR .0)) | ora (orb refl) with (yy n₁)
thm-rel-opt2 (AMult (ANum n₁) (ANum .0)) .(n₁ * 0) (AMultR .n₁ .0 .(ANum n₁) .(ANum 0) (ANumR .n₁) (ANumR .0)) | ora (orb refl) | j with n₁ * 0
thm-rel-opt2 (AMult (ANum n₁) (ANum _)) .(n₁ * _) (AMultR .n₁ _ .(ANum n₁) .(ANum _) (ANumR .n₁) (ANumR _)) | ora (orb refl) | refl | .0 = ANumR zero
thm-rel-opt2 (AMult (ANum n) (ANum n₁)) p e | orb x = e
thm-rel-opt2 (AMult (ANum n) (APlus b b₁)) p e = e
thm-rel-opt2 (AMult (ANum n) (AMult b b₁)) p e = e
thm-rel-opt2 (AMult (APlus a a₁) b) p e = e
thm-rel-opt2 (AMult (AMult a a₁) b) p e = e

th : (APlus (ANum 10) (ANum 10)) ⇓ 20
th = APlusR
       (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))))
       (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))))
       (ANum
        (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))
       (ANum
        (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))
       (ANumR
        (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))
       (ANumR
        (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))

t : ∀ (a : aexp) (p : ℕ) → (aeval a ≡ p) → (a ⇓ p)
t (ANum n) .n refl = ANumR n
t (APlus a a₁) .(aeval a + aeval a₁) refl = APlusR (aeval a) (aeval a₁) a a₁ (t a (aeval a) refl)
                                            (t a₁ (aeval a₁) refl)
t (AMult a a₁) .(aeval a * aeval a₁) refl = AMultR (aeval a) (aeval a₁) a a₁ (t a (aeval a) refl)
                                            (t a₁ (aeval a₁) refl)

tt : ∀ (a : aexp) (n : ℕ) → (a ⇓ n) → (aeval a ≡ n)
tt (ANum n₁) .n₁ (ANumR .n₁) = refl
tt (APlus a a₁) .(n₁ + n₂) (APlusR n₁ n₂ .a .a₁ p p₁) with tt a n₁ p | tt a₁ n₂ p₁
tt (APlus a a₁) .(aeval a + aeval a₁) (APlusR .(aeval a) .(aeval a₁) .a .a₁ p p₁) | refl | refl = refl
tt (AMult a a₁) .(n₁ * n₂) (AMultR n₁ n₂ .a .a₁ p p₁) with tt a n₁ p | tt a₁ n₂ p₁
tt (AMult a a₁) .(aeval a * aeval a₁) (AMultR .(aeval a) .(aeval a₁) .a .a₁ p p₁) | refl | refl = refl


text:
module Issue719 where

  import Common.Size as A
  module M where

  private open module A = M

-- NOT NICE:
-- Duplicate definition of module A. Previous definition of module A
-- at /Users/abel/cover/alfa/Agda2-clean/test/Common/Size.agda:7,15-19
-- when scope checking the declaration
--   open module A = M

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Categories.Functor.Monoidal.Construction.Product where

-- The functors associated with the product A × B of
-- (braided/symmetric) monoidal categories A and B are again
-- (braided/symmetric) monoidal.

open import Level using (Level)
open import Data.Product using (_,_; <_,_>)

open import Categories.Category using (Category)
open import Categories.Category.Product
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Construction.Product
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Monoidal
import Categories.Functor.Monoidal.Braided as BMF
import Categories.Functor.Monoidal.Symmetric as SMF
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MorphismReasoning
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)

private
  variable
    o ℓ e o₁ ℓ₁ e₁ o′₁ ℓ′₁ e′₁ o₂ ℓ₂ e₂ o′₂ ℓ′₂ e′₂ : Level

module _ {D₁ : MonoidalCategory o₁ ℓ₁ e₁} {D₂ : MonoidalCategory o₂ ℓ₂ e₂} where

  open MonoidalCategory using (U)
  private D₁×D₂ = Product-MonoidalCategory D₁ D₂

  -- Pairing for monoidal categories is a monoidal functor

  module _ {C : MonoidalCategory o ℓ e}
           {F : Functor (U C) (U D₁)} {G : Functor (U C) (U D₂)} where

    ※-IsMonoidalFunctor : IsMonoidalFunctor C D₁ F →
                          IsMonoidalFunctor C D₂ G →
                          IsMonoidalFunctor C D₁×D₂ (F ※ G)
    ※-IsMonoidalFunctor FM GM = record
      { ε         = FM.ε , GM.ε
      ; ⊗-homo    = ntHelper (record
        { η       = λ XY → FM.⊗-homo.η XY , GM.⊗-homo.η XY
        ; commute = λ fg → FM.⊗-homo.commute fg , GM.⊗-homo.commute fg
        })
      ; associativity = FM.associativity , GM.associativity
      ; unitaryˡ      = FM.unitaryˡ , GM.unitaryˡ
      ; unitaryʳ      = FM.unitaryʳ , GM.unitaryʳ
      }
      where
        module FM = IsMonoidalFunctor FM
        module GM = IsMonoidalFunctor GM

    ※-IsStrongMonoidalFunctor : IsStrongMonoidalFunctor C D₁ F →
                                IsStrongMonoidalFunctor C D₂ G →
                                IsStrongMonoidalFunctor C D₁×D₂ (F ※ G)
    ※-IsStrongMonoidalFunctor FM GM = record
      { ε         = record
        { from    = FM.ε.from , GM.ε.from
        ; to      = FM.ε.to   , GM.ε.to
        ; iso     = record
          { isoˡ  = FM.ε.isoˡ , GM.ε.isoˡ
          ; isoʳ  = FM.ε.isoʳ , GM.ε.isoʳ
          }
        }
      ; ⊗-homo    = niHelper (record
        { η       = < FM.⊗-homo.⇒.η , GM.⊗-homo.⇒.η >
        ; η⁻¹     = < FM.⊗-homo.⇐.η , GM.⊗-homo.⇐.η >
        ; commute = < FM.⊗-homo.⇒.commute , GM.⊗-homo.⇒.commute >
        ; iso     = λ XY → record
          { isoˡ  = FM.⊗-homo.iso.isoˡ XY , GM.⊗-homo.iso.isoˡ XY
          ; isoʳ  = FM.⊗-homo.iso.isoʳ XY , GM.⊗-homo.iso.isoʳ XY
          }
        })
      ; associativity = FM.associativity , GM.associativity
      ; unitaryˡ      = FM.unitaryˡ , GM.unitaryˡ
      ; unitaryʳ      = FM.unitaryʳ , GM.unitaryʳ
      }
      where
        module FM = IsStrongMonoidalFunctor FM
        module GM = IsStrongMonoidalFunctor GM

  module _ {C : MonoidalCategory o ℓ e} where

    ※-MonoidalFunctor : MonoidalFunctor C D₁ → MonoidalFunctor C D₂ →
                        MonoidalFunctor C D₁×D₂
    ※-MonoidalFunctor FM GM = record
      { isMonoidal = ※-IsMonoidalFunctor (isMonoidal FM) (isMonoidal GM) }
      where open MonoidalFunctor using (isMonoidal)

    ※-StrongMonoidalFunctor : StrongMonoidalFunctor C D₁ →
                              StrongMonoidalFunctor C D₂ →
                              StrongMonoidalFunctor C D₁×D₂
    ※-StrongMonoidalFunctor FM GM = record
      { isStrongMonoidal =
        ※-IsStrongMonoidalFunctor (isStrongMonoidal FM) (isStrongMonoidal GM)
      }
      where open StrongMonoidalFunctor using (isStrongMonoidal)

  -- The projections out of a product of monoidal categories are
  -- monoidal functors

  πˡ-IsStrongMonoidalFunctor : IsStrongMonoidalFunctor D₁×D₂ D₁ πˡ
  πˡ-IsStrongMonoidalFunctor = record
    { ε             = ≅.refl
    ; ⊗-homo        = niHelper (record
      { η           = λ _ → id
      ; η⁻¹         = λ _ → id
      ; commute     = λ _ → id-comm-sym
      ; iso         = λ _ → record { isoˡ = identity² ; isoʳ = identity² }
      })
    ; associativity = begin
        associator.from ∘ id ∘ id ⊗₁ id   ≈⟨ refl⟩∘⟨ elimʳ ⊗.identity ⟩
        associator.from ∘ id              ≈⟨ id-comm ⟩
        id ∘ associator.from              ≈⟨ pushˡ (introʳ ⊗.identity) ⟩
        id ∘ id ⊗₁ id ∘ associator.from   ∎
    ; unitaryˡ      = begin
        unitorˡ.from ∘ id ∘ id ⊗₁ id   ≈⟨ refl⟩∘⟨ elimʳ ⊗.identity ⟩
        unitorˡ.from ∘ id              ≈⟨ identityʳ ⟩
        unitorˡ.from                   ∎
    ; unitaryʳ      = begin
        unitorʳ.from ∘ id ∘ id ⊗₁ id   ≈⟨ refl⟩∘⟨ elimʳ ⊗.identity ⟩
        unitorʳ.from ∘ id              ≈⟨ identityʳ ⟩
        unitorʳ.from                   ∎
    }
    where
      open MonoidalCategory D₁
      open HomReasoning
      open Morphism (U D₁) using (module ≅)
      open MorphismReasoning (U D₁)

  πˡ-IsMonoidalFunctor : IsMonoidalFunctor D₁×D₂ D₁ πˡ
  πˡ-IsMonoidalFunctor =
    IsStrongMonoidalFunctor.isMonoidal πˡ-IsStrongMonoidalFunctor

  πˡ-StrongMonoidalFunctor : StrongMonoidalFunctor D₁×D₂ D₁
  πˡ-StrongMonoidalFunctor = record
    { isStrongMonoidal = πˡ-IsStrongMonoidalFunctor }

  πˡ-MonoidalFunctor : MonoidalFunctor D₁×D₂ D₁
  πˡ-MonoidalFunctor =
    StrongMonoidalFunctor.monoidalFunctor πˡ-StrongMonoidalFunctor

  πʳ-IsStrongMonoidalFunctor : IsStrongMonoidalFunctor D₁×D₂ D₂ πʳ
  πʳ-IsStrongMonoidalFunctor = record
    { ε             = ≅.refl
    ; ⊗-homo        = niHelper (record
      { η           = λ _ → id
      ; η⁻¹         = λ _ → id
      ; commute     = λ _ → id-comm-sym
      ; iso         = λ _ → record { isoˡ = identity² ; isoʳ = identity² }
      })
    ; associativity = begin
        associator.from ∘ id ∘ id ⊗₁ id   ≈⟨ refl⟩∘⟨ elimʳ ⊗.identity ⟩
        associator.from ∘ id              ≈⟨ id-comm ⟩
        id ∘ associator.from              ≈⟨ pushˡ (introʳ ⊗.identity) ⟩
        id ∘ id ⊗₁ id ∘ associator.from   ∎
    ; unitaryˡ      = begin
        unitorˡ.from ∘ id ∘ id ⊗₁ id   ≈⟨ refl⟩∘⟨ elimʳ ⊗.identity ⟩
        unitorˡ.from ∘ id              ≈⟨ identityʳ ⟩
        unitorˡ.from                   ∎
    ; unitaryʳ      = begin
        unitorʳ.from ∘ id ∘ id ⊗₁ id   ≈⟨ refl⟩∘⟨ elimʳ ⊗.identity ⟩
        unitorʳ.from ∘ id              ≈⟨ identityʳ ⟩
        unitorʳ.from                   ∎
    }
    where
      open MonoidalCategory D₂
      open HomReasoning
      open Morphism (U D₂) using (module ≅)
      open MorphismReasoning (U D₂)

  πʳ-IsMonoidalFunctor : IsMonoidalFunctor D₁×D₂ D₂ πʳ
  πʳ-IsMonoidalFunctor =
    IsStrongMonoidalFunctor.isMonoidal πʳ-IsStrongMonoidalFunctor

  πʳ-StrongMonoidalFunctor : StrongMonoidalFunctor D₁×D₂ D₂
  πʳ-StrongMonoidalFunctor = record
    { isStrongMonoidal = πʳ-IsStrongMonoidalFunctor }

  πʳ-MonoidalFunctor : MonoidalFunctor D₁×D₂ D₂
  πʳ-MonoidalFunctor =
    StrongMonoidalFunctor.monoidalFunctor πʳ-StrongMonoidalFunctor

  -- The cartesian product of two monoidal functors is again a
  -- monoidal functor

  module _ {C₁ : MonoidalCategory o′₁ ℓ′₁ e′₁}
           {C₂ : MonoidalCategory o′₂ ℓ′₂ e′₂}
           {F : Functor (U C₁) (U D₁)} {G : Functor (U C₂) (U D₂)} where
    private C₁×C₂ = Product-MonoidalCategory C₁ C₂

    ⁂-IsMonoidalFunctor : IsMonoidalFunctor C₁ D₁ F →
                          IsMonoidalFunctor C₂ D₂ G →
                          IsMonoidalFunctor C₁×C₂ D₁×D₂ (F ⁂ G)
    ⁂-IsMonoidalFunctor FM GM = record
      { ε         = FM.ε , GM.ε
      ; ⊗-homo    = ntHelper (record
        { η       = λ{ ((X₁ , X₂) , (Y₁ , Y₂)) →
                    FM.⊗-homo.η (X₁ , Y₁) , GM.⊗-homo.η (X₂ , Y₂) }
        ; commute = λ{ ((f₁ , f₂) , (g₁ , g₂)) →
                    FM.⊗-homo.commute (f₁ , g₁) , GM.⊗-homo.commute (f₂ , g₂) }
        })
      ; associativity = FM.associativity , GM.associativity
      ; unitaryˡ      = FM.unitaryˡ , GM.unitaryˡ
      ; unitaryʳ      = FM.unitaryʳ , GM.unitaryʳ
      }
      where
        module FM = IsMonoidalFunctor FM
        module GM = IsMonoidalFunctor GM

    ⁂-IsStrongMonoidalFunctor : IsStrongMonoidalFunctor C₁ D₁ F →
                                IsStrongMonoidalFunctor C₂ D₂ G →
                                IsStrongMonoidalFunctor C₁×C₂ D₁×D₂ (F ⁂ G)
    ⁂-IsStrongMonoidalFunctor FM GM = record
      { ε         = record
        { from    = FM.ε.from , GM.ε.from
        ; to      = FM.ε.to   , GM.ε.to
        ; iso     = record
          { isoˡ  = FM.ε.isoˡ , GM.ε.isoˡ
          ; isoʳ  = FM.ε.isoʳ , GM.ε.isoʳ
          }
        }
      ; ⊗-homo    = niHelper (record
        { η       = λ{ ((X₁ , X₂) , (Y₁ , Y₂)) →
                    FM.⊗-homo.⇒.η (X₁ , Y₁) , GM.⊗-homo.⇒.η (X₂ , Y₂) }
        ; η⁻¹     = λ{ ((X₁ , X₂) , (Y₁ , Y₂)) →
                    FM.⊗-homo.⇐.η (X₁ , Y₁) , GM.⊗-homo.⇐.η (X₂ , Y₂) }
        ; commute = λ{ ((f₁ , f₂) , (g₁ , g₂)) →
                    FM.⊗-homo.⇒.commute (f₁ , g₁) ,
                    GM.⊗-homo.⇒.commute (f₂ , g₂) }
        ; iso     = λ{ ((X₁ , X₂) , (Y₁ , Y₂)) → record
          { isoˡ  = FM.⊗-homo.iso.isoˡ (X₁ , Y₁) , GM.⊗-homo.iso.isoˡ (X₂ , Y₂)
          ; isoʳ  = FM.⊗-homo.iso.isoʳ (X₁ , Y₁) , GM.⊗-homo.iso.isoʳ (X₂ , Y₂)
          } }
        })
      ; associativity = FM.associativity , GM.associativity
      ; unitaryˡ      = FM.unitaryˡ , GM.unitaryˡ
      ; unitaryʳ      = FM.unitaryʳ , GM.unitaryʳ
      }
      where
        module FM = IsStrongMonoidalFunctor FM
        module GM = IsStrongMonoidalFunctor GM

  module _ {C₁ : MonoidalCategory o′₁ ℓ′₁ e′₁}
           {C₂ : MonoidalCategory o′₂ ℓ′₂ e′₂} where
    private C₁×C₂ = Product-MonoidalCategory C₁ C₂

    ⁂-MonoidalFunctor : MonoidalFunctor C₁ D₁ → MonoidalFunctor C₂ D₂ →
                        MonoidalFunctor C₁×C₂ D₁×D₂
    ⁂-MonoidalFunctor FM GM = record
      { isMonoidal = ⁂-IsMonoidalFunctor (isMonoidal FM) (isMonoidal GM) }
      where open MonoidalFunctor using (isMonoidal)

    ⁂-StrongMonoidalFunctor : StrongMonoidalFunctor C₁ D₁ →
                              StrongMonoidalFunctor C₂ D₂ →
                              StrongMonoidalFunctor C₁×C₂ D₁×D₂
    ⁂-StrongMonoidalFunctor FM GM = record
      { isStrongMonoidal =
        ⁂-IsStrongMonoidalFunctor (isStrongMonoidal FM) (isStrongMonoidal GM)
      }
      where open StrongMonoidalFunctor using (isStrongMonoidal)

module _ {D₁ : BraidedMonoidalCategory o₁ ℓ₁ e₁}
         {D₂ : BraidedMonoidalCategory o₂ ℓ₂ e₂} where

  open BMF
  open BraidedMonoidalCategory using (U)
  private D₁×D₂ = Product-BraidedMonoidalCategory D₁ D₂

  -- Pairing for braided monoidal categories is a braided monoidal
  -- functor

  module _ {C : BraidedMonoidalCategory o ℓ e}
           {F : Functor (U C) (U D₁)} {G : Functor (U C) (U D₂)} where

    ※-IsBraidedMonoidalFunctor : Lax.IsBraidedMonoidalFunctor C D₁ F →
                                 Lax.IsBraidedMonoidalFunctor C D₂ G →
                                 Lax.IsBraidedMonoidalFunctor C D₁×D₂ (F ※ G)
    ※-IsBraidedMonoidalFunctor FB GB = record
      { isMonoidal      = ※-IsMonoidalFunctor (isMonoidal FB) (isMonoidal GB)
      ; braiding-compat = (braiding-compat FB) , (braiding-compat GB)
      }
      where open Lax.IsBraidedMonoidalFunctor

    ※-IsStrongBraidedMonoidalFunctor :
      Strong.IsBraidedMonoidalFunctor C D₁ F →
      Strong.IsBraidedMonoidalFunctor C D₂ G →
      Strong.IsBraidedMonoidalFunctor C D₁×D₂ (F ※ G)
    ※-IsStrongBraidedMonoidalFunctor FB GB = record
      { isStrongMonoidal =
        ※-IsStrongMonoidalFunctor (isStrongMonoidal FB) (isStrongMonoidal GB)
      ; braiding-compat  = (braiding-compat FB) , (braiding-compat GB)
      }
      where open Strong.IsBraidedMonoidalFunctor

  module _ {C : BraidedMonoidalCategory o ℓ e} where

    ※-BraidedMonoidalFunctor : Lax.BraidedMonoidalFunctor C D₁ →
                               Lax.BraidedMonoidalFunctor C D₂ →
                               Lax.BraidedMonoidalFunctor C D₁×D₂
    ※-BraidedMonoidalFunctor FB GB = record
      { isBraidedMonoidal =
        ※-IsBraidedMonoidalFunctor (isBraidedMonoidal FB) (isBraidedMonoidal GB)
      }
      where open Lax.BraidedMonoidalFunctor

    ※-StrongBraidedMonoidalFunctor : Strong.BraidedMonoidalFunctor C D₁ →
                                     Strong.BraidedMonoidalFunctor C D₂ →
                                     Strong.BraidedMonoidalFunctor C D₁×D₂
    ※-StrongBraidedMonoidalFunctor FB GB = record
      { isBraidedMonoidal =
        ※-IsStrongBraidedMonoidalFunctor (isBraidedMonoidal FB)
                                         (isBraidedMonoidal GB)
      }
      where open Strong.BraidedMonoidalFunctor

  -- The projections out of a product of braided monoidal categories are
  -- braided monoidal functors

  πˡ-IsStrongBraidedMonoidalFunctor : Strong.IsBraidedMonoidalFunctor D₁×D₂ D₁ πˡ
  πˡ-IsStrongBraidedMonoidalFunctor = record
    { isStrongMonoidal = πˡ-IsStrongMonoidalFunctor
    ; braiding-compat  = MorphismReasoning.id-comm  (U D₁)
    }

  πˡ-IsBraidedMonoidalFunctor : Lax.IsBraidedMonoidalFunctor D₁×D₂ D₁ πˡ
  πˡ-IsBraidedMonoidalFunctor =
    Strong.IsBraidedMonoidalFunctor.isLaxBraidedMonoidal
      πˡ-IsStrongBraidedMonoidalFunctor

  πˡ-StrongBraidedMonoidalFunctor : Strong.BraidedMonoidalFunctor D₁×D₂ D₁
  πˡ-StrongBraidedMonoidalFunctor = record
    { isBraidedMonoidal = πˡ-IsStrongBraidedMonoidalFunctor }

  πˡ-BraidedMonoidalFunctor : Lax.BraidedMonoidalFunctor D₁×D₂ D₁
  πˡ-BraidedMonoidalFunctor =
    Strong.BraidedMonoidalFunctor.laxBraidedMonoidalFunctor
      πˡ-StrongBraidedMonoidalFunctor

  πʳ-IsStrongBraidedMonoidalFunctor : Strong.IsBraidedMonoidalFunctor D₁×D₂ D₂ πʳ
  πʳ-IsStrongBraidedMonoidalFunctor = record
    { isStrongMonoidal = πʳ-IsStrongMonoidalFunctor
    ; braiding-compat  = MorphismReasoning.id-comm  (U D₂)
    }

  πʳ-IsBraidedMonoidalFunctor : Lax.IsBraidedMonoidalFunctor D₁×D₂ D₂ πʳ
  πʳ-IsBraidedMonoidalFunctor =
    Strong.IsBraidedMonoidalFunctor.isLaxBraidedMonoidal
      πʳ-IsStrongBraidedMonoidalFunctor

  πʳ-StrongBraidedMonoidalFunctor : Strong.BraidedMonoidalFunctor D₁×D₂ D₂
  πʳ-StrongBraidedMonoidalFunctor = record
    { isBraidedMonoidal = πʳ-IsStrongBraidedMonoidalFunctor }

  πʳ-BraidedMonoidalFunctor : Lax.BraidedMonoidalFunctor D₁×D₂ D₂
  πʳ-BraidedMonoidalFunctor =
    Strong.BraidedMonoidalFunctor.laxBraidedMonoidalFunctor
      πʳ-StrongBraidedMonoidalFunctor

  -- The cartesian product of two braided monoidal functors is again a
  -- braided monoidal functor

  module _ {C₁ : BraidedMonoidalCategory o′₁ ℓ′₁ e′₁}
           {C₂ : BraidedMonoidalCategory o′₂ ℓ′₂ e′₂}
           {F : Functor (U C₁) (U D₁)} {G : Functor (U C₂) (U D₂)} where
    private C₁×C₂ = Product-BraidedMonoidalCategory C₁ C₂

    ⁂-IsBraidedMonoidalFunctor : Lax.IsBraidedMonoidalFunctor C₁ D₁ F →
                                 Lax.IsBraidedMonoidalFunctor C₂ D₂ G →
                                 Lax.IsBraidedMonoidalFunctor C₁×C₂ D₁×D₂ (F ⁂ G)
    ⁂-IsBraidedMonoidalFunctor FB GB = record
      { isMonoidal      = ⁂-IsMonoidalFunctor (isMonoidal FB) (isMonoidal GB)
      ; braiding-compat = braiding-compat FB , braiding-compat GB
      }
      where open Lax.IsBraidedMonoidalFunctor

    ⁂-IsStrongBraidedMonoidalFunctor :
      Strong.IsBraidedMonoidalFunctor C₁ D₁ F →
      Strong.IsBraidedMonoidalFunctor C₂ D₂ G →
      Strong.IsBraidedMonoidalFunctor C₁×C₂ D₁×D₂ (F ⁂ G)
    ⁂-IsStrongBraidedMonoidalFunctor FB GB = record
      { isStrongMonoidal =
        ⁂-IsStrongMonoidalFunctor (isStrongMonoidal FB) (isStrongMonoidal GB)
      ; braiding-compat  = braiding-compat FB , braiding-compat GB
      }
      where open Strong.IsBraidedMonoidalFunctor

  module _ {C₁ : BraidedMonoidalCategory o′₁ ℓ′₁ e′₁}
           {C₂ : BraidedMonoidalCategory o′₂ ℓ′₂ e′₂} where
    private C₁×C₂ = Product-BraidedMonoidalCategory C₁ C₂

    ⁂-BraidedMonoidalFunctor : Lax.BraidedMonoidalFunctor C₁ D₁ →
                               Lax.BraidedMonoidalFunctor C₂ D₂ →
                               Lax.BraidedMonoidalFunctor C₁×C₂ D₁×D₂
    ⁂-BraidedMonoidalFunctor FB GB = record
      { isBraidedMonoidal =
        ⁂-IsBraidedMonoidalFunctor (isBraidedMonoidal FB) (isBraidedMonoidal GB)
      }
      where open Lax.BraidedMonoidalFunctor

    ⁂-StrongBraidedMonoidalFunctor : Strong.BraidedMonoidalFunctor C₁ D₁ →
                                     Strong.BraidedMonoidalFunctor C₂ D₂ →
                                     Strong.BraidedMonoidalFunctor C₁×C₂ D₁×D₂
    ⁂-StrongBraidedMonoidalFunctor FB GB = record
      { isBraidedMonoidal =
        ⁂-IsStrongBraidedMonoidalFunctor (isBraidedMonoidal FB)
                                         (isBraidedMonoidal GB)
      }
      where open Strong.BraidedMonoidalFunctor

module _ {D₁ : SymmetricMonoidalCategory o₁ ℓ₁ e₁}
         {D₂ : SymmetricMonoidalCategory o₂ ℓ₂ e₂} where

  open SMF
  open SymmetricMonoidalCategory using (U)
    renaming (braidedMonoidalCategory to B)
  private D₁×D₂ = Product-SymmetricMonoidalCategory D₁ D₂

  -- Pairing for symmetric monoidal categories is a symmetric monoidal
  -- functor

  module _ {C : SymmetricMonoidalCategory o ℓ e} where

    ※-SymmetricMonoidalFunctor : Lax.SymmetricMonoidalFunctor C D₁ →
                                 Lax.SymmetricMonoidalFunctor C D₂ →
                                 Lax.SymmetricMonoidalFunctor C D₁×D₂
    ※-SymmetricMonoidalFunctor FB GB = record
      { isBraidedMonoidal =
        ※-IsBraidedMonoidalFunctor (isBraidedMonoidal FB) (isBraidedMonoidal GB)
      }
      where open Lax.SymmetricMonoidalFunctor

    ※-StrongSymmetricMonoidalFunctor : Strong.SymmetricMonoidalFunctor C D₁ →
                                       Strong.SymmetricMonoidalFunctor C D₂ →
                                       Strong.SymmetricMonoidalFunctor C D₁×D₂
    ※-StrongSymmetricMonoidalFunctor FB GB = record
      { isBraidedMonoidal =
        ※-IsStrongBraidedMonoidalFunctor (isBraidedMonoidal FB)
                                         (isBraidedMonoidal GB)
      }
      where open Strong.SymmetricMonoidalFunctor

  -- The projections out of a product of symmetric monoidal categories are
  -- symmetric monoidal functors

  πˡ-StrongSymmetricMonoidalFunctor : Strong.SymmetricMonoidalFunctor D₁×D₂ D₁
  πˡ-StrongSymmetricMonoidalFunctor = record
    { isBraidedMonoidal = πˡ-IsStrongBraidedMonoidalFunctor {D₂ = B D₂} }

  πˡ-SymmetricMonoidalFunctor : Lax.SymmetricMonoidalFunctor D₁×D₂ D₁
  πˡ-SymmetricMonoidalFunctor =
    Strong.SymmetricMonoidalFunctor.laxSymmetricMonoidalFunctor
      πˡ-StrongSymmetricMonoidalFunctor

  πʳ-StrongSymmetricMonoidalFunctor : Strong.SymmetricMonoidalFunctor D₁×D₂ D₂
  πʳ-StrongSymmetricMonoidalFunctor = record
    { isBraidedMonoidal = πʳ-IsStrongBraidedMonoidalFunctor {D₁ = B D₁} }

  πʳ-SymmetricMonoidalFunctor : Lax.SymmetricMonoidalFunctor D₁×D₂ D₂
  πʳ-SymmetricMonoidalFunctor =
    Strong.SymmetricMonoidalFunctor.laxSymmetricMonoidalFunctor
      πʳ-StrongSymmetricMonoidalFunctor

  -- The cartesian product of two symmetric monoidal functors is again a
  -- symmetric monoidal functor

  module _ {C₁ : SymmetricMonoidalCategory o′₁ ℓ′₁ e′₁}
           {C₂ : SymmetricMonoidalCategory o′₂ ℓ′₂ e′₂} where
    private C₁×C₂ = Product-SymmetricMonoidalCategory C₁ C₂

    ⁂-SymmetricMonoidalFunctor : Lax.SymmetricMonoidalFunctor C₁ D₁ →
                                 Lax.SymmetricMonoidalFunctor C₂ D₂ →
                                 Lax.SymmetricMonoidalFunctor C₁×C₂ D₁×D₂
    ⁂-SymmetricMonoidalFunctor FB GB = record
      { isBraidedMonoidal =
        ⁂-IsBraidedMonoidalFunctor (isBraidedMonoidal FB) (isBraidedMonoidal GB)
      }
      where open Lax.SymmetricMonoidalFunctor

    ⁂-StrongSymmetricMonoidalFunctor : Strong.SymmetricMonoidalFunctor C₁ D₁ →
                                       Strong.SymmetricMonoidalFunctor C₂ D₂ →
                                       Strong.SymmetricMonoidalFunctor C₁×C₂ D₁×D₂
    ⁂-StrongSymmetricMonoidalFunctor FB GB = record
      { isBraidedMonoidal =
        ⁂-IsStrongBraidedMonoidalFunctor (isBraidedMonoidal FB)
                                         (isBraidedMonoidal GB)
      }
      where open Strong.SymmetricMonoidalFunctor

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Tuple where

import Level
import Data.List as List
open import Data.List hiding (_++_; [_]; _∷ʳ_)
open import Data.Fin

open import Relation.Binary.PropositionalEquality hiding ([_])

infixr 5 _∷_

data Tuple {a} : List (Set a) → Set a where
  [] : Tuple []
  _∷_ : ∀ {A As} → A → Tuple As → Tuple (A ∷ As)

[_] : ∀ {a} {A : Set a} → A → Tuple (A ∷ [])
[ x ] = x ∷ []

_++_ : ∀ {a} {xs ys : List (Set a)}
     → Tuple xs → Tuple ys → Tuple (xs List.++ ys)
_++_ {xs = []} [] ys = ys
_++_ {xs = _ ∷ _} (x ∷ xs) ys = x ∷ (xs ++ ys)

_∷ʳ_ : ∀ {a} {x : Set a} {xs : List (Set a)}
     → Tuple xs → x → Tuple (xs List.∷ʳ x)
_∷ʳ_ xs x = xs ++ [ x ]

private
  listLookup : ∀ {a} {A : Set a} (xs : List A) → (n : Fin (length xs)) → A
  listLookup [] ()
  listLookup (x ∷ xs) zero = x
  listLookup (x ∷ xs) (suc n) = listLookup xs n

lookup : ∀ {a} {xs : List (Set a)}
       → (n : Fin (length xs)) → Tuple xs → listLookup xs n
lookup {xs = []} () []
lookup {xs = _ ∷ _} zero (x ∷ xs) = x
lookup {xs = _ ∷ _} (suc n) (x ∷ xs) = lookup n xs

unfoldToFunc : ∀ {a} → List (Set a) → Set a → Set a
unfoldToFunc [] B = B
unfoldToFunc (A ∷ As) B = A → unfoldToFunc As B

apply : {Xs : List Set} {A : Set} → unfoldToFunc Xs A → Tuple Xs → A
apply {[]} f [] = f
apply {_ ∷ _} f (x ∷ xs) = apply (f x) xs

list-proof : ∀ {a} {A : Set a} (xs : List A) → xs ≡ (xs List.++ [])
list-proof [] = refl
list-proof (x ∷ xs) = cong (_∷_ x) (list-proof xs)

list-proof₁ : ∀ {a} {A : Set a} (xs ys zs : List A)
            → (xs List.++ ys) List.++ zs ≡ xs List.++ (ys List.++ zs)
list-proof₁ [] ys zs = refl
list-proof₁ (x ∷ xs) ys zs = cong (_∷_ x) (list-proof₁ xs ys zs)

curry : ∀ {a} (xs : List (Set a)) → unfoldToFunc xs (Tuple xs)
curry xs = curry' [] xs []
  where curry' : ∀ {a} (xs ys : List (Set a)) → Tuple xs
               → unfoldToFunc ys (Tuple (xs List.++ ys))
        curry' xs [] tpl = subst Tuple (list-proof xs) tpl
        curry' xs (y ∷ ys) tpl x₁ =
          subst (λ x → unfoldToFunc ys (Tuple x))
                (list-proof₁ xs List.[ y ] ys)
                (curry' (xs List.∷ʳ y) ys (tpl ∷ʳ x₁))

proof₁ : ∀ {a} (As : List (Set a)) {B : Set a}
       → (Tuple As → B) → unfoldToFunc As B
proof₁ [] f = f []
proof₁ (A ∷ As) f x = proof₁ As (λ xs → f (x ∷ xs))

proof₂ : ∀ {a} (As : List (Set a)) {B : Set a}
       → unfoldToFunc As B → Tuple As → B
proof₂ [] f [] = f
proof₂ (A ∷ As) f (x ∷ xs) = proof₂ As (f x) xs

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
module builtinInModule where

module Str where

  postulate S : Set
  {-# BUILTIN STRING S #-}
  primitive primStringAppend : S → S → S

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Categories.Functor hiding (id)

-- Also defines the category of cocones "over a Functor F"

module Categories.Category.Construction.Cocones
  {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

open Category C

private
  variable
    X : Obj

open HomReasoning
open Functor F
open import Data.Product
open import Relation.Binary using (Rel; IsEquivalence; Setoid)
import Categories.Morphism as Mor
import Categories.Morphism.IsoEquiv as IsoEquiv
open import Categories.Diagram.Cocone F public

open Mor C
open IsoEquiv C
open import Categories.Morphism.Reasoning C
open Cocone
open Coapex
open Cocone⇒

Cocones : Category _ _ _
Cocones = record
  { Obj       = Cocone
  ; _⇒_       = Cocone⇒
  ; _≈_       = λ f g → arr f ≈ arr g
  ; id        = record { arr = id ; commute = identityˡ }
  ; _∘_       = λ {A B C} f g → record
    { arr     = arr f ∘ arr g
    ; commute = λ {X} → begin
      (arr f ∘ arr g) ∘ ψ A X ≈⟨ pullʳ (commute g) ⟩
      arr f ∘ ψ B X           ≈⟨ commute f ⟩
      ψ C X                   ∎
    }
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = ∘-resp-≈
  }

module Cocones = Category Cocones

private
  variable
    K K′ : Cocone
  module CM = Mor Cocones
  module CI = IsoEquiv Cocones

open CM using () renaming (_≅_ to _⇔_)
open CI using () renaming (_≃_ to _↮_)

cocone-resp-iso : ∀ (κ : Cocone) → Cocone.N κ ≅ X → Σ[ κ′ ∈ Cocone ] κ ⇔ κ′
cocone-resp-iso {X = X} κ κ≅X = record
  { coapex = record
    { ψ       = λ Y → from ∘ Cocone.ψ κ Y
    ; commute = λ f → pullʳ (Cocone.commute κ f)
    }
  } , record
  { from = record
    { arr     = from
    ; commute = refl
    }
  ; to   = record
    { arr     = to
    ; commute = cancelˡ isoˡ
    }
  ; iso  = record
    { isoˡ    = isoˡ
    ; isoʳ    = isoʳ
    }
  }
  where open _≅_ κ≅X
        open Cocone
        open Coapex

iso-cocone⇒iso-coapex : K ⇔ K′ → N K ≅ N K′
iso-cocone⇒iso-coapex K⇔K′ = record
  { from = arr from
  ; to   = arr to
  ; iso  = record
    { isoˡ = isoˡ
    ; isoʳ = isoʳ
    }
  }
  where open _⇔_ K⇔K′

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2015-08-26
{-# OPTIONS --rewriting #-} -- Should give error

open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE refl #-}


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

open import M-types.Base.Core
open import M-types.Base.Sum
open import M-types.Base.Prod

module M-types.Base.Eq where
    infix 4 _≡_
    data _≡_ {X : Ty ℓ} : X → X → Ty ℓ where
        refl : {x : X} → x ≡ x
    open _≡_ public

    infix 10 _⁻¹
    _⁻¹ : {X : Ty ℓ} {x₀ x₁ : X} →
        x₀ ≡ x₁ → x₁ ≡ x₀
    refl ⁻¹ = refl

    infixr 9 _·_
    _·_ : {X : Ty ℓ} {x₀ x₁ x₂ : X} →
        x₀ ≡ x₁ → x₁ ≡ x₂ → x₀ ≡ x₂
    refl · refl = refl

    ·-neutr₀ : {X : Ty ℓ} {x₀ x₁ : X} →
        ∏[ p ∈ x₀ ≡ x₁ ] refl · p ≡ p
    ·-neutr₀ refl = refl

    ·-neutr₁ : {X : Ty ℓ} {x₀ x₁ : X} →
        ∏[ p ∈ x₀ ≡ x₁ ] p · refl ≡ p
    ·-neutr₁ refl = refl

    infix 1 begin_
    begin_ : {X : Ty ℓ} {x₀ x₁ : X} →
        (x₀ ≡ x₁) → (x₀ ≡ x₁)
    begin p = p

    infixr 2 _≡⟨_⟩_
    _≡⟨_⟩_ : {X : Ty ℓ₀} {x₁ x₂ : X} →
        ∏[ x₀ ∈ X ] ((x₀ ≡ x₁) → (x₁ ≡ x₂) → (x₀ ≡ x₂))
    x₀ ≡⟨ p₀ ⟩ p₁ = p₀ · p₁

    infix 3 _∎
    _∎ : {X : Ty ℓ} →
        ∏[ x ∈ X ] x ≡ x
    x ∎ = refl

    tra : {X : Ty ℓ} {x₀ x₁ : X} →
        ∏[ Y ∈ (X → Ty ℓ₁) ] (x₀ ≡ x₁ → (Y x₀ → Y x₁))
    tra f refl = id

    tra-con : {X : Ty ℓ₀} {x₀ x₁ x₂ : X} →
        ∏[ Y ∈ (X → Ty ℓ₁) ] ∏[ p₀ ∈ x₀ ≡ x₁ ] ∏[ p₁ ∈ x₁ ≡ x₂ ]
        (tra Y p₁) ∘ (tra Y p₀) ≡ tra Y (p₀ · p₁)
    tra-con Y refl refl = refl

    ap : {X : Ty ℓ₀} {Y : Ty ℓ₁} {x₀ x₁ : X} →
        ∏[ f ∈ (X → Y) ] ((x₀ ≡ x₁) → (f x₀ ≡ f x₁))
    ap f refl = refl

    ap-inv : {X : Ty ℓ₀} {Y : Ty ℓ₁} {x₀ x₁ : X} →
        ∏[ f ∈ (X → Y) ] ∏[ p ∈ x₀ ≡ x₁ ] (ap f p)⁻¹ ≡ ap f (p ⁻¹)
    ap-inv f refl = refl

    apd : {X : Ty ℓ₀} {Y : X → Ty ℓ₁} {x₀ x₁ : X} →
        ∏[ f ∈ (∏ X Y) ] ∏[ p ∈ x₀ ≡ x₁ ] tra Y p (f x₀) ≡ f x₁
    apd f refl = refl

    ≡-pair : {X : Ty ℓ₀} {Y : X → Ty ℓ₁} {w₀ w₁ : ∑ X Y} →
        (∑[ p ∈ pr₀ w₀ ≡ pr₀ w₁ ] (tra Y p (pr₁ w₀) ≡ pr₁ w₁)) → (w₀ ≡ w₁)
    ≡-pair {ℓ₀} {ℓ₁} {X} {Y} {w} {w} (refl , refl) = refl

    ≡-apply : {X : Ty ℓ₀} {Y : X → Ty ℓ₁} {f₀ f₁ : ∏ X Y} →
        (f₀ ≡ f₁) → (∏[ x ∈ X ] (f₀ x ≡ f₁ x))
    ≡-apply refl = λ x → refl

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
module Issue3545 where

open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Common.IO

createElem : Nat → Set
createElem n = Nat

{-# NOINLINE createElem #-}

{-# COMPILE JS createElem = function (x0) {
    return x0;
} #-}

-- WAS: silently accepted
-- WANT: `createElem` is going to be erased; don't do that!

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

{-# COMPILE GHC map = \ _ _ _ _ -> Prelude.map #-}

-- `map` however is not erased so this should not raise a warning.

value : List Set
value = map (λ n → createElem n) (1 ∷ 1 ∷ [])


text:
open import Prelude hiding (id; Bool; _∷_; [])

module Examples.CompleteResolution where

data TC : Set where
  tc-int : TC
  tc-bool : TC

_tc≟_ : (a b : TC) → Dec (a ≡ b)
tc-int tc≟ tc-int = yes refl
tc-int tc≟ tc-bool = no (λ ())
tc-bool tc≟ tc-int = no (λ ())
tc-bool tc≟ tc-bool = yes refl

open import Implicits.Syntax TC _tc≟_
open import Implicits.WellTyped TC _tc≟_
open import Implicits.Substitutions TC _tc≟_
open import Implicits.Syntax.Type.Unification TC _tc≟_
open import Implicits.Resolution.Finite.Resolution TC _tc≟_
open import Implicits.Resolution.Finite.Algorithm TC _tc≟_
open import Data.Maybe
open import Data.List
open import Category.Monad.Partiality

Bool : ∀ {n} → Type n
Bool = simpl (tc tc-bool)

Int : ∀ {n} → Type n
Int = simpl (tc tc-int)

module Ex₁ where

  Δ : ICtx zero
  Δ = Bool ∷ Int ∷ []

  -- resolves directly using a value from the implicit context
  r = resolve Δ Int

  p : is-just r ≡ true
  p = refl

module Ex₂ where

  Δ : ICtx zero
  Δ = Bool ∷ (Bool ⇒ Int) ∷ []

  -- resolves using implicit application
  r = resolve Δ Int

  p : is-just r ≡ true
  p = refl

module Ex₃ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' (Bool ⇒ (simpl (tvar zero)))) ∷ []

  -- resolves using polymorphic implicit application
  r = resolve Δ Int

  p : is-just r ≡ true
  p = refl

module Ex₅ where

  -- The following context would not resolved Int in Oliveira's deterministic calculus.
  -- Demonstratint that partial resolution is more powerful for terminating contexts.
  Δ : ICtx zero
  Δ = (Bool ⇒ Int) ∷ Int ∷ []

  r = resolve Δ Int

  p : is-just r ≡ true
  p = refl

module Ex₆ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' (Bool ⇒ (simpl (tvar zero)))) ∷ []

  -- resolves rule types
  r = resolve Δ (Bool ⇒ Int)

  p : is-just r ≡ true
  p = refl

module Ex₇ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' (Bool ⇒ (simpl (tvar zero)))) ∷ []

  q : Type zero
  q = (∀' (Bool ⇒ (simpl (tvar zero))))

  -- Resolves polymorphic types.
  -- Note that it doesn't resolve to the rule in the context directly.
  -- Instead, it will apply r-tabs and r-iabs, to obtain resolve Δ' ⊢ᵣ (∀' (tvar zero))
  r = resolve Δ q

  p : is-just r ≡ true
  p = refl

module Ex₈ where

  Δ : ICtx zero
  Δ = Bool ∷ (∀' ((simpl (tvar zero)) ⇒ (simpl (tvar zero)))) ∷ []

  -- infinite derivation exists: fails divergence checking
  r = resolve Δ Int

  p : is-just r ≡ false
  p = refl

module Ex₉ where

  a⇒consta : Type zero
  a⇒consta = (∀' ((simpl (tvar zero)) ⇒ (∀' (simpl (simpl (tvar zero) →' (simpl (tvar (suc zero))))))))

  Δ : ICtx zero
  Δ = Bool ∷ a⇒consta ∷ []

  const-bool : Type zero
  const-bool = (∀' (simpl ((simpl (tvar zero)) →' Bool)))

  r = resolve Δ const-bool

  p : is-just r ≡ true
  p = refl

module Ex₁₀ where

  -- similar to Ex₉ but for this particular example we have that for the rule part
  -- || ρ₁ || ≮ || ρ₂ || such that Oliveira's ⊢term predicate on ρ₁ ⇒ ρ₂ fails
  a⇒∀a : Type zero
  a⇒∀a = (∀' ((simpl (tvar zero)) ⇒ (∀' (simpl (tvar (suc zero))))))

  Δ : ICtx zero
  Δ = Bool ∷ a⇒∀a ∷ []

  r = resolve Δ (∀' Bool)

  p : is-just r ≡ true
  p = refl


text:
module Section1 where

-- 1. Introduction
-- ===============
--
-- 1.1. Outline of the formalisation
-- ---------------------------------
--
-- -   We formalize terms-in-context, `Γ ⊢ t ∷ A`, as a calculus of proof trees, `Γ ⊢ A`, for
--     implicational logic, i.e., term `t` is seen as a proof tree that derives `A` from the assumptions
--     contained in `Γ`.  A notion of equivalence of terms-in-context (including, e.g., β-reduction
--     and η-conversion) is then defined with a conversion relation `_≅_` on these proof trees.
--
-- -   We give a Kripke model with an ordered set of worlds and define when a proposition `A` is
--     true for a world `w` in the model, `w ⊩ A`.  We also define an extensional equality between
--     objects in the model.
--
-- -   We define an interpreter `⟦_⟧` that maps a proof tree in the theory to its semantics in the
--     Kripke model.  According to the Curry-Howard correspondence of programs to proofs
--     and types to propositions, the type of the interpreter expresses soundness of the theory of
--     proof trees with respect to the Kripke model.  Consequently, the interpreter can be seen
--     as a constructive soundness proof.
--
-- -   We also define an inversion function, `reify`, which returns a proof tre corresponding to
--     a given semantic object, yielding—again by the Curry-Howard isomorphism—a
--     completeness proof.
--
--     The inversion function is based on the principle of normalization by evaluation [3].
--     Obviously, for proof trees `M` and `N` with the same semantics, inversion yields the same proof
--     tree `reify ⟦ M ⟧ = reify ⟦ N ⟧`.  Consequently, we define a normalization function, `nf`, as
--     the composition of the interpreter and the inversion function.  We prove that if `M` is a proof
--     tree, then `M ≅ nf M`; together with the soundness result, this yields a decision algorithm
--     for convertibility.  We further show that `nf` returns a proof term in long η-normal form.
--
-- -   We prove that the convertibility relation on proof trees is sound and complete.  The proof
--     of soundness, i.e., convertible proof trees have the same semantics, is straightforward by
--     induction on the structure of the trees.  The completeness proof, i.e., if `⟦ M ⟧` and `⟦ N ⟧` are
--     equal, then `M` and `N` are convertible, uses the fact that `reify ⟦ M ⟧` is exactly the same as
--     `reify ⟦ N ⟧`, and since `M ≅ nf M ≡ reify ⟦ M ⟧` and vice versa for `N`, we get that `M ≅ N`.
--
-- -   We define a calculus of simply typed ƛterms, a typed convertibility relation on the terms,
--     and a deterministic reduction, `_⇓_`.  We also define an erasure function on proof trees that
--     maps a proof tree `M` into a well-typed term `M ⁻`.  For every well-typed term there is at
--     least one proof tree that erases to this term; for defining the semantics of well-typed terms
--     through that of proof trees, it suffices to show that all proof trees that erase to the same
--     well-typed term have the same semantics.
--
-- -   Because we know that convertible proof trees have the same semantics, it remains to
--     show that all proof trees that erase to a given well-typed term are convertible.  We use an
--     argument due to Streicher [19]: we first prove that if `nf M ⁻` and `nf N ⁻` are the same,
--     then `M ≅ N`.  Secondly, we prove that if a proof tree `M` erases to a well-typed term `t`,
--     then `t ⇓ nf M ⁻`.  Now, if two proof trees `M` and `N` erase to the same well-typed term
--     `t`, then `t ⇓ nf M ⁻` and `t ⇓ nf N ⁻`.  Since the reduction is deterministic we have that
--     `nf M ⁻` and `nf N ⁻` are the same, and hence `M ≅ N`.
--
-- -   We prove that the convertibility relation on proof trees is sound and complete, and give
--     a decision algorithm for checking convertibility of two well-typed terms.
--
-- (…)

open import Agda.Builtin.FromString public
  using (IsString ; fromString)

open import Data.Bool public
  using (Bool ; T ; true ; false ; not)
  renaming (_∧_ to and)

open import Data.Empty public
  using (⊥)
  renaming (⊥-elim to elim⊥)

open import Data.Product public
  using (Σ ; _,_ ; _×_ ; proj₁ ; proj₂)

open import Data.Unit public
  using (⊤ ; tt)

import Data.String as Str
open Str
  using (String)

open import Function public
  using (_∘_ ; case_of_ ; flip ; id)

open import Relation.Binary.PropositionalEquality public
  using (_≡_ ; _≢_ ; refl ; cong ; subst ; sym ; trans)
  renaming (cong₂ to cong²)

open import Relation.Nullary public
  using (¬_ ; Dec ; yes ; no)

import Relation.Nullary.Decidable as Decidable
open Decidable using (⌊_⌋) public

open import Relation.Nullary.Negation public
  renaming (contradiction to _↯_)

module _ where
  data Name : Set where
    name : String → Name

  module _ where
    inj-name : ∀ {s s′} → name s ≡ name s′ → s ≡ s′
    inj-name refl = refl

    _≟_ : (x x′ : Name) → Dec (x ≡ x′)
    name s ≟ name s′ = Decidable.map′ (cong name) inj-name (s Str.≟ s′)

    _≠_ : Name → Name → Bool
    x ≠ x′ = not ⌊ x ≟ x′ ⌋

  instance
    str-Name : IsString Name
    str-Name = record
      { Constraint = λ s → ⊤
      ; fromString = λ s → name s
      }

module _ where
  record Raiseable
      {World : Set}
      (_⊩◌  : World → Set)
      {_⊒_   : World → World → Set} : Set₁ where
    field
      ↑⟨_⟩  : ∀ {w w′} → w′ ⊒ w → w ⊩◌ → w′ ⊩◌
  open Raiseable {{…}} public

  record Lowerable
      {World : Set}
      (◌⊩_  : World → Set)
      {_⊒_   : World → World → Set} : Set₁ where
    field
      ↓⟨_⟩  : ∀ {w w′} → w′ ⊒ w → ◌⊩ w′ → ◌⊩ w
  open Lowerable {{…}} public

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
module Dissect where

  import Functor
  import Sets
  import Isomorphism

  open Sets
  open Functor
  open Functor.Semantics
  open Functor.Recursive

  infixr 40 _+₂_
  infixr 60 _×₂_

  ∇ : U -> U₂
  ∇ (K A) = K₂ [0]
  ∇ Id	  = K₂ [1]
  ∇ (F + G) = ∇ F +₂ ∇ G
  ∇ (F × G) = ∇ F ×₂ ↗ G  +₂  ↖ F ×₂ ∇ G

  diagonal : U₂ -> U
  diagonal (K₂ A) = K A
  diagonal (↖ F)  = F
  diagonal (↗ F)  = F
  diagonal (F +₂ G) = diagonal F + diagonal G
  diagonal (F ×₂ G) = diagonal F × diagonal G

  module Derivative where

    import Derivative as D

    ∂ : U -> U
    ∂ F = diagonal (∇ F)

    open Isomorphism

    same : (F : U)(X : Set) -> ⟦ ∂ F ⟧ X ≅ ⟦ D.∂ F ⟧ X
    same (K A)	 X = refl-≅ [0]
    same Id	 X = refl-≅ [1]
    same (F + G) X = iso[+] (same F X) (same G X)
    same (F × G) X = iso[+] (iso[×] (same F X) (refl-≅ _))
			    (iso[×] (refl-≅ _) (same G X))

  Stack : (F : U) -> Set -> Set -> Set
  Stack F C J = List (⟦ ∇ F ⟧₂ C J)

  NextJoker : U -> Set -> Set -> Set
  NextJoker F C J = J  [×]  ⟦ ∇ F ⟧₂ C J  [+]  ⟦ F ⟧ C

  mutual
    into : (F : U){C J : Set} -> ⟦ F ⟧ J -> NextJoker F C J
    into (K A)	  a	     = inr a
    into Id	  x	     = inl < x , <> >
    into (F + G) (inl f)     = (id <×> inl <+> inl) (into F f)
    into (F + G) (inr g)     = (id <×> inr <+> inr) (into G g)
    into (F × G) < fj , gj > = tryL F G (into F fj) gj

    next : (F : U){C J : Set} -> ⟦ ∇ F ⟧₂ C J -> C -> NextJoker F C J
    next (K A)	 ()		   _
    next Id	 <>		   c = inr c
    next (F + G) (inl f')	   c = (id <×> inl <+> inl) (next F f' c)
    next (F + G) (inr g')	   c = (id <×> inr <+> inr) (next G g' c)
    next (F × G) (inl < f' , gj >) c = tryL F G (next F f' c) gj
    next (F × G) (inr < fc , g' >) c = tryR F G fc (next G g' c)

    tryL : (F G : U){C J : Set} ->
	   NextJoker F C J -> ⟦ G ⟧ J -> NextJoker (F × G) C J
    tryL F G (inl < j , f' >) gj = inl < j , inl < f' , gj > >
    tryL F G (inr fc)         gj = tryR F G fc (into G gj)

    tryR : (F G : U){C J : Set} ->
	   ⟦ F ⟧ C -> NextJoker G C J -> NextJoker (F × G) C J
    tryR F G fc (inl < j , g' >) = inl < j , inr < fc , g' > >
    tryR F G fc (inr gc)	 = inr < fc , gc >

  map : (F : U){C J : Set} -> (J -> C) -> ⟦ F ⟧ J -> ⟦ F ⟧ C
  map F φ f = iter (into F f) where
    iter : NextJoker F _ _ -> ⟦ F ⟧ _
    iter (inl < j , d >) = iter (next F d (φ j))
    iter (inr f)	 = f

  fold : (F : U){T : Set} -> (⟦ F ⟧ T -> T) -> μ F -> T
  fold F {T} φ r = inward r [] where
    mutual
      inward : μ F -> Stack F T (μ F) -> T
      inward (inn f) γ = onward (into F f) γ

      outward : T -> Stack F T (μ F) -> T
      outward t []	  = t
      outward t (f' :: γ) = onward (next F f' t) γ

      onward : NextJoker F T (μ F) -> Stack F T (μ F) -> T
      onward (inl < r , f' >) γ = inward r (f' :: γ)
      onward (inr t)	      γ = outward (φ t) γ

  -- can we make a non-tail recursive fold?
  -- of course, nothing could be simpler: (not structurally recursive though)
  fold' : (F : U){T : Set} -> (⟦ F ⟧ T -> T) -> μ F -> T
  fold' F φ = φ ∘ map F (fold' F φ) ∘ out

  -- Fold operators
  Φ : (F : U) -> Set -> Set
  Φ (K A)   T = A -> T
  Φ Id	    T = T -> T
  Φ (F + G) T = Φ F T [×] Φ G T
  Φ (F × G) T = (T -> T -> T) [×] (Φ F T [×] Φ G T)

  mkφ : (F : U){T : Set} -> Φ F T -> ⟦ F ⟧ T -> T
  mkφ (K A)   f			    a	      = f a
  mkφ Id      f			    t	      = f t
  mkφ (F + G) < φf , φg >	    (inl f)   = mkφ F φf f
  mkφ (F + G) < φf , φg >	    (inr g)   = mkφ G φg g
  mkφ (F × G) < _○_ , < φf , φg > > < f , g > = mkφ F φf f ○ mkφ G φg g

max_stars_repo_name: asr/agda-kanso


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

module Math.NumberTheory.Summation.Nat where

-- agda-stdlib
open import Algebra
open import Data.Nat.Properties

-- agda-misc
open import Math.NumberTheory.Summation.Generic

-- DO NOT change this line
open MonoidSummation (Semiring.+-monoid *-+-semiring) public


text:
{-

Theory about path split equivalences.
They are convenient to construct localization HITs as in
(the "modalities paper")
https://arxiv.org/abs/1706.07526

- there are construction from and to equivalences ([pathSplitToEquiv] , [equivToPathSplit])
- the structure of a path split equivalence is actually a proposition ([isPropIsPathSplitEquiv])

The module starts with a couple of general facts about equivalences:

- if f is an equivalence then (cong f) is an equivalence ([equivCong])
- if f is an equivalence then pre- and postcomposition with f are equivalences ([preCompEquiv], [postCompEquiv])

(those are not in 'Equiv.agda' because they need Univalence.agda (which imports Equiv.agda))
-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.PathSplitEquiv where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism

open import Cubical.Foundations.Equiv.Properties

record isPathSplitEquiv {ℓ ℓ'} {A : Type  ℓ} {B : Type ℓ'} (f : A → B) : Type (ℓ-max ℓ ℓ') where
  field
    s : B → A
    sec : section f s
    secCong : (x y : A) → Σ[ s' ∈ (f(x) ≡ f(y) → x ≡ y) ] section (cong f) s'

PathSplitEquiv : ∀ {ℓ ℓ'} (A : Type  ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
PathSplitEquiv A B = Σ[ f ∈ (A → B) ] isPathSplitEquiv f

open isPathSplitEquiv

idIsPathSplitEquiv : ∀ {ℓ} {A : Type ℓ} → isPathSplitEquiv (λ (x : A) → x)
s idIsPathSplitEquiv x = x
sec idIsPathSplitEquiv x = refl
secCong idIsPathSplitEquiv = λ x y → (λ p → p) , λ p _ → p

module _ {ℓ} {A B : Type ℓ} where
  toIsEquiv : (f : A → B) → isPathSplitEquiv f → isEquiv f
  toIsEquiv f record { s = s ; sec = sec ; secCong = secCong } =
    (isoToEquiv (iso f s sec (λ x → (secCong (s (f x)) x).fst (sec (f x))))) .snd

  sectionOfEquiv' : (f : A → B) → isEquiv f → B → A
  sectionOfEquiv' f record { equiv-proof = all-fibers-contractible } x =
    all-fibers-contractible x .fst .fst

  isSec : (f : A → B) → (pf : isEquiv f) → section f (sectionOfEquiv' f pf)
  isSec f record { equiv-proof = all-fibers-contractible } x =
    all-fibers-contractible x .fst .snd

  sectionOfEquiv : (f : A → B) → isEquiv f → Σ (B → A) (section f)
  sectionOfEquiv f e = sectionOfEquiv' f e , isSec f e

module _ {ℓ} {A B : Type ℓ} where
  abstract
    fromIsEquiv : (f : A → B) → isEquiv f → isPathSplitEquiv f
    s (fromIsEquiv f pf) = sectionOfEquiv' f pf
    sec (fromIsEquiv f pf) = isSec f pf
    secCong (fromIsEquiv f pf) x y = sectionOfEquiv cong-f eq-cong
            where
            cong-f : x ≡ y → f x ≡ f y
            cong-f = λ (p : x ≡ y) → cong f p
            eq-cong : isEquiv cong-f
            eq-cong = isEquivCong (f , pf)

  pathSplitToEquiv : PathSplitEquiv A B → A ≃ B
  fst (pathSplitToEquiv (f , _)) = f
  snd (pathSplitToEquiv (_ , e)) = toIsEquiv _ e

  equivToPathSplit : A ≃ B → PathSplitEquiv A B
  fst (equivToPathSplit (f , _)) = f
  snd (equivToPathSplit (_ , e)) = fromIsEquiv _ e

  equivHasUniqueSection : (f : A → B)
    → isEquiv f → isContr (Σ (B → A) (section f))
  equivHasUniqueSection f eq = helper'
    where
      idB = λ (x : B) → x
      abstract
        helper : isContr (fiber (λ (φ : B → A) → f ∘ φ) idB)
        helper = (equiv-proof (snd (postCompEquiv (f , eq)))) idB
      helper' : isContr (Σ[ φ ∈ (B → A) ] ((x : B) → f (φ x) ≡ x))
      fst helper' = (φ , λ x i → η i x)
        where φ = fst (fst helper)
              η : f ∘ φ ≡ idB
              η = snd (fst helper)
      (snd helper') y i = (fst (η i) , λ b j → snd (η i) j b)
        where η = (snd helper) (fst y , λ i b → snd y b i)

{-
  PathSplitEquiv is a proposition and the type
  of path split equivs is equivalent to the type of equivalences
-}
isPropIsPathSplitEquiv : ∀ {ℓ} {A B : Type ℓ} (f : A → B)
     → isProp (isPathSplitEquiv f)
isPropIsPathSplitEquiv {_} {A} {B} f
  record { s = φ ; sec = sec-φ ; secCong = secCong-φ }
  record { s = ψ ; sec = sec-ψ ; secCong = secCong-ψ } i
  =
  record {
    s = fst (sectionsAreEqual i) ;
    sec = snd (sectionsAreEqual i) ;
    secCong = λ x y → congSectionsAreEqual x y (secCong-φ x y) (secCong-ψ x y) i
  }
  where
    φ' = record { s = φ ; sec = sec-φ ; secCong = secCong-φ }
    ψ' = record { s = ψ ; sec = sec-ψ ; secCong = secCong-ψ }
    sectionsAreEqual : (φ , sec-φ) ≡ (ψ , sec-ψ)
    sectionsAreEqual = (sym (contraction (φ , sec-φ))) ∙ (contraction  (ψ , sec-ψ))
      where contraction = snd (equivHasUniqueSection f (toIsEquiv f φ'))
    congSectionsAreEqual : (x y : A) (l u : Σ (f(x) ≡ f(y) → x ≡ y) (section (cong f))) → l ≡ u
    congSectionsAreEqual x y l u = (sym (contraction l)) ∙ (contraction u)
      where contraction = snd (equivHasUniqueSection
                                 (λ (p : x ≡ y) → cong f p)
                                 (isEquivCong (pathSplitToEquiv (f , φ'))))

module _ {ℓ} {A B : Type ℓ} where
  isEquivIsPathSplitToIsEquiv : (f : A → B) → isEquiv (fromIsEquiv f)
  isEquivIsPathSplitToIsEquiv f =
    isoToIsEquiv
      (iso (fromIsEquiv f) (toIsEquiv f) (λ b → isPropIsPathSplitEquiv f _ _) (λ a → isPropIsEquiv f _ _ ))

  isEquivPathSplitToEquiv : isEquiv (pathSplitToEquiv {A = A} {B = B})
  isEquivPathSplitToEquiv =
    isoToIsEquiv
      (iso pathSplitToEquiv equivToPathSplit
        (λ {(f , e) i → (f , isPropIsEquiv f (toIsEquiv f (fromIsEquiv f e)) e i)})
        (λ {(f , e) i → (f , isPropIsPathSplitEquiv f (fromIsEquiv f (toIsEquiv f e)) e i)}))

  equivPathSplitToEquiv : (PathSplitEquiv A B) ≃ (A ≃ B)
  equivPathSplitToEquiv = (pathSplitToEquiv , isEquivPathSplitToEquiv)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Type.Size.Countable where

import      Data.Either as Type
import      Data.Either.Equiv as Either
import      Data.Tuple as Type
import      Data.Tuple.Equiv as Tuple
import      Lvl
open import Logic
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Sequence
open import Numeral.Natural.Sequence.Proofs
open import Relator.Equals.Proofs.Equivalence
open import Structure.Setoid
open import Type
open import Type.Size
open import Type.Size.Proofs

private variable ℓ ℓ₁ ℓ₂ ℓₑ : Lvl.Level

-- Definition of a countable type
Countable : (T : Type{ℓ}) → ⦃ _ : Equiv{ℓₑ}(T) ⦄ → Stmt
Countable(T) = (ℕ ≽ T)

-- Definition of a countably infinite type
CountablyInfinite : (T : Type{ℓ}) → ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → Stmt
CountablyInfinite(T) ⦃ equiv ⦄ = _≍_ ℕ ⦃ [≡]-equiv ⦄ T

private variable A : Type{ℓ₁}
private variable B : Type{ℓ₂}
private variable ⦃ equiv-A ⦄ : Equiv{ℓₑ}(A)
private variable ⦃ equiv-B ⦄ : Equiv{ℓₑ}(B)
private variable ⦃ equiv-A‖B ⦄ : Equiv{ℓₑ}(A Type.‖ B)
private variable ⦃ equiv-A⨯B ⦄ : Equiv{ℓₑ}(A Type.⨯ B)

module Countable where
  -- TODO: Do something similar to CountablyInfinite here

  -- _+_ : Countable (A) ⦃ equiv-A ⦄ → Countable(B) ⦃ equiv-B ⦄ → Countable(A ‖ B) ⦃ equiv-A‖B ⦄
  -- [∃]-intro a ⦃ intro pa ⦄ + [∃]-intro b ⦃ intro pb ⦄ = [∃]-intro (Left ∘ a) ⦃ intro (\{y} → [∃]-intro ([∃]-witness pa) ⦃ {!!} ⦄) ⦄
  -- [∃]-intro (Left ∘ a) ⦃ intro (\{y} → [∃]-intro ([∃]-witness pa) ⦃ {!!} ⦄) ⦄

  -- _⋅_ : Countable (A) ⦃ equiv-A ⦄ → Countable(B) ⦃ equiv-B ⦄ → Countable(A ⨯ B) ⦃ equiv-A⨯B ⦄

module CountablyInfinite where
  index : ∀{ℓ} → (T : Type{ℓ}) → ⦃ equiv-T : Equiv{ℓₑ}(T) ⦄ → ⦃ size : CountablyInfinite(T) ⦄ → (ℕ → T)
  index(_) ⦃ size = size ⦄ = [∃]-witness size

  indexing : ∀{ℓ} → (T : Type{ℓ}) → ⦃ equiv-T : Equiv{ℓₑ}(T) ⦄ → ⦃ size : CountablyInfinite(T) ⦄ → (T → ℕ)
  indexing(T) ⦃ size = size ⦄ = [∃]-witness([≍]-symmetry-raw ⦃ [≡]-equiv ⦄ size ⦃ [≡]-to-function ⦄)

  _+_ : ⦃ ext : Either.Extensionality ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (equiv-A‖B) ⦄ → CountablyInfinite(A) ⦃ equiv-A ⦄ → CountablyInfinite(B) ⦃ equiv-B ⦄ → CountablyInfinite(A Type.‖ B) ⦃ equiv-A‖B ⦄
  [∃]-intro a + [∃]-intro b = [∃]-intro (interleave a b)

  _⨯_ : ⦃ ext : Tuple.Extensionality ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (equiv-A⨯B) ⦄ → CountablyInfinite(A) ⦃ equiv-A ⦄ → CountablyInfinite(B) ⦃ equiv-B ⦄ → CountablyInfinite(A Type.⨯ B) ⦃ equiv-A⨯B ⦄
  [∃]-intro a ⨯ [∃]-intro b = [∃]-intro (pair a 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:
module regular-concat where

open import Level renaming ( suc to Suc ; zero to Zero )
open import Data.List
open import Data.Nat hiding ( _≟_ )
open import Data.Fin hiding ( _+_ )
open import Data.Empty
open import Data.Unit
open import Data.Product
-- open import Data.Maybe
open import  Relation.Nullary
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import logic
open import nat
open import automaton
open import regular-language

open import nfa
open import sbconst2
open import finiteSet
open import finiteSetUtil

open Automaton
open FiniteSet

open RegularLanguage

Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ
Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend }
   module Concat-NFA where
       δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
       δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
       δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\
           (equal? (afin B) qb (δ (automaton B) (astart B) i) )
       δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁
       δnfa _ i _ = false
       nend : states A ∨ states B → Bool
       nend (case2 q) = aend (automaton B) q
       nend (case1 q) = aend (automaton A) q /\ aend (automaton B) (astart B) -- empty B case

Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q

CNFA-exist : {Σ : Set} → (A B : RegularLanguage Σ ) → (states A ∨ states B → Bool) → Bool
CNFA-exist A B qs = exists (fin-∨ (afin A) (afin B)) qs

M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
M-Concat {Σ} A B = record {
       states = states A ∨ states B → Bool
     ; astart = Concat-NFA-start A B
     ; afin = finf
     ; automaton = subset-construction (CNFA-exist A B) (Concat-NFA A B)
   } where
       fin : FiniteSet (states A ∨ states B )
       fin = fin-∨ (afin A) (afin B)
       finf : FiniteSet (states A ∨ states B → Bool )
       finf = fin→ fin

-- closed-in-concat' :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
-- closed-in-concat' {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
--     closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
--     closed-in-concat→ = {!!}
--     closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
--     closed-in-concat← = {!!}

record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
    field
        sp0 : List Σ
        sp1 : List Σ
        sp-concat : sp0 ++ sp1 ≡ x
        prop0 : A sp0 ≡ true
        prop1 : B sp1 ≡ true

open Split

list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
list-empty++ [] (x ∷ y) ()
list-empty++ (x ∷ x₁) y ()

open _∧_

open import Relation.Binary.PropositionalEquality hiding ( [_] )

c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
   → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
   → split (λ t1 → A (h ∷ t1)) B t ≡ true
c-split-lemma {Σ} A B h t eq p = sym ( begin
      true
  ≡⟨  sym eq  ⟩
      split A B (h ∷ t )
  ≡⟨⟩
      A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
  ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩
      false \/ split (λ t1 → A (h ∷ t1)) B t
  ≡⟨ bool-or-1 refl ⟩
      split (λ t1 → A (h ∷ t1)) B t
  ∎ ) where
     open ≡-Reasoning
     lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false
     lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A )
     lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B )

split→AB :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true
split→AB {Σ} A B [] eq | yes eqa | yes eqb =
    record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
split→AB {Σ} A B (h ∷ t ) eq  | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }

AB→split :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
AB→split {Σ} A B [] [] eqa eqb = begin
       split A B []
     ≡⟨⟩
       A [] /\ B []
     ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
      true
     ∎  where open ≡-Reasoning
AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin
      split A B (h ∷ y )
     ≡⟨⟩
      A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
     ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
      true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
     ≡⟨⟩
      true \/ split (λ t1 → A (h ∷ t1)) B y
     ≡⟨⟩
      true
     ∎  where open ≡-Reasoning
AB→split {Σ} A B (h ∷ t) y eqa eqb = begin
       split A B ((h ∷ t) ++ y)
     ≡⟨⟩
       A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
     ≡⟨ cong ( λ k →  A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
       A [] /\ B (h ∷ t ++ y) \/ true
     ≡⟨ bool-or-3 ⟩
      true
     ∎  where open ≡-Reasoning

open NAutomaton
open import Data.List.Properties

closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
    finab = (fin-∨ (afin A) (afin B))
    NFA = (Concat-NFA A B)
    abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B
    abmove (case1 q) h = case1 (δ (automaton A) q h)
    abmove (case2 q) h = case2 (δ (automaton B) q h)
    lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true
    lemma-nmove-ab (case1 q) h = equal?-refl (afin A)
    lemma-nmove-ab (case2 q) h = equal?-refl (afin B)
    nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
       exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
    nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )
    nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) )
    acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true )
        → Naccept NFA (CNFA-exist A B) nq z  ≡ true
    acceptB [] q nq nqt fb = lemma8 where
        lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true
        lemma8 = found finab (case2 q) ( bool-and-tt nqt fb )
    acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA (CNFA-exist A B) nq h) (nmove (case2 q) nq nq=q h) fb

    acceptA : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
        → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true )
        → Naccept NFA (CNFA-exist A B) nq (y ++ z)  ≡ true
    acceptA [] [] q nq nqt fa fb = found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb ))
    acceptA [] (h ∷ z)  q nq nq=q fa fb = acceptB z nextb (Nmoves NFA (CNFA-exist A B) nq h) lemma70 fb where
         nextb : states B
         nextb = δ (automaton B) (astart B) h
         lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true
         lemma70 = found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) ))
    acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA (CNFA-exist A B) nq h) (nmove (case1 q) nq nq=q h)  fa fb

    acceptAB : Split (contain A) (contain B) x
        → Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x  ≡ true
    acceptAB S = subst ( λ k → Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) )

    closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
    closed-in-concat→ concat with split→AB (contain A) (contain B) x concat
    ... | S = begin
          accept  (subset-construction (CNFA-exist A B) (Concat-NFA A B) ) (Concat-NFA-start A B ) x
       ≡⟨ ≡-Bool-func (subset-construction-lemma←  (CNFA-exist A B)  NFA (equal? finab (case1 (astart A))) x )
          (subset-construction-lemma→  (CNFA-exist A B)  NFA (equal? finab (case1 (astart A))) x ) ⟩
          Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x
       ≡⟨ acceptAB S ⟩
         true
       ∎  where open ≡-Reasoning

    open Found

    ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set
    ab-case (case1 qa') qa x = qa'  ≡ qa
    ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x  ≡ true )

    contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA (CNFA-exist A B) nq x ≡ true )
          → (qa : states A )  → (  (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
          → split (accept (automaton A) qa ) (contain B) x ≡ true
    contain-A [] nq fn qa cond with found← finab fn  -- at this stage, A and B must be satisfied with [] (ab-case cond forces it)
    ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
    ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S)
    ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S)))
    contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
    ... | yes eq = bool-or-41 eq  -- found A ++ B all end
    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion
       --- prove ab-case condition (we haven't checked but case2 b may happen)
       lemma11 :  (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
       lemma11 (case1 qa')  ex with found← finab ex
       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
       ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A)  ( bool-∧→tt-1 (found-p S) ))  -- continued A case
       ... | case2 qb | record { eq = refl } | nb with  bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false
       ... | ()
       lemma11 (case2 qb)  ex with found← finab ex
       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
       lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb = contra-position lemma13 nb where -- continued B case should fail
           lemma13 :  accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true
           lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb
       lemma11 (case2 qb)  ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S)
       ... | eee = contra-position lemma12 ne where -- starting B case should fail
           lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
           lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )

    lemma10 : Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where
       lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x
       lemma15 q nq=t with equal→refl finab nq=t
       ... | refl = refl

    closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
    closed-in-concat← C with subset-construction-lemma← (CNFA-exist A B) NFA (equal? finab (case1 (astart A))) x C
    ... | CC = lemma10 CC

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
open import Categories
open import Monads

module Monads.CatofAdj.InitAdj {a b}{C : Cat {a}{b} }(M : Monad C) where

open import Library
open import Functors
open import Naturals hiding (Iso; module Iso)
open import Adjunctions
open import Monads.CatofAdj M
open import Categories.Initial
open import Monads.Kleisli M
open import Monads.Kleisli.Functors M
open import Monads.Kleisli.Adjunction M
open import Adjunctions.Adj2Mon

open Cat
open Fun
open Monad M
open NatT
open Adj

lemX : R KlAdj ○ L KlAdj ≅ TFun M
lemX = FunctorEq _ _ refl refl

KlObj : Obj CatofAdj
KlObj = record {
  D   = Kl;
  adj = KlAdj;
  law = lemX;
  ηlaw = refl;
  bindlaw = λ{X}{Y}{f} →
    cong bind
         (stripsubst (Hom C X) f (fcong Y (cong OMap (sym lemX))))}

open ObjAdj
open import Isomorphism
open Iso

lemZ : {D : Cat {a}{b}}{F G G' : Fun C D} →
       G ≅ G' → {α : NatT F G}{β : NatT F G'} → α ≅ β →
       ∀ {X} → cmp α {X} ≅ cmp β {X}
lemZ refl refl = refl

lemZ' : {D : Cat {a}{b}}{F F' G G' : Fun C D} →
        F ≅ F' → G ≅ G' → {α : NatT F G}{β : NatT F' G'} → α ≅ β →
        ∀ {X} → cmp α {X} ≅ cmp β {X}
lemZ' refl refl refl = refl

lemfid : {D : Cat {a}{b}}(L : Fun C D)(R : Fun D C)(T : Fun C C)
  (p : T ≅ R ○ L) (η : ∀ {X} → Hom C X (OMap T X))
  (right : {X : Obj C}{Y : Obj D} → Hom C X (OMap R Y) → Hom D (OMap L X) Y) →
  (left : {X : Obj C}{Y : Obj D} → Hom D (OMap L X) Y → Hom C X (OMap R Y)) →
  (q :  {X : Obj C}{Y : Obj D}(f : Hom D (OMap L X) Y) → right (left f) ≅ f) →
  (r : {X : Obj C} → left (iden D {OMap L X}) ≅ η {X}) →
  {X : Obj C} →
    right (subst (Hom C X) (fcong X (cong OMap p)) η)
    ≅
    iden D {OMap L X}
lemfid {D = D} L R .(R ○ L) refl η right left q r {X} =
  trans (cong right (sym r)) (q (iden D))

lemfcomp : {D : Cat {a}{b}}(L : Fun C D)(R : Fun D C)(T : Fun C C)
  (p : T ≅ R ○ L)
  (bind : ∀{X Y} → Hom C X (OMap T Y) → Hom C (OMap T X) (OMap T Y)) →
  (right : {X : Obj C} {Y : Obj D} → Hom C X (OMap R Y) → Hom D (OMap L X) Y) →
  (q : {X Y : Obj C} {f : Hom C X (OMap T Y)} →
       HMap R (right (subst (Hom C X) (fcong Y (cong OMap p)) f)) ≅ bind f) →
  (r : {X X' : Obj C}{Y Y' : Obj D}
       (f : Hom C X' X)(g : Hom D Y Y')
       (h : Hom C X (OMap R Y)) →
       right (comp C (HMap R g) (comp C h f))
       ≅
       comp D g (comp D (right h) (HMap L f))) →
  ∀{X Y Z : Obj C} {f : Hom C Y (OMap T Z)} {g : Hom C X (OMap T Y)} →
    right (subst (Hom C X) (fcong Z (cong OMap p)) (comp C (bind f) g))
    ≅
    comp D (right (subst (Hom C Y) (fcong Z (cong OMap p)) f))
           (right (subst (Hom C X) (fcong Y (cong OMap p)) g))
lemfcomp {D = D} L R .(R ○ L) refl bind right q r {X}{Y}{Z}{f}{g} =
  trans (cong₂ (λ f g → right (comp C f g)) (sym (q {f = f})) (sym (idr C)))
        (trans (r (iden C) (right f) g)
               (cong (comp D (right f))
                     (trans (cong (comp D (right g)) (fid L)) (idr D))))

lemLlaw : {D : Cat {a}{b}}(L : Fun C D)(R : Fun D C)(T : Fun C C)
          (p : T ≅ R ○ L) (η : ∀ {X} → Hom C X (OMap T X)) →
          (right : {X : Obj C} {Y : Obj D} →
                   Hom C X (OMap R Y) → Hom D (OMap L X) Y) →
          (left : {X : Obj C} {Y : Obj D} →
                  Hom D (OMap L X) Y → Hom C X (OMap R Y)) →
          (q : {X : Obj C} {Y : Obj D} (f : Hom D (OMap L X) Y) →
               right (left f) ≅ f) →
          (r : {X : Obj C} → left (iden D {OMap L X}) ≅ η {X}) →
          (t : {X X' : Obj C}{Y Y' : Obj D}
                   (f : Hom C X' X)(g : Hom D Y Y')
                   (h : Hom C X (OMap R Y)) →
                   right (comp C (HMap R g) (comp C h f))
                   ≅
                   comp D g (comp D (right h) (HMap L f)) ) →
          {X Y : Obj C} (f : Hom C X Y) →
          right (subst (Hom C X) (fcong Y (cong OMap p))  (comp C η f))
          ≅
          HMap L f
lemLlaw {D = D} L R .(R ○ L) refl η right left q r t {X}{Y} f =
  trans (cong (λ g → right (comp C g f)) (sym r))
        (trans (trans (trans (cong right
                                   (trans (sym (idl C))
                                          (cong (λ g → comp C g
                                                   (comp C (left (iden D)) f))
                                                (sym (fid R)))))
                             (t f (iden D) (left (iden D))))
                      (cong (comp D (iden D))
                            (trans (cong (λ g → comp D g (HMap L f))
                                         (q (iden D)))
                                   (idl D))))
               (idl D))

K' : (A : Obj CatofAdj) → Fun (D KlObj) (D A)
K' A = record {
                 OMap = OMap (L (adj A));
                 HMap =
                   λ {X} {Y} f →
                     right (adj A)
                     (subst (Hom C X) (fcong Y (cong OMap (sym (law A)))) f);
                 fid =
                   lemfid (L (adj A)) (R (adj A)) (TFun M) (sym (law A)) η
                   (right (adj A)) (left (adj A)) (lawa (adj A)) (ηlaw A);
                 fcomp =
                   lemfcomp (L (adj A))
                            (R (adj A))
                            (TFun M)
                            (sym (law A))
                            bind
                            (right (adj A))
                            (bindlaw A)
                            (natright (adj A)) }

Llaw' : (A : Obj CatofAdj) → K' A ○ L (adj KlObj) ≅ L (adj A)
Llaw' A = FunctorEq
  _
  _
  refl
  (iext λ _ → iext λ _ → ext $ lemLlaw
    (L (adj A))
    (R (adj A))
    (TFun M)
    (sym (law A))
    η
    (right (adj A))
    (left (adj A))
    (lawa (adj A))
    (ηlaw A)
    (natright (adj A)))

Rlaw' : (A : Obj CatofAdj) → R (adj KlObj) ≅ R (adj A) ○ K' A
Rlaw' A = FunctorEq
  _
  _
  (cong OMap (sym (law A)))
             (iext λ _ → iext λ _ → ext λ _ → sym (bindlaw A))

rightlaw' : (A : Obj CatofAdj) →
            {X : Obj C} {Y : Obj (D KlObj)}
            {f : Hom C X (OMap (R (adj KlObj)) Y)} →
            HMap (K' A) (right (adj KlObj) f) ≅
            right (adj A) (subst (Hom C X) (fcong Y (cong OMap (Rlaw' A))) f)
rightlaw' A {X}{Y}{f} =
  cong (right (adj A))
       (trans (stripsubst (Hom C X) f (fcong Y (cong OMap (sym (law A)))))
              (sym (stripsubst (Hom C X) f (fcong Y (cong OMap (Rlaw' A))))))

KlHom : {A : Obj CatofAdj} → Hom CatofAdj KlObj A
KlHom {A} = record {
  K        = K' A;
  Llaw     = Llaw' A;
  Rlaw     = Rlaw' A;
  rightlaw = rightlaw' A }

uniq : {X : Obj CatofAdj}{f : Hom CatofAdj KlObj X} → KlHom ≅ f
uniq {X}{V} = HomAdjEq
  _
  _
  (FunctorEq
    _
    _
    (cong OMap (sym (HomAdj.Llaw V)))
    (iext λ A → iext λ B → ext λ f →
                          trans (cong₂ (λ B₁ → right (adj X) {A} {B₁})
                                (sym (fcong B (cong OMap (HomAdj.Llaw V))))
                                (trans (stripsubst
                                         (Hom C A)
                                         f
                                         (fcong B (cong OMap (sym (law X)))))
                                       (sym (stripsubst
                                              (Hom C A)
                                              f
                                              (fcong
                                                B
                                                (cong OMap (HomAdj.Rlaw V)))))))
                         (sym (HomAdj.rightlaw V))))

KlIsInit : Init CatofAdj KlObj
KlIsInit = record {
  i   = KlHom;
  law = uniq}
-- -}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --cubical --no-sized-types --no-guardedness #-}
module Issue2487.c where

postulate admit : {A : Set} -> A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda