text:
module Basic.Axiomatic.Total where

open import Data.Bool hiding (not; if_then_else_; _∧_)
open import Data.Vec hiding ([_]; _++_; split)
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (map to prodMap)
open import Data.Nat
open import Relation.Nullary
open import Data.Empty
import Level as L

open import Utils.Decidable
open import Basic.AST
open import Basic.BigStep

{-
Total axiomatic correctness (The first part of chapter 6.4).
For general notes on axiomatic correctness see Partial.agda
The most interesting part is here is the proof of completeness (exercise 6.33).
-}

_∧_ :
  ∀ {α β γ}{A : Set α}
  → (A → Set β)
  → (A → Set γ)
  → (A → Set _)
_∧_ f g x = f x × g x

_==>_ :
  ∀ {α β γ}{A : Set α}
  → (A → Set β)
  → (A → Set γ)
  → Set _
_==>_ f g = ∀ {x} → f x → g x

infixr 4 _,_
data 〈_〉_〈_〉 {n} : (State n → Set) → St n → (State n → Set) → Set₁ where

  skip :
           ∀ {P}
    → -----------------
      〈 P 〉 skip 〈 P 〉

  ass :
                        ∀ {x a P}
    → ----------------------------------------------
      〈 (λ s → P (s [ x ]≔ ⟦ a ⟧ᵉ s)) 〉 x := a 〈 P 〉

  _,_ :
             ∀ {P Q R S₁ S₂} →
      〈 P 〉 S₁ 〈 Q 〉 → 〈 Q 〉 S₂ 〈 R 〉
    → --------------------------------
            〈 P 〉 S₁ , S₂ 〈 R 〉

  if :
                          ∀ {P Q b S₁ S₂} →
      〈 (T ∘ ⟦ b ⟧ᵉ) ∧ P 〉 S₁ 〈 Q 〉 → 〈 (F ∘ ⟦ b ⟧ᵉ) ∧ P 〉 S₂ 〈 Q 〉
    → --------------------------------------------------------------
                  〈 P 〉 if b then S₁ else S₂ 〈 Q 〉

  {-
  This is the only difference between the partial and total system.
  The definition is exactly the same as in the book.
  -}
  while :
       ∀ {b S}
     → (P : ℕ → State n → Set)
     → (∀ n → P (suc n) ==> (T ∘ ⟦ b ⟧ᵉ))
     → (P 0 ==> (F ∘ ⟦ b ⟧ᵉ))
     → (∀ n → 〈 P (suc n) 〉 S 〈 P n 〉)
    → ---------------------------------
      〈 (λ s → ∃ λ n → P n s) 〉 while b do S 〈 P 0 〉

  cons :
                ∀ {P' Q' P Q S} →
      P ==> P' → 〈 P' 〉 S 〈 Q' 〉 → Q' ==> Q
    → -----------------------------------------
                 〈 P 〉 S 〈 Q 〉

-- Weakest precondition
------------------------------------------------------------
wp : ∀ {n} → St n → (State n → Set) → State n → Set
wp S Q s = ∃ λ s' → ⟨ S , s ⟩⟱ s' × Q s'

-- Soundness
------------------------------------------------------------

{-
This is more complicated than the soundess proof for the partial system,
because we have to construct an actual big-step derivation.

In the "if" case we have to evaluate the branch condition to
see whether we should return an "if-true" or an "if-false"  derivation.

In the "while" case we recurse on the natural number "measure" of the loop,
building an appropriately sized derivation for the loop
-}

sound : ∀ {n}{S : St n}{P Q} → 〈 P 〉 S 〈 Q 〉 → (P ==> wp S Q)
sound skip ps = _ , skip , ps

sound ass ps =  _ , ass , ps
sound (p , p₁) ps with sound p ps
... | s'  , runp  , qs' with sound p₁ qs'
... | s'' , runp₁ , qs'' = s'' , (runp , runp₁) , qs''

sound (if {b = b} p p₁) {s} ps with ⟦ b ⟧ᵉ s | inspect ⟦ b ⟧ᵉ s
... | true  | [ b≡true  ] =
  let Tb = ≡true→T b≡true
  in prodMap id
       (λ x₁ → (if-true Tb (proj₁ x₁)) , (proj₂ x₁))
       (sound p {s} (Tb , ps))

... | false | [ b≡false ] =
  let Fb = ≡false→F b≡false
  in prodMap id
       (λ x₁ → (if-false Fb (proj₁ x₁)) , (proj₂ x₁))
       (sound p₁ {s} (Fb , ps))

sound (while{b = b}{S = S} P pre post decr) {s} (start , ps) = go s start ps
  where
    go : ∀ s n → P n s → wp (while b do S) (P 0) s
    go s zero    ps = s , while-false (post ps) , ps
    go s (suc n) ps with sound (decr n) ps
    ... | s' , runS , ps' with go s' n ps'
    ... | s'' , runW , ps'' = s'' , while-true (pre n ps) runS runW , ps''

sound (cons x p x₁) ps with sound p (x ps)
... | s' , runp , qs' = s' , runp , x₁ qs'

-- Completeness
------------------------------------------------------------

complete : ∀ {n}(S : St n){P Q} → (P ==> wp S Q) → 〈 P 〉 S 〈 Q 〉

complete (x := exp) {P}{Q} f = cons go ass id
  where go : P ==> (λ s → Q (s [ x ]≔ ⟦ exp ⟧ᵉ s))
        go {s} ps with f ps
        go ps | ._ , ass , qs' = qs'

complete skip {P}{Q} f = cons go skip id
  where go : P ==> Q
        go {s} ps with f ps
        go ps | x , skip , qs' = qs'

complete (S , S₁){P}{Q} f  = complete S {P} {wp S₁ Q} go , complete S₁ id
  where go : P ==> wp S (wp S₁ Q)
        go {s} ps with f ps
        go {s} ps | s' , (run , run₂) , qs' = _ , run , s' , run₂ , qs'

complete (if b then S else S₁){P}{Q} f =
  if (complete S {(T ∘ ⟦ b ⟧ᵉ) ∧ P} {Q} go1) (complete S₁ {(F ∘ ⟦ b ⟧ᵉ) ∧ P} {Q} go2)
  where go1 : ((T ∘ ⟦ b ⟧ᵉ) ∧ P) ==> wp S Q
        go1 {s} (pb , ps) with f ps
        go1 (pb , ps) | s' , if-true pb' run , qs' = s' , run , qs'
        go1 (pb , ps) | s' , if-false pb' run , qs' with trans (sym (F→≡false pb')) (T→≡true pb)
        ... | ()

        go2 : ((F ∘ ⟦ b ⟧ᵉ) ∧ P) ==> wp S₁ Q
        go2 {s} (pb , ps) with f ps
        go2 (pb , ps) | s' , if-true pb' run , qs' with trans (sym $ F→≡false pb) (T→≡true pb')
        ... | ()
        go2 (pb , ps) | s' , if-false pb' run , qs' = s' , run , qs'

{-
This is the interesting part. I needed to do quite a bit of thinking to get this right.

So, we'd like to construct a proof of total corectness given the validity of a Hoare triple.

We're much less constrained here than in pretty much all of the other proofs, because our objective
is to construct a suitable P *predicate* for the loop body. Recall the axiom for "while"

  while :
       ∀ {b S}
     → (P : ℕ → State n → Set)
     → (∀ n → P (suc n) ==> (T ∘ ⟦ b ⟧ᵉ))
     → (P 0 ==> (F ∘ ⟦ b ⟧ᵉ))
     → (∀ n → 〈 P (suc n) 〉 S 〈 P n 〉)
    → ---------------------------------
      〈 (λ s → ∃ λ n → P n s) 〉 while b do S 〈 P 0 〉
-}
complete {n}(while b do S){P}{Q} f = cons pre-loop loop post-loop
  where

    {-
    P must decrease on each iteration, and P 0 must imply that the loop has finished, and
    P (suc n) must imply that the loop's still running.

    The only sensible choice for the decreasing loop variant is the length of the derivation
    of the loop:
    -}

    loop-size : ∀ {n b s s'}{S : St n} → ⟨ while b do S , s ⟩⟱ s' → ℕ
    loop-size (while-true x runS runW) = suc (loop-size runW)
    loop-size (while-false x)          = zero

    {- And now the loop predicate can be defined as: -}

    P' : ℕ → State n → Set
    P' n s = ∃₂ λ s' (runW : ⟨ while b do S , s ⟩⟱ s') → (loop-size runW ≡ n) × Q s'

    {- The construction of the loop body proof is slightly complicated by the fact that if we want
       to recurse on the measure "n" argument, then we have to unfold the loop derivation two layers
       deep (because the successor case for indction on "n" implies "(suc (suc n))" value for the
       derivation length -}

    body : ∀ n → 〈 P' (suc n) 〉 S 〈 P' n 〉
    body n = complete S (go n)
      where
        go : ∀ n → P' (suc n) ==> wp S (P' n)
        go zero (x , while-false x₁ , () , qs')
        go zero (s''' , while-true x₁ runW (while-true x₂ runW₁ runW₂) , () , qs')
        go (suc n₂) (x , while-false x₁ , () , qs')
        go (suc n₂) (s' , while-true x₁ runW (while-false x₂) , () , qs')

        go zero (s' , while-true x₁ runW (while-false x₂) , psize , qs') =
          s' , runW , s' , while-false x₂ , refl , qs'

        go (suc n) {s1} (slast , while-true pb1 runS1 (while-true pb2 runS2 runW2) , psize1 , qslast)
          with go n (slast , while-true pb2 runS2 runW2 , cong pred psize1 , qslast)
        ... | s2 , runS3 , s3 , runW3 , psize3 , q3 =
          _ , runS1 , s3 , (while-true pb2 runS3 runW3) , cong suc psize3 , q3

    pre-loop : P ==> (λ s → ∃ λ n → P' n s)
    pre-loop {s} ps with f ps
    ... | s' , runW , qs' = loop-size runW , s' , runW , refl , qs'

    post-loop : P' 0 ==> Q
    post-loop (s' , while-false pb , psize , qs') = qs'
    post-loop (s' , while-true pb x₁ x₂ , () , qs')

    loop : 〈 (λ s → ∃ λ n → P' n s) 〉 while b do S 〈 P' 0 〉
    loop = while P' pre post body
      where
        pre : ∀ n → P' (suc n) ==> (T ∘ ⟦ b ⟧ᵉ)
        pre n (s' , while-true pb _ _ , _) = pb
        pre n (s' , while-false _ , () , qs')

        post : P' 0 ==> (F ∘ ⟦ b ⟧ᵉ)
        post (s' , while-true pb runS runW , () , qs')
        post (s' , while-false pb , refl , qs') = pb


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

module Categories.Functor.Construction.Limit where

open import Function using (_$_)

open import Categories.Adjoint
open import Categories.Adjoint.Equivalence
open import Categories.Adjoint.Properties
open import Categories.Category
open import Categories.Category.Equivalence
open import Categories.Category.Construction.Cones
open import Categories.Category.Complete
open import Categories.Category.Cocomplete
open import Categories.Category.Construction.Functors
open import Categories.Functor
open import Categories.Functor.Construction.Diagonal
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; module ≃)
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Duality

import Categories.Diagram.Limit as Lim
import Categories.Diagram.Cone as Con
import Categories.Morphism.Reasoning as MR

module _ {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (Com : Complete o′ ℓ′ e′ C) {J : Category o′ ℓ′ e′} where
  private
    module C = Category C
    module J = Category J
    open C
    open HomReasoning
    open Lim.Limit
    open Con.Cone⇒ renaming (commute to ⇒-commute)
    open MR C

    K⇒lim : ∀ {F G : Functor J C} (α : NaturalTransformation F G) (K : Con.Cone F) →
              Cones G [ nat-map-Cone α K , limit (Com G) ]
    K⇒lim {G = G} α K = rep-cone (Com G) (nat-map-Cone α K)

    lim⇒lim : ∀ {F G : Functor J C} (α : NaturalTransformation F G) →
                Cones G [ nat-map-Cone α (limit (Com F)) , limit (Com G) ]
    lim⇒lim {F} α = K⇒lim α (limit (Com F))

    id-Cone : ∀ X → Con.Cone {C = C} {J = J} (const X)
    id-Cone X = record
      { apex = record
        { ψ       = λ _ → C.id
        ; commute = λ _ → C.identity²
        }
      }

    X⇒limΔ : ∀ X → Cones (const {C = J} X) [ id-Cone X , limit (Com (const X)) ]
    X⇒limΔ X = rep-cone (Com (const X)) _

  LimitF : Functor (Functors J C) C
  LimitF = record
    { F₀           = λ F → apex (Com F)
    ; F₁           = λ {F G} α → arr (lim⇒lim α)
    ; identity     = λ {F} → terminal.!-unique (Com F) $ record
      { arr     = C.id
      ; commute = id-comm
      }
    ; homomorphism = λ {F G H} {α β} →
      let module α = NaturalTransformation α
          module β = NaturalTransformation β
      in terminal.!-unique₂ (Com H) {_} {terminal.! (Com H)}
      {record { commute = λ {j} → begin
        proj (Com H) j ∘ arr (lim⇒lim β) ∘ arr (lim⇒lim α) ≈⟨ pullˡ (⇒-commute (lim⇒lim β)) ⟩
        (β.η j ∘ proj (Com G) j) ∘ arr (lim⇒lim α)         ≈⟨ assoc ⟩
        β.η j ∘ proj (Com G) j ∘ arr (lim⇒lim α)           ≈⟨ pushʳ (⇒-commute (lim⇒lim α)) ⟩
        (β.η j ∘ α.η j) ∘ proj (Com F) j                   ∎ }}
    ; F-resp-≈     = λ {F G} {α β} eq → terminal.!-unique (Com G) $ record
      { commute = ⇒-commute (lim⇒lim β) ○ ∘-resp-≈ˡ (⟺ eq)
      }
    }

  Δ⊣LimitF : ΔF J ⊣ LimitF
  Δ⊣LimitF = record
    { unit   = ntHelper record
      { η       = λ X → rep (Com (const X)) (id-Cone X)
      ; commute = λ {X Y} f → terminal.!-unique₂ (Com (const Y))
        {record
          { apex = record
            { ψ       = λ _ → f
            ; commute = λ _ → C.identityˡ
            }
          }}
        {record
          { commute = cancelˡ (⇒-commute (X⇒limΔ Y))
          }}
        {record
          { commute =
            ⇒-commute (Cones (const Y) [ lim⇒lim (constNat f)
                                       ∘ nat-map-Cone⇒ (constNat f) (terminal.! (Com (const X)) {id-Cone X}) ])
            ○ identityʳ
          }}
      }
    ; counit = ntHelper record
      { η       = counit-nat
      ; commute = λ α → ⇒-commute (lim⇒lim α)
      }
    ; zig    = λ {X} → ⇒-commute (X⇒limΔ X)
    ; zag    = λ {F} →
      let apF = apex (Com F)
          align : Cones F [ limit (Com F) , nat-map-Cone (counit-nat F) (id-Cone apF) ]
          align = record
            { arr     = C.id
            ; commute = identityʳ ○ identityʳ
            }
          limF⇒limF : Cones F [ limit (Com F) , limit (Com F) ]
          limF⇒limF = Cones F [ Cones F [ lim⇒lim (counit-nat F)
                              ∘ nat-map-Cone⇒ (counit-nat F) (terminal.! (Com (const apF))) ]
                              ∘ align ]
      in terminal.!-unique₂ (Com F)
         {limit (Com F)}
         {record { commute = ∘-resp-≈ʳ (⟺ identityʳ) ○ ⇒-commute limF⇒limF }}
         {record { commute = identityʳ }}
    }
    where counit-nat : (F : Functor J C) → NaturalTransformation (const (apex (Com F))) F
          counit-nat F = ntHelper record
            { η       = proj (Com F)
            ; commute = λ f → identityʳ ○ ⟺ (limit-commute (Com F) f)
            }

module _ {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (Coc : Cocomplete o′ ℓ′ e′ C) {J : Category o′ ℓ′ e′} where
  private
    module C = Category C
    module J = Category J
    open C
    open MR C

    Com : Complete o′ ℓ′ e′ C.op
    Com F = Colimit⇒coLimit C (Coc (Functor.op F))
    LF  : Functor (Functors J.op op) C.op
    LF    = LimitF C.op Com {J.op}

  ColimitF : Functor (Functors J C) C
  ColimitF = Functor.op LF ∘F opF⇐

  ColimitF⊣Δ : ColimitF ⊣ ΔF J
  ColimitF⊣Δ = ⊣×≃⇒⊣ helper ≃.refl ΔF≃
    where Δ⊣LimitFᵒᵖ : ΔF J.op ⊣ LF
          Δ⊣LimitFᵒᵖ = Δ⊣LimitF op Com {J.op}
          opF⊣ : opF⇐ {A = J} {C} ⊣ opF⇒
          opF⊣ = StrongEquivalence.F⊣G.R⊣L Functorsᵒᵖ-equiv
          helper : ColimitF ⊣ opF⇒ ∘F Functor.op (ΔF J.op)
          helper = opF⊣ ∘⊣ Adjoint.op Δ⊣LimitFᵒᵖ
          ΔF≃ : opF⇒ ∘F Functor.op (ΔF J.op) ≃ ΔF J
          ΔF≃ = record
            { F⇒G = record
              { η           = λ _ → idN
              ; commute     = λ _ → id-comm-sym
              ; sym-commute = λ _ → id-comm
              }
            ; F⇐G = record
              { η           = λ _ → idN
              ; commute     = λ _ → id-comm-sym
              ; sym-commute = λ _ → id-comm
              }
            ; iso = λ X → record
              { isoˡ = identity²
              ; isoʳ = identity²
              }
            }

ext: agda

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
------------------------------------------------------------------------
-- Strong bisimilarity for partially defined values, along with a
-- proof showing that this relation is pointwise isomorphic to path
-- equality
------------------------------------------------------------------------

{-# OPTIONS --cubical --sized-types #-}

module Delay-monad.Bisimilarity.For-all-sizes where

open import Equality.Path hiding (ext)
open import Prelude
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)

open import Delay-monad

private
  variable
    a : Level
    A : Type a
    x : A
    i : Size

mutual

  -- A variant of strong bisimilarity that relates values of any size,
  -- not only those of size ∞.
  --
  -- Note: I have not managed to prove that this relation is pointwise
  -- isomorphic to strong bisimilarity as defined in
  -- Delay-monad.Bisimilarity (when the relation is restricted to
  -- fully defined values).

  infix 4 [_]_∼ˢ_ [_]_∼ˢ′_

  data [_]_∼ˢ_ {A : Type a} (i : Size) :
               Delay A i → Delay A i → Type a where
    now   : [ i ] now x ∼ˢ now x
    later : {x y : Delay′ A i} →
            [ i ] x ∼ˢ′ y → [ i ] later x ∼ˢ later y

  record [_]_∼ˢ′_ {A : Type a}
                  (i : Size) (x y : Delay′ A i) : Type a where
    coinductive
    field
      force : {j : Size< i} → [ j ] x .force ∼ˢ y .force

open [_]_∼ˢ′_ public

mutual

  -- Strong bisimilarity is reflexive. Note that the proof is
  -- size-preserving.

  reflexiveˢ : (x : Delay A i) → [ i ] x ∼ˢ x
  reflexiveˢ (now x)   = now
  reflexiveˢ (later x) = later (reflexiveˢ′ x)

  reflexiveˢ′ : (x : Delay′ A i) → [ i ] x ∼ˢ′ x
  reflexiveˢ′ x .force = reflexiveˢ (x .force)

mutual

  -- Extensionality: Strong bisimilarity implies equality.

  ext : {x y : Delay A i} →
        [ i ] x ∼ˢ y → x ≡ y
  ext now       = refl
  ext (later p) = cong later (ext′ p)

  ext′ : {x y : Delay′ A i} →
         [ i ] x ∼ˢ′ y → x ≡ y
  ext′ p i .force = ext (p .force) i

mutual

  -- The extensionality proof maps reflexivity to reflexivity.

  ext-reflexiveˢ :
    (x : Delay A i) →
    ext (reflexiveˢ x) ≡ refl {x = x}
  ext-reflexiveˢ         (now x)   = refl
  ext-reflexiveˢ {i = i} (later x) =
    ext (reflexiveˢ (later x))         ≡⟨⟩
    cong later (ext′ (reflexiveˢ′ x))  ≡⟨ cong (cong later) (ext′-reflexiveˢ′ x) ⟩
    cong later refl                    ≡⟨⟩
    refl                               ∎

  ext′-reflexiveˢ′ :
    (x : Delay′ A i) →
    ext′ (reflexiveˢ′ x) ≡ refl {x = x}
  ext′-reflexiveˢ′ x i j .force = ext-reflexiveˢ (x .force) i j

-- Equality implies strong bisimilarity.

≡⇒∼ : {x y : Delay A i} → x ≡ y → [ i ] x ∼ˢ y
≡⇒∼ {x = x} eq = subst ([ _ ] x ∼ˢ_) eq (reflexiveˢ x)

≡⇒∼′ : {x y : Delay′ A i} → x ≡ y → [ i ] x ∼ˢ′ y
≡⇒∼′ eq .force = ≡⇒∼ (cong (λ x → x .force) eq)

private

  ≡⇒∼″ : {x y : Delay′ A i} → x ≡ y → [ i ] x ∼ˢ′ y
  ≡⇒∼″ {x = x} eq = subst ([ _ ] x ∼ˢ′_) eq (reflexiveˢ′ x)

-- The three lemmas above map reflexivity to reflexivity.

≡⇒∼-refl :
  {x : Delay A i} →
  ≡⇒∼ (refl {x = x}) ≡ reflexiveˢ x
≡⇒∼-refl {x = x} =
  ≡⇒∼ refl                                 ≡⟨⟩
  subst ([ _ ] x ∼ˢ_) refl (reflexiveˢ x)  ≡⟨ subst-refl ([ _ ] x ∼ˢ_) (reflexiveˢ x) ⟩∎
  reflexiveˢ x                             ∎

≡⇒∼′-refl :
  {x : Delay′ A i} →
  ≡⇒∼′ (refl {x = x}) ≡ reflexiveˢ′ x
≡⇒∼′-refl i .force = ≡⇒∼-refl i

private

  ≡⇒∼″-refl :
    {x : Delay′ A i} →
    ≡⇒∼″ (refl {x = x}) ≡ reflexiveˢ′ x
  ≡⇒∼″-refl {x = x} =
    ≡⇒∼″ refl                                  ≡⟨⟩
    subst ([ _ ] x ∼ˢ′_) refl (reflexiveˢ′ x)  ≡⟨ subst-refl ([ _ ] x ∼ˢ′_) (reflexiveˢ′ x) ⟩∎
    reflexiveˢ′ x                              ∎

  -- ≡⇒∼′ and ≡⇒″ are pointwise equal.

  ≡⇒∼′≡≡⇒∼″ :
    {x y : Delay′ A i} {eq : x ≡ y} →
    ≡⇒∼′ eq ≡ ≡⇒∼″ eq
  ≡⇒∼′≡≡⇒∼″ = elim
    (λ eq → ≡⇒∼′ eq ≡ ≡⇒∼″ eq)
    (λ x →
       ≡⇒∼′ refl      ≡⟨ ≡⇒∼′-refl ⟩
       reflexiveˢ′ x  ≡⟨ sym ≡⇒∼″-refl ⟩∎
       ≡⇒∼″ refl      ∎)
    _

private

  -- Extensionality and ≡⇒∼/≡⇒∼′ are inverses.

  ext∘≡⇒∼ :
    {x y : Delay A i}
    (eq : x ≡ y) → ext (≡⇒∼ eq) ≡ eq
  ext∘≡⇒∼ = elim
    (λ eq → ext (≡⇒∼ eq) ≡ eq)
    (λ x → ext (≡⇒∼ refl)      ≡⟨ cong ext ≡⇒∼-refl ⟩
           ext (reflexiveˢ x)  ≡⟨ ext-reflexiveˢ x ⟩∎
           refl                ∎)

  ext′∘≡⇒∼′ :
    {x y : Delay′ A i}
    (eq : x ≡ y) → ext′ (≡⇒∼′ eq) ≡ eq
  ext′∘≡⇒∼′ = elim
    (λ eq → ext′ (≡⇒∼′ eq) ≡ eq)
    (λ x → ext′ (≡⇒∼′ refl)      ≡⟨ cong ext′ ≡⇒∼′-refl ⟩
           ext′ (reflexiveˢ′ x)  ≡⟨ ext′-reflexiveˢ′ x ⟩∎
           refl                  ∎)

  mutual

    ≡⇒∼∘ext :
      {x y : Delay A i}
      (eq : [ i ] x ∼ˢ y) →
      ≡⇒∼ (ext eq) ≡ eq
    ≡⇒∼∘ext now =
      ≡⇒∼ (ext now)  ≡⟨⟩
      ≡⇒∼ refl       ≡⟨ ≡⇒∼-refl ⟩∎
      now            ∎
    ≡⇒∼∘ext (later {x = x} {y = y} p) =
      ≡⇒∼ (ext (later p))                                    ≡⟨⟩

      ≡⇒∼ (cong later (ext′ p))                              ≡⟨⟩

      subst ([ _ ] later x ∼ˢ_) (cong later (ext′ p))
        (later (reflexiveˢ′ x))                              ≡⟨ sym $ subst-∘ ([ _ ] later x ∼ˢ_) later _ {p = later (reflexiveˢ′ x)} ⟩

      subst (λ y → [ _ ] later x ∼ˢ later y) (ext′ p)
        (later (reflexiveˢ′ x))                              ≡⟨ elim¹
                                                                  (λ eq → subst (λ y → [ _ ] later x ∼ˢ later y) eq (later (reflexiveˢ′ x)) ≡
                                                                          later (subst ([ _ ] x ∼ˢ′_) eq (reflexiveˢ′ x))) (
          subst (λ y → [ _ ] later x ∼ˢ later y) refl
            (later (reflexiveˢ′ x))                                 ≡⟨ subst-refl (λ y → [ _ ] later x ∼ˢ later y) _ ⟩

          later (reflexiveˢ′ x)                                     ≡⟨ cong later $ sym $ subst-refl ([ _ ] x ∼ˢ′_) _ ⟩∎

          later (subst ([ _ ] x ∼ˢ′_) refl (reflexiveˢ′ x))         ∎)
                                                                  (ext′ p) ⟩
      later (subst ([ _ ] x ∼ˢ′_) (ext′ p) (reflexiveˢ′ x))  ≡⟨⟩

      later (≡⇒∼″ (ext′ p))                                  ≡⟨ cong later $ sym ≡⇒∼′≡≡⇒∼″ ⟩

      later (≡⇒∼′ (ext′ p))                                  ≡⟨ cong later (≡⇒∼′∘ext′ p) ⟩∎

      later p                                                ∎

    ≡⇒∼′∘ext′ :
      {x y : Delay′ A i}
      (eq : [ i ] x ∼ˢ′ y) →
      ≡⇒∼′ (ext′ eq) ≡ eq
    ≡⇒∼′∘ext′ eq i .force = ≡⇒∼∘ext (eq .force) i

-- Strong bisimilarity and equality are pointwise isomorphic.

∼↔≡ : {x y : Delay A i} → [ i ] x ∼ˢ y ↔ x ≡ y
∼↔≡ = record
  { surjection = record
    { logical-equivalence = record
      { to   = ext
      ; from = ≡⇒∼
      }
    ; right-inverse-of = ext∘≡⇒∼
    }
  ; left-inverse-of = ≡⇒∼∘ext
  }

∼′↔≡ : {x y : Delay′ A i} → [ i ] x ∼ˢ′ y ↔ x ≡ y
∼′↔≡ = record
  { surjection = record
    { logical-equivalence = record
      { to   = ext′
      ; from = ≡⇒∼′
      }
    ; right-inverse-of = ext′∘≡⇒∼′
    }
  ; left-inverse-of = ≡⇒∼′∘ext′
  }

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


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

open import HoTT
open import homotopy.FunctionOver
open import groups.ProductRepr
open import cohomology.Theory
open import cohomology.WedgeCofiber

{- For the cohomology group of a suspension ΣX, the group inverse has the
 - explicit form Cⁿ(flip-susp) : Cⁿ(ΣX) → Cⁿ(ΣX).
 -}

module cohomology.InverseInSusp {i} (CT : CohomologyTheory i)
  (n : ℤ) {X : Ptd i} where

open CohomologyTheory CT
open import cohomology.Functor CT
open import cohomology.BaseIndependence CT
open import cohomology.Wedge CT

private
  module CW = CWedge n (⊙Susp X) (⊙Susp X)

  module Subtract = SuspRec {C = fst (⊙Susp X ⊙∨ ⊙Susp X)}
    (winl south)
    (winr south)
    (λ x → ap winl (! (merid x)) ∙ wglue ∙ ap winr (merid x))

  subtract = Subtract.f

  ⊙subtract : ⊙Susp X ⊙→ ⊙Susp X ⊙∨ ⊙Susp X
  ⊙subtract = (subtract , ! (ap winl (merid (pt X))))

  projl-subtract : ∀ σ → projl _ _ (subtract σ) == Susp-flip σ
  projl-subtract = Susp-elim idp idp $
    ↓-='-from-square ∘ vert-degen-square ∘ λ x →
      ap-∘ (projl _ _) subtract (merid x)
      ∙ ap (ap (projl _ _)) (Subtract.merid-β x)
      ∙ ap-∙ (projl _ _) (ap winl (! (merid x))) (wglue ∙ ap winr (merid x))
      ∙ ((∘-ap (projl _ _) winl (! (merid x))
          ∙ ap-idf _)
         ∙2 (ap-∙ (projl _ _) wglue (ap winr (merid x))
             ∙ (Projl.glue-β _ _
                ∙2 (∘-ap (projl _ _) winr (merid x) ∙ ap-cst _ _))))
      ∙ ∙-unit-r _
      ∙ ! (FlipSusp.merid-β x)

  projr-subtract : ∀ σ → projr _ _ (subtract σ) == σ
  projr-subtract = Susp-elim idp idp $
    ↓-∘=idf-in' (projr _ _) subtract ∘ λ x →
      ap (ap (projr _ _)) (Subtract.merid-β x)
      ∙ ap-∙ (projr _ _) (ap winl (! (merid x))) (wglue ∙ ap winr (merid x))
      ∙ ((∘-ap (projr _ _) winl (! (merid x)) ∙ ap-cst _ _)
         ∙2 (ap-∙ (projr _ _) wglue (ap winr (merid x))
             ∙ (Projr.glue-β _ _
                ∙2 (∘-ap (projr _ _) winr (merid x) ∙ ap-idf _))))

  fold-subtract : ∀ σ → fold (subtract σ) == south
  fold-subtract = Susp-elim idp idp $
    ↓-app=cst-in ∘ ! ∘ λ x →
      ∙-unit-r _
      ∙ ap-∘ fold subtract (merid x)
      ∙ ap (ap fold) (Subtract.merid-β x)
      ∙ ap-∙ fold (ap winl (! (merid x))) (wglue ∙ ap winr (merid x))
      ∙ ((∘-ap fold winl (! (merid x)) ∙ ap-idf _)
         ∙2 (ap-∙ fold wglue (ap winr (merid x))
             ∙ (Fold.glue-β
                ∙2 (∘-ap fold winr (merid x) ∙ ap-idf _))))
      ∙ !-inv-l (merid x)

  cancel :
    ×ᴳ-fanin (C-is-abelian n _) (CF-hom n (⊙Susp-flip X)) (idhom _) ∘ᴳ ×ᴳ-diag
    == cst-hom
  cancel =
    ap2 (λ φ ψ → ×ᴳ-fanin (C-is-abelian n _) φ ψ ∘ᴳ ×ᴳ-diag)
        (! (CF-λ= n projl-subtract))
        (! (CF-ident n) ∙ ! (CF-λ= n projr-subtract))
    ∙ transport (λ {(G , φ , ψ) → φ ∘ᴳ ψ == cst-hom})
        (pair= (CW.path) $ ↓-×-in
          (CW.Wedge-in-over ⊙subtract)
          (CW.⊙Wedge-rec-over (⊙idf _) (⊙idf _)
           ▹ ap2 ×ᴳ-fanout (CF-ident n) (CF-ident n)))
        (! (CF-comp n ⊙fold ⊙subtract)
         ∙ CF-λ= n (λ σ → fold-subtract σ ∙ ! (merid (pt X)))
         ∙ CF-cst n)

C-Susp-flip-is-inv :
  CF-hom n (⊙Susp-flip X) == inv-hom (C n (⊙Susp X)) (C-is-abelian _ _)
C-Susp-flip-is-inv = group-hom= $ λ= λ g →
  ! (Group.inv-unique-l (C n (⊙Susp X)) _ g (app= (ap GroupHom.f cancel) g))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --safe --warning=error #-}

open import Setoids.Setoids
open import Groups.SymmetricGroups.Definition
open import Groups.FreeGroup.Definition
open import Decidable.Sets
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import LogicalFormulae
open import Boolean.Definition

module Groups.FreeGroup.Word {a : _} {A : Set a} (decA : DecidableSet A) where

data ReducedWord : Set a
wordLength : ReducedWord → ℕ
firstLetter : (w : ReducedWord) → .(0 <N wordLength w) → FreeCompletion A

data PrependIsValid (w : ReducedWord) (l : FreeCompletion A) : Set a where
  wordEmpty : wordLength w ≡ 0 → PrependIsValid w l
  wordEnding : .(pr : 0 <N wordLength w) → .(freeCompletionEqual decA l (freeInverse (firstLetter w pr)) ≡ BoolFalse) → PrependIsValid w l

data ReducedWord where
  empty : ReducedWord
  prependLetter : (letter : FreeCompletion A) → (w : ReducedWord) → PrependIsValid w letter → ReducedWord

firstLetter empty ()
firstLetter (prependLetter letter w x) pr = letter

wordLength empty = 0
wordLength (prependLetter letter w pr) = succ (wordLength w)

prependLetterRefl : {x : FreeCompletion A} {w : ReducedWord} → {pr1 pr2 : PrependIsValid w x} → prependLetter x w pr1 ≡ prependLetter x w pr2
prependLetterRefl {x} {empty} {wordEmpty refl} {wordEmpty refl} = refl
prependLetterRefl {x} {empty} {wordEmpty refl} {wordEnding () x₂}
prependLetterRefl {x} {empty} {wordEnding () x₁} {pr2}
prependLetterRefl {x} {prependLetter letter w x₁} {wordEmpty ()} {pr2}
prependLetterRefl {x} {prependLetter letter w x₁} {wordEnding pr x₂} {wordEmpty ()}
prependLetterRefl {x} {prependLetter letter w x₁} {wordEnding pr2 r2} {wordEnding pr1 r1} = refl

prependLetterInjective : {x : FreeCompletion A} {w1 w2 : ReducedWord} {pr1 : PrependIsValid w1 x} {pr2 : PrependIsValid w2 x} → prependLetter x w1 pr1 ≡ prependLetter x w2 pr2 → w1 ≡ w2
prependLetterInjective {x = x} {empty} {empty} {pr1} {pr2} pr = refl
prependLetterInjective {x = x} {prependLetter l1 w1 x1} {prependLetter .l1 .w1 .x1} {wordEnding pr₁ x₁} {wordEnding pr₂ x₂} refl = refl

prependLetterInjective' : {x y : FreeCompletion A} {w1 w2 : ReducedWord} {pr1 : PrependIsValid w1 x} {pr2 : PrependIsValid w2 y} → prependLetter x w1 pr1 ≡ prependLetter y w2 pr2 → x ≡ y
prependLetterInjective' refl = refl

badPrepend : {x : A} {w : ReducedWord} {pr : PrependIsValid w (ofInv x)} → (PrependIsValid (prependLetter (ofInv x) w pr) (ofLetter x)) → False
badPrepend (wordEmpty ())
badPrepend {x = x} (wordEnding pr bad) with decidableFreeCompletion decA (ofLetter x) (ofLetter x)
badPrepend {x} (wordEnding pr ()) | inl x₁
badPrepend {x} (wordEnding pr bad) | inr pr2 = pr2 refl

badPrepend' : {x : A} {w : ReducedWord} {pr : PrependIsValid w (ofLetter x)} → (PrependIsValid (prependLetter (ofLetter x) w pr) (ofInv x)) → False
badPrepend' (wordEmpty ())
badPrepend' {x = x} (wordEnding pr x₁) with decidableFreeCompletion decA (ofInv x) (ofInv x)
badPrepend' {x} (wordEnding pr ()) | inl x₂
badPrepend' {x} (wordEnding pr x₁) | inr pr2 = pr2 refl


text:
{-# OPTIONS --allow-unsolved-metas #-}
{- Diamond operator. -}
module TemporalOps.Diamond where

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad
open import TemporalOps.Common
open import TemporalOps.Next
open import TemporalOps.Delay
open import TemporalOps.Diamond.Functor public
open import TemporalOps.Diamond.Join
open import TemporalOps.Diamond.JoinLemmas

import Relation.Binary.PropositionalEquality as ≡
open import Data.Product
open import Relation.Binary.HeterogeneousEquality as ≅
            using (_≅_ ; ≅-to-≡ ; ≡-to-≅ ; cong₂)
open import Data.Nat.Properties
            using (+-identityʳ ; +-comm ; +-suc ; +-assoc)

open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

M-◇ : Monad ℝeactive
M-◇ = record
    { T = F-◇
    ; η = η-◇
    ; μ = μ-◇
    ; η-unit1 = refl
    ; η-unit2 = η-unit2-◇
    ; μ-assoc = λ{A}{n}{k} -> μ-assoc-◇ {A} {n} {k}
    }
    where
    η-◇ : I ⟹ F-◇
    η-◇ = record
        { at = λ A n x -> zero , x
        ; nat-cond = λ {A} {B} {f} {n} {a} → refl }

    private module μ = _⟹_ μ-◇
    private module η = _⟹_ η-◇
    private module F-◇ = Functor F-◇
    open ≡.≡-Reasoning

    η-unit2-◇ : {A : τ} {n : ℕ} {a : ◇ A at n} → (μ.at A n (F-◇.fmap (η.at A) n a)) ≡ a
    η-unit2-◇ {A} {n} {k , v} with inspect (compareLeq k n)
    -- n = k + l
    η-unit2-◇ {A} {.(k + l)} {k , v} | snd==[ .k + l ] with≡ pf =
        begin
            μ.at A (k + l) (F-◇.fmap (η.at A) (k + l) (k , v))
        ≡⟨⟩
            μ.at A (k + l) (k , (Functor.fmap (F-delay k) (η.at A) at (k + l)) v)
        ≡⟨⟩
            μ-compare A (k + l) k ((Functor.fmap (F-delay k) (η.at A) at (k + l)) v) (compareLeq k (k + l))
        ≡⟨ cong (λ x → μ-compare A (k + l) k ((Functor.fmap (F-delay k) (η.at A) at (k + l)) v) x) pf ⟩
            μ-compare A (k + l) k ((Functor.fmap (F-delay k) (η.at A) at (k + l)) v) snd==[ k + l ]
        ≡⟨⟩
            μ-shift k l ⌞ (rew (delay-+-left0 k l) ((Functor.fmap (F-delay k) (η.at A) at (k + l)) v)) ⌟
        ≡⟨ cong!
            (delay-+-left0-eq k l ((Functor.fmap (F-delay k) (η.at A) at (k + l)) v)
                                          ((Functor.fmap (F-delay (k + 0)) (η.at A) at (k + l)) v′) pr)
         ⟩
            μ-shift k l (rew (delay-+ k 0 l) ((Functor.fmap (F-delay (k + 0)) (η.at A) at (k + l)) v′))
        ≡⟨ cong (λ x → μ-shift k l x) (fmap-delay-+-n+k k 0 l v′) ⟩
            μ-shift k l ((Functor.fmap (F-delay 0) (η.at A) at l) (rew (delay-+ k 0 l) v′))
        ≡⟨⟩ -- Def. of Functor.fmap (F-delay 0)
            μ-shift k l ((η.at A) l (rew (delay-+ k 0 l) v′))
        ≡⟨⟩ -- Def. of η.at
            μ-shift k l (0 , rew (delay-+ k 0 l) v′)
        ≡⟨⟩
            k + 0 , rew (sym (delay-+ k 0 l)) (rew (delay-+ k 0 l) v′)
        ≡⟨ cong (λ x → k + 0 , x) (rew-cancel v′ (delay-+ k 0 l)) ⟩
            k + 0 , rew (delay-+0-left k (k + l)) v
        ≡⟨ ≅-to-≡ {_} {◇ A at (k + l)}
            (cong₂ {A = ℕ} {_} {λ n v → ◇ A at (k + l)}
                (λ x y → x , y) (≡-to-≅ (+-identityʳ k)) (≅.sym v≅v′)) ⟩
            k , v
        ∎
        where
        v′ : delay A by (k + 0) at (k + l)
        v′ = rew (delay-+0-left k (k + l)) v
        v≅v′ : v ≅ v′
        v≅v′ = rew-to-≅ (delay-+0-left k (k + l))
        pr : (Functor.fmap (F-delay k) (η.at A) at (k + l)) v
           ≅ (Functor.fmap (F-delay (k + 0)) (η.at A) at (k + l)) v′
        pr = cong₂ (λ x y → (Functor.fmap (F-delay x) (η.at A) at (k + l)) y)
                        (≡-to-≅ (sym (+-identityʳ k))) v≅v′
        v-no-delay : A at l
        v-no-delay = rew (delay-+-left0 k l) v

    -- k = suc n + l
    η-unit2-◇ {A} {n} {.(n + suc l) , v} | fst==suc[ .n + l ] with≡ pf =
        begin
            μ.at A n (F-◇.fmap (η.at A) n (n + suc l , v))
        ≡⟨⟩
            μ.at A n (n + suc l , (Functor.fmap (F-delay (n + suc l)) (η.at A) at n) v)
        ≡⟨⟩
            μ-compare A n (n + suc l) ((Functor.fmap (F-delay (n + suc l)) (η.at A) at n) v) (compareLeq (n + suc l) n)
        ≡⟨ cong (λ x → μ-compare A n (n + suc l) ((Functor.fmap (F-delay (n + suc l)) (η.at A) at n) v) x) pf ⟩
            μ-compare A n (n + suc l) ((Functor.fmap (F-delay (n + suc l)) (η.at A) at n) v) fst==suc[ n + l ]
        ≡⟨⟩
            n + suc l , rew (delay-⊤ n l) top.tt
        ≡⟨ cong (λ x → n + suc l , x) (eq n l v) ⟩
            n + suc l , v
        ∎
        where
        eq : ∀ (n l : ℕ) -> (v : delay A by (n + suc l) at n )
          -> rew (delay-⊤ n l) top.tt
           ≡ v
        eq zero l v = refl
        eq (suc n) l v = eq n l v

    μ-assoc-◇ : {A : τ} {n : ℕ} {a : ◇ ◇ ◇ A at n}
             -> (μ.at A n (μ.at (F-◇.omap A) n a))
              ≡ (μ.at A n (F-◇.fmap (μ.at A) n a))
    μ-assoc-◇ {A} {n} {k , v} with inspect (compareLeq k n)
    -- n = k + l
    μ-assoc-◇ {A} {.(k + l)} {k , v} | snd==[ .k + l ] with≡ pf =
        begin
            μ.at A (k + l) (μ.at (F-◇.omap A) (k + l) (k , v))
        ≡⟨⟩
            μ.at A (k + l) (μ-compare (F-◇.omap A) (k + l) k v ⌞ compareLeq k (k + l) ⌟)
        ≡⟨ cong! pf ⟩
            μ.at A (k + l) (μ-compare (F-◇.omap A) (k + l) k v (snd==[ k + l ]))
        ≡⟨⟩
            μ.at A (k + l) (μ-shift k l (rew (delay-+-left0 k l) v))
        ≡⟨ ≅-to-≡ (μ-interchange {A} {l} {k} {rew (delay-+-left0 k l) v}) ⟩
            μ-shift k l (μ.at A l ⌞ rew (delay-+-left0 k l) v ⌟)
        ≡⟨ cong! (v≡v′-rew k l v v′ v≅v′) ⟩
            μ-shift k l (μ.at A l (rew (delay-+ k 0 l) v′))
        ≡⟨⟩ -- Def. of (F-delay 0).fmap
            μ-shift k l ((Functor.fmap (F-delay 0) (μ.at A) at l) (rew (delay-+ k 0 l) v′))
        ≡⟨ cong (λ x → μ-shift k l x) (sym (fmap-delay-+-n+k k 0 l v′)) ⟩
            μ-shift k l ⌞ rew (delay-+ k 0 l) ((Functor.fmap (F-delay (k + 0)) (μ.at A) at (k + l)) v′) ⌟
        ≡⟨ cong!
            (sym (delay-+-left0-eq k l ((Functor.fmap (F-delay k) (μ.at A) at (k + l)) v)
                                       ((Functor.fmap (F-delay (k + 0)) (μ.at A) at (k + l)) v′) pr))
         ⟩
            μ-shift k l (rew (delay-+-left0 k l) ((Functor.fmap (F-delay k) (μ.at A) at (k + l)) v))
        ≡⟨⟩
            μ-compare A (k + l) k ((Functor.fmap (F-delay k) (μ.at A) at (k + l)) v) (snd==[ k + l ])
        ≡⟨ cong (λ x → μ-compare A (k + l) k ((Functor.fmap (F-delay k) (μ.at A) at (k + l)) v) x) (sym pf) ⟩
            μ-compare A (k + l) k ((Functor.fmap (F-delay k) (μ.at A) at (k + l)) v) (compareLeq k (k + l))
        ≡⟨⟩
            μ.at A (k + l) (k , (Functor.fmap (F-delay k) (μ.at A) at (k + l)) v)
        ≡⟨⟩
            μ.at A (k + l) (F-◇.fmap (μ.at A) (k + l) (k , ?))
        ∎
        where
        v′ : delay (◇ ◇ A) by (k + 0) at (k + l)
        v′ = rew (delay-+0-left k (k + l)) v
        v≅v′ : v ≅ v′
        v≅v′ = rew-to-≅ (delay-+0-left k (k + l))
        pr : (Functor.fmap (F-delay k) (μ.at A) at (k + l)) v
           ≅ (Functor.fmap (F-delay (k + 0)) (μ.at A) at (k + l)) v′
        pr = ≅.cong₂ (λ x y → (Functor.fmap (F-delay x) (μ.at A) at (k + l)) y)
                (≡-to-≅ (sym (+-identityʳ k))) v≅v′
        v≡v′-rew : ∀ {A} (k l : ℕ) -> Proof-≡ (delay-+-left0 {A} k l)
                                              (delay-+ {A} k 0 l)
        v≡v′-rew zero l v v′ ≅.refl = refl
        v≡v′-rew (suc k) l = v≡v′-rew k l
    -- k = suc n + l
    μ-assoc-◇ {A} {.n} {.(n + suc l) , v} | fst==suc[ n + l ] with≡ pf =
        begin
            μ.at A n (μ.at (F-◇.omap A) n (n + suc l , v))
        ≡⟨⟩
            μ.at A n (μ-compare (F-◇.omap A) n (n + suc l) v ⌞ compareLeq (n + suc l) n ⌟)
        ≡⟨ cong! pf ⟩
            μ.at A n (μ-compare (F-◇.omap A) n (n + suc l) v (fst==suc[ n + l ]))
        ≡⟨⟩
            μ.at A n (n + suc l , rew (delay-⊤ n l) top.tt)
        ≡⟨⟩
            μ-compare A n (n + suc l) (rew (delay-⊤ n l) top.tt) ⌞ compareLeq (n + suc l) n ⌟
        ≡⟨ cong! pf ⟩
            μ-compare A n (n + suc l) (rew (delay-⊤ n l) top.tt) (fst==suc[ n + l ])
        ≡⟨⟩
            n + suc l , rew (delay-⊤ n l) top.tt
        ≡⟨⟩
            μ-compare A n (n + suc l) ((Functor.fmap (F-delay (n + suc l)) (μ.at A) at n) v) (fst==suc[ n + l ])
        ≡⟨ cong (λ x -> μ-compare A n (n + suc l) ((Functor.fmap (F-delay (n + suc l)) (μ.at A) at n) v) x) (sym pf) ⟩
            μ-compare A n (n + suc l) ((Functor.fmap (F-delay (n + suc l)) (μ.at A) at n) v) (compareLeq (n + suc l) n)
        ≡⟨⟩
            μ.at A n (n + suc l , (Functor.fmap (F-delay (n + suc l)) (μ.at A) at n) v)
        ≡⟨⟩
            μ.at A n (F-◇.fmap (μ.at A) n (n + suc l , v))
        ∎

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Ex1Sol where

----------------------------------------------------------------------------
-- EXERCISE 1 -- NUMBERS, LISTS, VECTORS (a driving lesson)
--
-- VALUE:     15%
-- DEADLINE:  5pm, Friday 2 October (week 2)
--
-- DON'T SUBMIT, COMMIT! Create your own private version of the CS410 repo,
-- hosted somewhere like BitBucket, and invite users "pigworker" and
-- "jmchapman" to collaborate with you on the project. The last version of
-- your repo committed before the deadline is the "official" version, for
-- marking purposes, but we're unlikely to penalise submission over the
-- weekend. You can trust us not to look until Monday!
--
-- The purpose of this exercise is to get you used to using Agda and its
-- emacs interface.
----------------------------------------------------------------------------

open import CS410-Prelude

-- HINT: your tasks are heralded with the eminently searchable tag, "???"

-- TIP: when you load this file, you should see 11 open goals, which is
-- too many to think about at once; use comments {- .. -} to switch off the
-- parts of the file you haven't reached yet.

----------------------------------------------------------------------------
-- "Nat" -- the type of unary natural numbers
----------------------------------------------------------------------------

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat
{-# BUILTIN NATURAL Nat #-} -- means we can write 2 for suc (suc zero)

-- TERMINOLOGY Set and "type". By "type", I mean anything you can put to
-- the right of : to classify the thing to the left of :, so "Set" is a
-- type, as in Nat : Set, and Nat is a type, as in zero : Nat. Being a
-- Set is *one* way of being a type, but it is not the only way. In
-- particular, try uncommenting this (and then change your mind).

{-+}
mySet : Set
mySet = Set
{+-}

-- SPOT THE DIFFERENCE: in Haskell, we'd write
--
-- data Nat = Zero | Suc Nat
--
-- saying what the type is called and what is in it, and then we'd find
-- that Zero :: Nat and Suc :: Nat -> Nat. Also, constructors live in a
-- separate namespace, with capital initial letters.
--
-- In Agda, we say what type each thing belongs to. Everything lives in
-- the same namespace. Capitalisation is only a social convention. I tend
-- to use capitals for typey things and lower case for valuey things.
-- And we use just the one colon for typing, not two, because types are
-- more important than lists.

----------------------------------------------------------------------------
-- ??? 1.1 addition (score: ? / 1)
--
-- There are lots of ways to add two numbers together. Do you inspect the
-- first? Do you inspect the second? Make sure you get the correct numerical
-- answer, whatever you do. You may need to revisit this problem later, when
-- the way addition works has a significant impact on types.
----------------------------------------------------------------------------

_+N_ : Nat -> Nat -> Nat
zero +N n = n
suc m +N n = suc (m +N n)
infixr 3 _+N_

-- NOTATION: a name _+N_ with underscores in it serves double duty.
-- (1) it is a perfectly sensible PREFIX operator, so _+N_ 2 2 makes sense
-- (2) it describes the INFIX usage of the operator, with the underscores
--       showing where the arguments go, with EXTRA SPACING, so the infix
--       version of _+N_ 2 2 is 2 +N 2.

-- When you think you're done, uncomment these unit tests, e.g., by turning
-- {-+} to {-(-} and {+-} to {-)-}. They should typecheck ok.
{-+}
testPlus1 : 2 +N 2 == 4
testPlus1 = refl

testPlus2 : 0 +N 5 == 5
testPlus2 = refl

testPlus3 : 5 +N 0 == 5
testPlus3 = refl
{+-}

----------------------------------------------------------------------------
-- ??? 1.2 multiplication (score: ? / 1)
--
-- There's also a lot of choice in how to multiply, but they all rely on
-- repeated addition. Find a way to do it.
----------------------------------------------------------------------------

_*N_ : Nat -> Nat -> Nat
m *N n  =  {!!}
infixr 4 _*N_

-- unit tests
{-+}
testMult1 : 2 *N 2 == 4
testMult1 = refl

testMult2 : 0 *N 5 == 0
testMult2 = refl

testMult3 : 5 *N 0 == 0
testMult3 = refl

testMult4 : 1 *N 5 == 5
testMult4 = refl

testMult5 : 5 *N 1 == 5
testMult5 = refl

testMult6 : 2 *N 3 == 6
testMult6 = refl
{+-}

----------------------------------------------------------------------------
-- ??? 1.3 subtraction I (score: ? / 1)
--
-- Subtraction is a nuisance. How do you take a big number away from a
-- smaller one? Give the closest answer you can to the correct answer.
----------------------------------------------------------------------------

_-N1_ : Nat -> Nat -> Nat
m -N1 n  =  {!!}

-- unit tests
{-+}
testSubN1-1 : 4 -N1 2 == 2
testSubN1-1 = refl

testSubN1-2 : 42 -N1 37 == 5
testSubN1-2 = refl
{+-}

----------------------------------------------------------------------------
-- "Maybe" allows for the possibility of errors
----------------------------------------------------------------------------

data Maybe (X : Set) : Set where
  yes  : X -> Maybe X
  no   : Maybe X

-- SPOT THE DIFFERENCE: in Haskell, these are "Just" and "Nothing"

-- LATER, we'll revisit Maybe and define it in terms of more basic ideas.

----------------------------------------------------------------------------
-- ??? 1.4 subtraction II (score: ? / 1)
--
-- Implement subtraction with a type acknowledging that failure can happen.
----------------------------------------------------------------------------

_-N2_ : Nat -> Nat -> Maybe Nat
m -N2 n  =  {!!}

-- unit tests
{-+}
testSubN2-1 : 4 -N2 2 == yes 2
testSubN2-1 = refl

testSubN2-2 : 42 -N2 37 == yes 5
testSubN2-2 = refl

testSubN2-3 : 37 -N2 42 == no
testSubN2-3 = refl
{+-}

----------------------------------------------------------------------------
-- _N>=_ as a relation, not a test
----------------------------------------------------------------------------

_N>=_ : Nat -> Nat -> Set      -- not Two (a.k.a. Bool), but Set
                               -- the set of "ways it can be true"
                               -- i.e., what counts as EVIDENCE
m      N>=  zero   =  One      -- anything is at least zero in a boring way
zero   N>=  suc n  =  Zero     -- no way is zero bigger than a successor
suc m  N>=  suc n  =  m N>= n  -- the way to compare successors

-- What's funny is that it's just an ordinary program, computing by
-- pattern matching and recursion.

----------------------------------------------------------------------------
-- ??? 1.5 subtraction III (score: ? / 1)
--
-- Implement subtraction with explicit evidence that the inputs are
-- amenable to subtraction.
----------------------------------------------------------------------------

_-N3_-:_ : (m : Nat) -> (n : Nat) -> m N>= n -> Nat
m -N3 n -: p  = {!!}

-- DON'T PANIC about the syntax (m : Nat) -> (n : Nat) ->
-- The type of both those arguments is Nat. However, when we write the
-- type this way, we can name those arguments for use further along in
-- the type, i.e. in the third argument. That's an example of a *dependent*
-- type. In fact, the regular syntax Nat -> is short for (_ : Nat) -> where
-- we don't bother naming the thing.

-- NOTICE that we can have fancy multi-place operators.

-- HINT: you will need to learn about the "absurd" pattern, written ().

-- unit tests
{-+}
testSubN3-1 : 4 -N3 2 -: <> == 2
testSubN3-1 = refl

testSubN3-2 : 42 -N3 37 -: <> == 5
testSubN3-2 = refl
{+-}

-- Uncomment this test and try to fill in the missing bits to make it work.
{-+}
testSubN3-3 : 37 -N3 42 -: {!!} == {!!}
testSubN3-3 = refl
{+-}
-- HAHA! YA CANNAE! So comment it out again.

-- EXTRA! You can
-- write     (m : Nat) -> (n : Nat) ->
-- as        (m : Nat)(n : Nat) ->        -- omitting all but the last ->
-- or as     (m n : Nat) ->               -- two named args sharing a type.

-- NOTICE how the defining equations for _N>=_ play a crucial role in the
-- typechecking of the above.

-- NOTICE that attempts II and III take contrasting approaches to the
-- problem with I. II broadens the output to allow failure. III narrows the
-- input to ensure success.

-- LATER, we'll see how to make the proof-plumbing less explicit

-- SUSPICIOUS: why aren't they asking us to define division?

----------------------------------------------------------------------------
-- List -- the thing that was [ .. ] in Haskell
----------------------------------------------------------------------------

data List (X : Set) : Set where  -- X scopes over the whole declaration...
  []    : List X                 -- ...so you can use it here...
  _::_  : X -> List X -> List X  -- ...and here.
infixr 3 _::_

----------------------------------------------------------------------------
-- ??? 1.6 concatenation (score: ? / 1)
----------------------------------------------------------------------------

_+L_ : {X : Set} -> List X -> List X -> List X
[] +L ys = ys
(x :: xs) +L ys = x :: (xs +L ys)
infixr 3 _+L_

-- DON'T PANIC about the "curly braces" syntax. It's very similar to the
-- (m : Nat) -> syntax we saw, above. It describes an argument by giving
-- its type, Set, and a name X to allow dependency. All the braces do is
-- set the default usage convention that X is by default INVISIBLE. Any
-- time you use the function _+L_, Agda will try to figure out what is
-- the appropriate thing to put for the invisible argument, which is the
-- element type for the lists. She will usually succeed, because the types
-- of the lists you feed in will be a dead giveaway.

-- SPOT THE DIFFERENCE: back when you learned Haskell, you learned about
-- TWO ideas, FUNCTIONS and POLYMORPHISM. Now you can see that there was
-- only ONE IDEA, after all. This sort of collapse will keep happening.
-- The world is simpler, made of a smaller number of better articulated
-- parts.

-- unit test
{-+}
testConcL  :   (0 :: 1 :: 2 :: []) +L (3 :: 4 :: [])
           ==   0 :: 1 :: 2 ::         3 :: 4 :: []
testConcL = refl
{+-}

----------------------------------------------------------------------------
-- ??? 1.7 take I (score: ? / 1)
--
-- Given a number, n, and a list, xs, compute the first n elements of xs.
-- Of course, there will be a tiny little problem if the caller asks for
-- more elements than are available, hence the name of the function.
-- You must ensure that the list returned is indeed a prefix of the list
-- supplied, and that it has the requested length if possible, and at most
-- that length if not.
----------------------------------------------------------------------------

mis-take : {X : Set} -> Nat -> List X -> List X
mis-take n xs  =  {!!}

-- unit test
{-+}
testMisTake  :   mis-take 3 (0 :: 1 :: 2 :: 3 :: 4 :: [])
             ==              0 :: 1 :: 2 :: []
testMisTake = refl
{+-}

----------------------------------------------------------------------------
-- ??? 1.8 take II (score: ? / 2)
--
-- Fix mis-take by acknowledging the possibility of error. Ensure that your
-- function returns "yes" with a list of exactly the right length if
-- possible, or says "no". You may need to use the "with" construct to
-- inspect the result of the recursive call.
----------------------------------------------------------------------------

may-take : {X : Set} -> Nat -> List X -> Maybe (List X)
may-take n xs  =  {!!}

-- unit test
{-+}
testMayTake1  :   may-take 3 (0 :: 1 :: 2 :: 3 :: 4 :: [])
              ==         yes (0 :: 1 :: 2 :: [])
testMayTake1 = refl

testMayTake2  :   may-take 6 (0 :: 1 :: 2 :: 3 :: 4 :: [])
              ==  no
testMayTake2 = refl

testMayTake3  :   may-take 5 (0 :: 1 :: 2 :: 3 :: 4 :: [])
              ==         yes (0 :: 1 :: 2 :: 3 :: 4 :: [])
testMayTake3 = refl
{+-}

----------------------------------------------------------------------------
-- ??? 1.9 length (score: ? / 1)
----------------------------------------------------------------------------

-- Show how to compute the length of a list.

length : {X : Set} -> List X -> Nat
length xs = {!!}

-- unit test
{-+}
testLength  :  length (0 :: 1 :: 2 :: 3 :: 4 :: [])  ==  5
testLength  =  refl
{+-}

----------------------------------------------------------------------------
-- "Vectors" -- Lists indexed by length
----------------------------------------------------------------------------

-- We seem to be troubled by things fouling up when lists have the wrong
-- length. Here's a way to make list-like structures whose types let us
-- keep tabs on length: the "vectors".

data Vec (X : Set) : (n : Nat) -> Set where -- n's not in scope after "where"
  []    : Vec X zero                                  -- it's zero here,...
  _::_  : {n : Nat} -> X -> Vec X n -> Vec X (suc n)  -- ...successor, there

-- DON'T PANIC
-- Vec X is not a Set, but rather an INDEXED FAMILY of sets. For each n in
-- Nat, Vec X n is a Set. The index, n, is the length. The constructors are
-- just like those of List, except that their types also tell the truth
-- about length, via the index.

-- NOTICE that when we write a "cons", x :: xs, the length of the tail, xs,
-- is an invisible argument.

-- DON'T PANIC about the reuse of constructor names. We're usually starting
-- with types and working towards code, so it is almost always clear which
-- type's constructors we mean.

-- SUSPICION: we declared List, then wrote length, then invented Vec.
-- Perhaps there is some way to say "Vec is List indexed by length" and
-- have it invented for us.

----------------------------------------------------------------------------
-- ??? 1.10 concatenation (score: ? / 1)
----------------------------------------------------------------------------

-- When we concatenate vectors, we add their lengths.

_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V ys = ys
(x :: xs) +V ys = x :: (xs +V ys)
infixr 3 _+V_

-- NOTICE that even though m and n are numbers, not types, they can
-- still be invisible.

-- DON'T PANIC if this doesn't work out to be just as easy (or even easier)
-- than for lists. You may need to tinker with your definition of _+N_ to
-- make _+V_ typecheck smoothly. That's because the defining equations for
-- _+N_ are all the typechecker has to go on when seeing that your code
-- here fits together properly.

-- unit test
{-+}
testConcV  :   (0 :: 1 :: 2 :: []) +V (3 :: 4 :: [])
           ==   0 :: 1 :: 2 ::         3 :: 4 :: []
testConcV = refl
{+-}

----------------------------------------------------------------------------
-- ??? 1.11 take (score: ? / 2)
----------------------------------------------------------------------------

-- Now we know the lengths, we can give a PRECONDITION for taking.

take : {X : Set}{m : Nat}(n : Nat) -> m N>= n -> Vec X m -> Vec X n
take n p xs = {!!}

-- unit test
{-+}
testTake1  :  take 3 <> (0 :: 1 :: 2 :: 3 :: 4 :: [])
              ==         0 :: 1 :: 2 :: []
testTake1 = refl

testTake3  :  take 5 <> (0 :: 1 :: 2 :: 3 :: 4 :: [])
              ==         0 :: 1 :: 2 :: 3 :: 4 :: []
testTake3 = refl
{+-}

-- check you can't finish this
{-+}
testTake2  :  take 6 {!!} (0 :: 1 :: 2 :: 3 :: 4 :: [])
              ==  {!!}
testTake2 = refl
{+-}

----------------------------------------------------------------------------
-- Chopping: one last wild weird new thing
----------------------------------------------------------------------------

-- Here's a thing you'd struggle to do in Haskell. It's really about seeing.
-- A vector of length m +N n is "Choppable" if you can show how it is given
-- by concatenating a vector of length m and a vector of length n.

data Choppable {X : Set}(m n : Nat) : Vec X (m +N n) -> Set where
  chopTo : (xs : Vec X m)(ys : Vec X n) -> Choppable m n (xs +V ys)

----------------------------------------------------------------------------
-- ??? 1.12 chop (score: ? / 2)
----------------------------------------------------------------------------

chop : {X : Set}(m n : Nat)(xs : Vec X (m +N n)) -> Choppable m n xs
chop zero n xs = chopTo [] xs
chop (suc m) n (x :: xs) with chop m n xs
chop (suc m) n (x :: .(xs +V ys)) | chopTo xs ys = chopTo (x :: xs) ys

-- DON'T PANIC if you can't pattern match on the vector right away, because
-- the fact is that without looking at WHERE TO CHOP, you don't know if you
-- need to.

-- HINT You can access vectors only from the "left end", which is a big
-- clue about which number you should inspect.

-- HINT Much like in -N2 and may-take, you will probably benefit from using
-- the "with" feature to allow you to match on the outcome of a recursive
-- call.

-- DON'T PANIC if dotty things appear spontaneously in your patterns. That's
-- knowledge for free: the pattern checker is saying "you don't need to ask,
-- because I know that the only thing which goes here is such-and-such".

-- unit test

{-+}
testChop  :   chop 3 2 (0 :: 1 :: 2 :: 3 :: 4 :: [])
          ==  chopTo (0 :: 1 :: 2 :: []) (3 :: 4 :: [])
testChop = refl
{+-}

-- SUSPICION: unit tests may, in this case, be a little beside the point

-- TERMINOLOGY: we call this method "constructing a view" of vectors. The
-- datatype Choppable explains how we would like to be able to look at
-- vectors. The chop function *proves* that we always can. We get for free
-- that we can look at vectors as being made by [] and _::_, but now we
-- can PROGRAM new ways of looking: vectors as made by _+V_.

-- Welcome to the new programming.


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

module Homotopy_Equivalence where

open import Basic_Types
open import Identity

-- ------------------------------------
-- In homotopy type theory, a homotopy is just a point-wise equality (path)
-- between to (dependent) functions f and g
infix  2 _~_

_~_ : ∀ {A : Set} {B : A → Set} → ∀ (f g : ∀ (x : A) → B x) → Set
_~_ {A} f g = ∀ (x : A) → f x ≡ g x

-- operations on homotopies, which give them groupoid-like structures
hp-refl : ∀ {A : Set} {B : A → Set} → ∀ (f : ∀ (a : A) → B a) → f ~ f
hp-refl {A} f = λ (x : A) → refl (f x)

hp-inv : ∀ {A : Set} {B : A → Set} {f g : ∀ (a : A) → B a} → f ~ g → g ~ f
hp-inv {A} H = λ (x : A) → inv (H x)

hp-concat : ∀ {A : Set} {B : A → Set} {f g h : ∀ (a : A) → B a} →
            f ~ g → g ~ h → f ~ h
hp-concat {A} H K = λ (x : A) → (H x) ∙ (K x)

-- naturality of homotopies
<<<<<<< HEAD
hpna : ∀ {A B : Set} {x y : A} → ∀ (p : x ≡ y) → ∀ (f g : A → B) → ∀ (H : f ~ g) →
       (H x) ∙ (ap g p) ≡ (ap f p) ∙ (H y)
hpna {_} {_} {x} {x} (refl x) f g H = (right_unit (H x)) ∙ (inv (left_unit (H x)))

=======

>>>>>>> a0dc66dca08059f740d9290f3d1cad1bb007d721
infix  3 _·_

_·_ : ∀ {A : Set} {B : A → Set} {f g h : ∀ (a : A) → B a} →
      f ~ g → g ~ h → f ~ h
H · K = hp-concat H K

hp-ass : ∀ {A : Set} {B : A → Set} {f g h k : ∀ (a : A) → B a} →
         ∀ (H : f ~ g) (K : g ~ h) (L : h ~ k) → H · (K · L) ~ (H · K) · L
hp-ass {A} H K L = λ (x : A) → p-ass (H x) (K x) (L x)

hp-left_unit : ∀ {A : Set} {B : A → Set} {f g : ∀ (a : A) → B a} →
               ∀ (H : f ~ g) → (hp-refl f) · H ~ H
hp-left_unit {A} H = λ (x : A) → left_unit (H x)

hp-right_unit : ∀ {A : Set} {B : A → Set} {f g : ∀ (a : A) → B a} →
                ∀ (H : f ~ g) → H · (hp-refl g) ~ H
hp-right_unit {A} H = λ (x : A) → right_unit (H x)

-- whiskering operations
whis-r : ∀ {A B C : Set} {f g : A → B} → ∀ (H : f ~ g) → ∀ (h : B → C) →
         (comp h f) ~ (comp h g)
<<<<<<< HEAD
whis-r {A} H h = λ (x : A) → ap h (H x)
=======
whis-f {A} h H = λ (x : A) → ap h (H x)
>>>>>>> a0dc66dca08059f740d9290f3d1cad1bb007d721

whis-l : ∀ {A B C : Set} {g h : B → C} → ∀ (H : g ~ h) → ∀ (f : A → B) →
         (comp g f) ~ (comp h f)
whis-l {A} H f = λ (x : A) → H (f x)

-- ------------------------------------
-- equivalences
-- first, let's consider quasi-equivalences
qinv : ∀ {A B : Set} → ∀ (f : A → B) → Set
qinv {A} {B} f = Σ g ∶ (B → A) , (((comp f g) ~ id) × ((comp g f) ~ id))

isequiv : ∀ {A B : Set} → ∀ (f : A → B) → Set
isequiv {A} {B} f = (Σ g ∶ (B → A) , ((comp f g) ~ id)) × (Σ h ∶ (B → A) , ((comp h f) ~ id))

isequivid : ∀ {A : Set} → isequiv (id {A})
isequivid {A} = ((id {A} , hp-refl (id {A})) , (id {A} , hp-refl (id {A})))

-- the relation between quasi-inverse and equivalence is as following:
q→e : ∀ {A B : Set} → ∀ (f : A → B) → qinv f → isequiv f
q→e f q = ((π₁ q , π₁ (π₂ q)) , (π₁ q , π₂ (π₂ q)))

e→q : ∀ {A B : Set} → ∀ (f : A → B) → isequiv f → qinv f
e→q {A} {B} f ((g , fgid) , (h , hfid)) = (comp h (comp f g) , (e→q1 , e→q2))
  where e→q1 : comp f (comp h (comp f g)) ~ id
        e→q1 = (whis-l {B} {A} {B} (whis-r {A} {A} {B} hfid f) g) · fgid
        e→q2 : comp (comp h (comp f g)) f ~ id
        e→q2 = (whis-l {A} {B} {A} (whis-r {B} {B} {A} fgid h) f) · hfid
-- the above two lemmas shows that quasi-equivalence and equivalence are
-- logically equivalent

-- ------------------------------------
-- type equivalence
infix  3 _≃_

_≃_ : ∀ (A B : Set) → Set
A ≃ B = Σ f ∶ (A → B) , (isequiv f)

-- type equivalence is an equivalence relation on Set
≃-refl : ∀ (A : Set) → A ≃ A
≃-refl A = id {A} , isequivid {A}

-- ------------------------------------
-- The higher groupoid structure of type formers
-- Cartesian product types
p×1 : ∀ {A B : Set} {x y : A × B} → x ≡ y → π₁ x ≡ π₁ y
p×1 {_} {_} {x} {x} (refl x) = refl (π₁ x)

p×2 : ∀ {A B : Set} {x y : A × B} → x ≡ y → π₂ x ≡ π₂ y
p×2 {_} {_} {x} {x} (refl x) = refl (π₂ x)

p≡p× : ∀ {A B : Set} {x y : A × B} → ∀ (p : x ≡ y) → (π₁ x ≡ π₁ y) × (π₂ x ≡ π₂ y)
p≡p× = λ p → (p×1 p , p×2 p)

p×≡p : ∀ {A B : Set} {x1 y1 : A} {x2 y2 : B} →
      ((x1 ≡ y1) × (x2 ≡ y2)) → (x1 , x2) ≡ (y1 , y2)
p×≡p {_} {_} {x1} {x1} {x2} {x2} (refl x1 , refl x2) = refl (x1 , x2)


text:
open import Numeral.Natural
open import Relator.Equals
open import Type.Properties.Decidable
open import Type

module Formalization.ClassicalPredicateLogic.Semantics
  {ℓₘ ℓₚ ℓᵥ ℓₒ}
  (Prop : ℕ → Type{ℓₚ})
  (Var : Type{ℓᵥ}) ⦃ var-eq-dec : Decidable(2)(_≡_ {T = Var}) ⦄
  (Obj : ℕ → Type{ℓₒ})
  where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.ListSized
import      Data.ListSized.Functions as List
open import Formalization.ClassicalPredicateLogic.Syntax(Prop)(Var)(Obj)
open import Functional using (_∘_ ; _∘₂_)
import      Logic.Propositional as Logic
import      Logic.Predicate     as Logic
open import Sets.PredicateSet using (PredSet)
open        Sets.PredicateSet.BoundedQuantifiers
open import Syntax.Function
open import Type.Dependent renaming (intro to _,_)
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level

module _ where
  private variable P : Type{ℓₚ}
  private variable n : ℕ

  -- Model.
  -- A model decides which propositional constants that are true or false.
  record Model : Type{ℓₚ Lvl.⊔ ℓₒ Lvl.⊔ ℓᵥ Lvl.⊔ Lvl.𝐒(ℓₘ)} where
    field
      Domain : Type{ℓₘ}
      function : Obj(n) → List(Domain)(n) → Domain
      predicate : Prop(n) → List(Domain)(n) → Bool

  private variable 𝔐 : Model

  -- Also called: Variable assignment.
  VarMapping : Model → Type
  VarMapping(𝔐) =  Var → Model.Domain(𝔐)

  mapSingle : VarMapping(𝔐) → Var → Model.Domain(𝔐) → VarMapping(𝔐)
  mapSingle 𝔰 x t y =
    if decide(2)(_≡_) ⦃ var-eq-dec ⦄ x y
    then t
    else 𝔰(y)

  private variable 𝔰 : VarMapping(𝔐)

  module _ ((𝔐 , 𝔰) : Σ Model VarMapping) where
    val : Term → Model.Domain(𝔐)
    val₊ : List(Term)(n) → List(Model.Domain(𝔐))(n)

    val(var v)    = 𝔰(v)
    val(func f x) = Model.function 𝔐 f (val₊ x)
    val₊ {0}       ∅       = ∅
    val₊ {𝐒(n)} (t ⊰ ts) = (val t ⊰ val₊ {n} ts)
    --val₊ = List.map val

  -- Satisfication relation.
  -- ((𝔐 , 𝔰) ⊧ φ) means that the formula φ is satisfied in the model 𝔐 with the variable mapping.
  -- Or in other words: A formula is true in the model 𝔐.
  _⊧_ : (Σ Model VarMapping) → Formula → Type{ℓₘ}
  (𝔐 , 𝔰) ⊧ (f $ x)  = Lvl.Up(IsTrue(Model.predicate 𝔐 f (val₊(𝔐 , 𝔰) x)))  -- A model decides whether a relation is satisfied.
  (𝔐 , 𝔰) ⊧ ⊤        = Unit                                                 -- All models satisfy top.
  (𝔐 , 𝔰) ⊧ ⊥        = Empty                                                -- No model satisfies bottom.
  (𝔐 , 𝔰) ⊧ (φ ∧ ψ)  = ((𝔐 , 𝔰) ⊧ φ) Logic.∧ ((𝔐 , 𝔰) ⊧ ψ)                  -- A model satisfies a conjunction when it satisfies both of the propositions.
  (𝔐 , 𝔰) ⊧ (φ ∨ ψ)  = ((𝔐 , 𝔰) ⊧ φ) Logic.∨ ((𝔐 , 𝔰) ⊧ ψ)                  -- A model satisfies a disjunction when it satisfies any one of the propositions.
  (𝔐 , 𝔰) ⊧ (φ ⟶ ψ)  = Logic.¬((𝔐 , 𝔰) ⊧ φ) Logic.∨ ((𝔐 , 𝔰) ⊧ ψ)
  (𝔐 , 𝔰) ⊧ (Ɐ(x) φ) = Logic.∀ₗ(t ↦ (𝔐 , mapSingle{𝔐 = 𝔐} 𝔰 x t) ⊧ φ)
  (𝔐 , 𝔰) ⊧ (∃(x) φ) = Logic.∃(t ↦ (𝔐 , mapSingle{𝔐 = 𝔐} 𝔰 x t) ⊧ φ)

  -- Satisfication of a set of formulas.
  -- This means that a model satisfies all formulas at the same time.
  _⊧₊_ : (Σ Model VarMapping) → PredSet{ℓ}(Formula) → Type
  𝔐 ⊧₊ Γ = ∀ₛ(Γ) (𝔐 ⊧_)

  -- Validity of a formula.
  -- A formula is valid when it is true independent of any model.
  Valid : Formula → Type
  Valid(φ) = Logic.∀ₗ(_⊧ φ)

  -- Satisfiability of sets of formulas.
  -- A set of formulas is valid when there is a model that satisfies all of them at the same time.
  Satisfiable : PredSet{ℓ}(Formula) → Type
  Satisfiable(Γ) = Logic.∃(_⊧₊ Γ)

  -- Unsatisfiability of sets of formulas.
  Unsatisfiable : PredSet{ℓ}(Formula) → Type
  Unsatisfiable{ℓ} = Logic.¬_ ∘ Satisfiable{ℓ}

  -- Semantic entailment of a formula.
  -- A hypothetical statement. If a model would satisfy all formulas in Γ, then this same model satisifes the formula φ.
  _⊨_ : PredSet{ℓ}(Formula) → Formula → Type
  Γ ⊨ φ = ∀{𝔐} → (𝔐 ⊧₊ Γ) → (𝔐 ⊧ φ)

  _⊭_ : PredSet{ℓ}(Formula) → Formula → Type
  _⊭_ = (Logic.¬_) ∘₂ (_⊨_)

  -- Axiomatization of a theory by a set of axioms.
  -- A set of axioms is a set of formulas.
  -- A theory is the closure of a set of axioms.
  -- An axiomatization is a subset of formulas of the theory which entails all formulas in the axiomatized theory.
  _axiomatizes_ : PredSet{ℓ₁}(Formula) → PredSet{ℓ₂}(Formula) → Type
  Γ₁ axiomatizes Γ₂ = ∀{φ} → (Γ₁ ⊨ φ) → Γ₂(φ)

  -- A set of formulas is closed when it includes all formulas that it entails.
  Closed : PredSet{ℓ}(Formula) → Type
  Closed(Γ) = Γ axiomatizes Γ

  _⊨₊_ : PredSet{ℓ₁}(Formula) → PredSet{ℓ₂}(Formula) → Type
  Γ₁ ⊨₊ Γ₂ = ∀{𝔐} → (𝔐 ⊧₊ Γ₁) → (𝔐 ⊧₊ Γ₂)

  _⊭₊_ : PredSet{ℓ₁}(Formula) → PredSet{ℓ₂}(Formula) → Type
  _⊭₊_ = (Logic.¬_) ∘₂ (_⊨₊_)

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples of how to use non-trivial induction over the natural
-- numbers.
------------------------------------------------------------------------

module README.Data.Nat.Induction where

open import Data.Nat
open import Data.Nat.Induction
open import Data.Product using (_,_)
open import Function using (_∘_)
open import Induction.WellFounded
open import Relation.Binary.PropositionalEquality

-- Doubles its input.

twice : ℕ → ℕ
twice = rec _ λ
  { zero    _       → zero
  ; (suc n) twice-n → suc (suc twice-n)
  }

-- Halves its input (rounding downwards).
--
-- The step function is mentioned in a proof below, so it has been
-- given a name. (The mutual keyword is used to avoid having to give
-- a type signature for the step function.)

mutual

  half₁-step = λ
    { zero          _                → zero
    ; (suc zero)    _                → zero
    ; (suc (suc n)) (_ , half₁n , _) → suc half₁n
    }

  half₁ : ℕ → ℕ
  half₁ = cRec _ half₁-step

-- An alternative implementation of half₁.

mutual

  half₂-step = λ
    { zero          _   → zero
    ; (suc zero)    _   → zero
    ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl))
    }

  half₂ : ℕ → ℕ
  half₂ = <′-rec _ half₂-step

-- The application half₁ (2 + n) is definitionally equal to
-- 1 + half₁ n. Perhaps it is instructive to see why.

half₁-2+ : ∀ n → half₁ (2 + n) ≡ 1 + half₁ n
half₁-2+ n = begin

  half₁ (2 + n)                                                         ≡⟨⟩

  cRec _ half₁-step (2 + n)                                             ≡⟨⟩

  half₁-step (2 + n) (cRecBuilder _ half₁-step (2 + n))                 ≡⟨⟩

  half₁-step (2 + n)
    (let ih = cRecBuilder _ half₁-step (1 + n) in
     half₁-step (1 + n) ih , ih)                                        ≡⟨⟩

  half₁-step (2 + n)
    (let ih = cRecBuilder _ half₁-step n in
     half₁-step (1 + n) (half₁-step n ih , ih) , half₁-step n ih , ih)  ≡⟨⟩

  1 + half₁-step n (cRecBuilder _ half₁-step n)                         ≡⟨⟩

  1 + cRec _ half₁-step n                                               ≡⟨⟩

  1 + half₁ n                                                           ∎

  where open ≡-Reasoning

-- The application half₂ (2 + n) is definitionally equal to
-- 1 + half₂ n. Perhaps it is instructive to see why.

half₂-2+ : ∀ n → half₂ (2 + n) ≡ 1 + half₂ n
half₂-2+ n = begin

  half₂ (2 + n)                                               ≡⟨⟩

  <′-rec _ half₂-step (2 + n)                                 ≡⟨⟩

  half₂-step (2 + n) (<′-recBuilder _ half₂-step (2 + n))     ≡⟨⟩

  1 + <′-recBuilder _ half₂-step (2 + n) n (≤′-step ≤′-refl)  ≡⟨⟩

  1 + Some.wfRecBuilder _ half₂-step (2 + n)
        (<′-wellFounded (2 + n)) n (≤′-step ≤′-refl)          ≡⟨⟩

  1 + Some.wfRecBuilder _ half₂-step (2 + n)
        (acc (<′-wellFounded′ (2 + n))) n (≤′-step ≤′-refl)   ≡⟨⟩

  1 + half₂-step n
        (Some.wfRecBuilder _ half₂-step n
           (<′-wellFounded′ (2 + n) n (≤′-step ≤′-refl)))     ≡⟨⟩

  1 + half₂-step n
        (Some.wfRecBuilder _ half₂-step n
           (<′-wellFounded′ (1 + n) n ≤′-refl))               ≡⟨⟩

  1 + half₂-step n
        (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩

  1 + half₂-step n (<′-recBuilder _ half₂-step n)             ≡⟨⟩

  1 + <′-rec _ half₂-step n                                   ≡⟨⟩

  1 + half₂ n                                                 ∎

  where open ≡-Reasoning

-- Some properties that the functions above satisfy, proved using
-- cRec.

half₁-+₁ : ∀ n → half₁ (twice n) ≡ n
half₁-+₁ = cRec _ λ
  { zero          _                        → refl
  ; (suc zero)    _                        → refl
  ; (suc (suc n)) (_ , half₁twice-n≡n , _) →
      cong (suc ∘ suc) half₁twice-n≡n
  }

half₂-+₁ : ∀ n → half₂ (twice n) ≡ n
half₂-+₁ = cRec _ λ
  { zero          _                        → refl
  ; (suc zero)    _                        → refl
  ; (suc (suc n)) (_ , half₁twice-n≡n , _) →
      cong (suc ∘ suc) half₁twice-n≡n
  }

-- Some properties that the functions above satisfy, proved using
-- <′-rec.

half₁-+₂ : ∀ n → half₁ (twice n) ≡ n
half₁-+₂ = <′-rec _ λ
  { zero          _   → refl
  ; (suc zero)    _   → refl
  ; (suc (suc n)) rec →
      cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
  }

half₂-+₂ : ∀ n → half₂ (twice n) ≡ n
half₂-+₂ = <′-rec _ λ
  { zero          _   → refl
  ; (suc zero)    _   → refl
  ; (suc (suc n)) rec →
      cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
  }


text:
{-# OPTIONS --without-K #-}
module LeftCancellation where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product using (_,_; _,′_; proj₁; proj₂)
open import Function renaming (_∘_ to _○_)

-- explicit 'using', to show how little of HoTT is needed
open import SimpleHoTT using (refl; ap; _∘_; !; _≡_; _≡⟨_⟩_ ; _∎)
open import Equivalences
open import TypeEquivalences using (swap₊)
open import Inspect

----------------------------------------------------------------------------
-- Very complex proof that we can cancel units on the left of ⊎

-- Some repeated patterns:
-- use injectivity of equivalences to go from f x ≡ f y to x ≡ y
injectivity : {A B : Set} (equiv : (⊤ ⊎ A) ≃ (⊤ ⊎ B)) → (a : A) → equiv ⋆ inj₁ tt ≡ equiv ⋆ inj₂ a → (inj₁ tt ≡ inj₂ a)
injectivity equiv x path = inj≃ equiv (inj₁ tt) (inj₂ x) path

-- Use that disjoint unions are, well, disjoint, to derive a contradiction
bad-path : {A : Set} → (x : A) → inj₁ tt ≡ inj₂ x → ⊥
bad-path x path = proj₁ (thm2-12-5 tt (inj₂ x)) path

left-cancel-⊤ : {A B : Set} →  ((⊤ ⊎ A) ≃ (⊤ ⊎ B)) → A ≃ B
left-cancel-⊤ {A} {B}  (f₁ , mkisequiv g₁ α₁ h₁ β₁) with f₁ (inj₁ tt) | inspect f₁ (inj₁ tt) | g₁ (inj₁ tt) | inspect g₁ (inj₁ tt)
left-cancel-⊤ {A} {B} (f₁ , mkisequiv g₁ α₁ h₁ β₁) | inj₁ tt | ⟪ eq₁ ⟫ | inj₁ tt | ⟪ eq₂ ⟫ = f , equiv₁ (mkqinv g α β)
  where equiv = (f₁ , mkisequiv g₁ α₁ h₁ β₁)
        f : A → B
        f a with f₁ (inj₂ a) | inspect f₁ (inj₂ a)
        f a | inj₂ b  | _ = b
        f a | inj₁ tt | ⟪ eq ⟫ with bad-path a inject
          where inject = injectivity equiv a (eq₁ ∘ ! eq)
        f a | inj₁ tt | ⟪ eq ⟫ | ()
        g : B → A
        g b with g₁ (inj₂ b) | inspect g₁ (inj₂ b)
        g b | inj₂ a  | _ = a
        g b | inj₁ tt | ⟪ eq ⟫ with bad-path b inject
          where inject = injectivity (sym≃ equiv) b (eq₂ ∘ ! eq)
        g b | inj₁ tt | ⟪ eq ⟫ | ()
        α : f ○ g ∼ id
        α b with g₁ (inj₂ b) | inspect g₁ (inj₂ b)
        α b | inj₁ tt | ⟪ eq ⟫ with bad-path b inject
          where inject = injectivity (sym≃ equiv) b (eq₂ ∘ ! eq)
        α b | inj₁ tt | ⟪ eq ⟫ | ()
        α b | inj₂ a  | ⟪ eq ⟫ with f₁ (inj₂ a) | inspect f₁ (inj₂ a)
        α b | inj₂ a | ⟪ eq ⟫ | inj₁ tt | ⟪ eq₃ ⟫ with bad-path a inject
          where inject = injectivity equiv a (eq₁ ∘ ! eq₃)
        α b | inj₂ a | ⟪ eq ⟫ | inj₁ tt | ⟪ eq₃ ⟫ | ()
        α b | inj₂ a | ⟪ eq ⟫ | inj₂ b′ | ⟪ eq₃ ⟫ =
            proj₁ (inj₁₁path b′ b) (ap swap₊ (! (ap f₁ eq ∘ eq₃) ∘ α₁ (inj₂ b)))
        β : g ○ f ∼ id
        β a with f₁ (inj₂ a) | inspect f₁ (inj₂ a)
        β a | inj₁ tt | ⟪ eq ⟫ with bad-path a inject
          where inject = injectivity equiv a (! (eq ∘ ! eq₁))
        ... | ()
        β a | inj₂ b | ⟪ eq ⟫ with g₁ (inj₂ b) | inspect g₁ (inj₂ b)
        ... | inj₁ tt | ⟪ eq₃ ⟫ with bad-path a inject
          where inject = injectivity equiv a (! (ap f₁ eq₃) ∘ (α₁ (inj₂ b)) ∘ ! eq)
        β a | inj₂ b | ⟪ eq ⟫ | inj₁ tt | ⟪ eq₃ ⟫ | ()
        β a | inj₂ b | ⟪ eq ⟫ | inj₂ a′ | ⟪ eq₃ ⟫ = proj₁ (inj₁₁path a′ a) (ap swap₊ ((! eq₃) ∘ ap g₁ (! eq) ∘ β₂ (inj₂ a)))
            where module EQ = qinv (equiv₂ {f = f₁} (proj₂ equiv))
                  β₂ = EQ.β

left-cancel-⊤ (f₁ , mkisequiv g α h β) | inj₁ tt | ⟪ eq₁ ⟫ | inj₂ a | ⟪ eq₂ ⟫ with bad-path a inject
  where equiv = (f₁ , mkisequiv g α h β)
        inject = injectivity equiv a (eq₁ ∘ ! (α (inj₁ tt)) ∘ (ap f₁ eq₂))
left-cancel-⊤ (f₁ , mkisequiv g α h β) | inj₁ tt | ⟪ eq₁ ⟫ | inj₂ a | ⟪ eq₂ ⟫ | ()

left-cancel-⊤ (f₁ , mkisequiv g α h β) | inj₂ b | ⟪ eq₁ ⟫ | inj₁ tt | ⟪ eq₂ ⟫ with bad-path b (! (α (inj₁ tt)) ∘ (ap f₁ eq₂) ∘ eq₁ )
... | ()
left-cancel-⊤ {A} {B} (f₁ , mkisequiv g₁ α₁ h₁ β₁) | inj₂ b₁ | ⟪ eq₁ ⟫ | inj₂ a₁ | ⟪ eq₂ ⟫ = f , equiv₁ (mkqinv g α β)
  where equiv = (f₁ ,′ mkisequiv g₁ α₁ h₁ β₁)
        module EQ = qinv (equiv₂ {f = f₁} (proj₂ equiv))
        β₂ = EQ.β
        f : A → B
        f a with f₁ (inj₂ a)
        f a | inj₂ b′  = b′
        f a | inj₁ tt  = b₁
        g : B → A
        g b with g₁ (inj₂ b)
        g b | inj₂ a′ = a′
        g b | inj₁ tt = a₁
        α : f ○ g ∼ id
        α b with g₁ (inj₂ b) | inspect g₁ (inj₂ b)
        ... |  inj₂ a′ | ⟪ eq ⟫ with f₁ (inj₂ a′) | inspect f₁ (inj₂ a′)
        ...     | inj₂ b′ | ⟪ eq₃ ⟫ = ! (proj₁ (inj₁₁path b b′) (ap swap₊ (! (α₁ (inj₂ b)) ∘ ap f₁ eq ∘ eq₃)))
        ...     | inj₁ tt | ⟪ eq₃ ⟫ with bad-path b (! (! (α₁ (inj₂ b)) ∘ (ap f₁ eq) ∘ eq₃))
        α b | inj₂ a′ | ⟪ eq ⟫ | inj₁ tt | ⟪ eq₃ ⟫ | ()
        α b | inj₁ tt | ⟪ eq ⟫ with f₁ (inj₂ a₁) | inspect f₁ (inj₂ a₁)
        α b | inj₁ tt | ⟪ eq ⟫ | inj₁ tt | ⟪ eq₃ ⟫ = proj₁ (inj₁₁path b₁ b) (ap swap₊ (!(! (α₁ (inj₂ b)) ∘ ap f₁ eq ∘ eq₁)))
        α b | inj₁ tt | ⟪ eq ⟫ | inj₂ b′ | ⟪ eq₃ ⟫ with bad-path b′ (! (α₁ (inj₁ tt)) ∘ ap f₁ eq₂ ∘ eq₃)
        ... | ()
        β : g ○ f ∼ id
        β a with f₁ (inj₂ a) | inspect f₁ (inj₂ a)
        β a | inj₁ tt | ⟪ eq ⟫ with g₁ (inj₂ b₁) | inspect g₁ (inj₂ b₁)
        ...    | inj₁ tt | ⟪ eq₃ ⟫ = proj₁ (inj₁₁path a₁ a) (ap swap₊ (! eq₂ ∘ ! (ap g₁ eq) ∘ β₂ (inj₂ a)))
        β a | inj₁ tt | ⟪ eq ⟫ | inj₂ a′ | ⟪ eq₃ ⟫ with bad-path a′ ((! (β₂ (inj₁ tt)) ∘ ap g₁ eq₁) ∘ eq₃)
        ... | ()
        β a | inj₂ b | ⟪ eq ⟫ with g₁ (inj₂ b) | inspect g₁ (inj₂ b)
        β a | inj₂ b | ⟪ eq₃ ⟫ | inj₁ tt | ⟪ eq ⟫ with bad-path a (! eq ∘ ap g₁ (! eq₃) ∘ β₂ (inj₂ a))
        ... | ()
        β a | inj₂ b | ⟪ eq₃ ⟫ | inj₂ a′ | ⟪ eq ⟫ = proj₁ (inj₁₁path a′ a) (ap swap₊ (! eq ∘ ap g₁ (! eq₃) ∘ β₂ (inj₂ a)))

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{- Basic theory about transport:

- transport is invertible
- transport is an equivalence ([pathToEquiv])

-}
{-# OPTIONS --safe #-}
module Cubical.Foundations.Transport where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Function using (_∘_)

-- Direct definition of transport filler, note that we have to
-- explicitly tell Agda that the type is constant (like in CHM)
transpFill : ∀ {ℓ} {A : Type ℓ}
             (φ : I)
             (A : (i : I) → Type ℓ [ φ ↦ (λ _ → A) ])
             (u0 : outS (A i0))
           → --------------------------------------
             PathP (λ i → outS (A i)) u0 (transp (λ i → outS (A i)) φ u0)
transpFill φ A u0 i = transp (λ j → outS (A (i ∧ j))) (~ i ∨ φ) u0

transport⁻ : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → B → A
transport⁻ p = transport (λ i → p (~ i))

subst⁻ : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) → B y → B x
subst⁻ B p pa = transport⁻ (λ i → B (p i)) pa

transport-fillerExt : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B)
                    → PathP (λ i → A → p i) (λ x → x) (transport p)
transport-fillerExt p i x = transport-filler p x i

transport⁻-fillerExt : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B)
                     → PathP (λ i → p i → A) (λ x → x) (transport⁻ p)
transport⁻-fillerExt p i x = transp (λ j → p (i ∧ ~ j)) (~ i) x

transport-fillerExt⁻ : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B)
                    → PathP (λ i → p i → B) (transport p) (λ x → x)
transport-fillerExt⁻ p = symP (transport⁻-fillerExt (sym p))

transport⁻-fillerExt⁻ : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B)
                     → PathP (λ i → B → p i) (transport⁻ p) (λ x → x)
transport⁻-fillerExt⁻ p = symP (transport-fillerExt (sym p))

transport⁻-filler : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) (x : B)
                   → PathP (λ i → p (~ i)) x (transport⁻ p x)
transport⁻-filler p x = transport-filler (λ i → p (~ i)) x

transport⁻Transport : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (a : A) →
                          transport⁻ p (transport p a) ≡ a
transport⁻Transport p a j = transport⁻-fillerExt p (~ j) (transport-fillerExt p (~ j) a)

transportTransport⁻ : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (b : B) →
                        transport p (transport⁻ p b) ≡ b
transportTransport⁻ p b j = transport-fillerExt⁻ p j (transport⁻-fillerExt⁻ p j b)

substEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {a a' : A} (P : A → Type ℓ') (p : a ≡ a') → P a ≃ P a'
substEquiv P p = (subst P p , isEquivTransport (λ i → P (p i)))

liftEquiv : ∀ {ℓ ℓ'} {A B : Type ℓ} (P : Type ℓ → Type ℓ') (e : A ≃ B) → P A ≃ P B
liftEquiv P e = substEquiv P (ua e)

transpEquiv : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) → ∀ i → p i ≃ B
transpEquiv P i .fst = transp (λ j → P (i ∨ j)) i
transpEquiv P i .snd
  = transp (λ k → isEquiv (transp (λ j → P (i ∨ (j ∧ k))) (i ∨ ~ k)))
      i (idIsEquiv (P i))

uaTransportη : ∀ {ℓ} {A B : Type ℓ} (P : A ≡ B) → ua (pathToEquiv P) ≡ P
uaTransportη P i j
  = Glue (P i1) λ where
      (j = i0) → P i0 , pathToEquiv P
      (i = i1) → P j , transpEquiv P j
      (j = i1) → P i1 , idEquiv (P i1)

pathToIso : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → Iso A B
Iso.fun (pathToIso x) = transport x
Iso.inv (pathToIso x) = transport⁻ x
Iso.rightInv (pathToIso x) = transportTransport⁻ x
Iso.leftInv (pathToIso x) = transport⁻Transport x

isInjectiveTransport : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B}
  → transport p ≡ transport q → p ≡ q
isInjectiveTransport {p = p} {q} α i =
  hcomp
    (λ j → λ
      { (i = i0) → retEq univalence p j
      ; (i = i1) → retEq univalence q j
      })
    (invEq univalence ((λ a → α i a) , t i))
  where
  t : PathP (λ i → isEquiv (λ a → α i a)) (pathToEquiv p .snd) (pathToEquiv q .snd)
  t = isProp→PathP (λ i → isPropIsEquiv (λ a → α i a)) _ _

transportUaInv : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) → transport (ua (invEquiv e)) ≡ transport (sym (ua e))
transportUaInv e = cong transport (uaInvEquiv e)
-- notice that transport (ua e) would reduce, thus an alternative definition using EquivJ can give
-- refl for the case of idEquiv:
-- transportUaInv e = EquivJ (λ _ e → transport (ua (invEquiv e)) ≡ transport (sym (ua e))) refl e

isSet-subst : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
                → (isSet-A : isSet A)
                → ∀ {a : A}
                → (p : a ≡ a) → (x : B a) → subst B p x ≡ x
isSet-subst {B = B} isSet-A p x = subst (λ p′ → subst B p′ x ≡ x) (isSet-A _ _ refl p) (substRefl {B = B} x)

-- substituting along a composite path is equivalent to substituting twice
substComposite : ∀ {ℓ ℓ'} {A : Type ℓ} → (B : A → Type ℓ')
                 → {x y z : A} (p : x ≡ y) (q : y ≡ z) (u : B x)
                 → subst B (p ∙ q) u ≡ subst B q (subst B p u)
substComposite B p q Bx i =
  transport (cong B (compPath-filler' p q (~ i))) (transport-fillerExt (cong B p) i Bx)

-- transporting along a composite path is equivalent to transporting twice
transportComposite : ∀ {ℓ} {A B C : Type ℓ} (p : A ≡ B) (q : B ≡ C) (x : A)
                 → transport (p ∙ q) x ≡ transport q (transport p x)
transportComposite = substComposite (λ D → D)

-- substitution commutes with morphisms in slices
substCommSlice : ∀ {ℓ ℓ′} {A : Type ℓ}
                   → (B C : A → Type ℓ′)
                   → (F : ∀ a → B a → C a)
                   → {x y : A} (p : x ≡ y) (u : B x)
                   → subst C p (F x u) ≡ F y (subst B p u)
substCommSlice B C F p Bx a =
  transport-fillerExt⁻ (cong C p) a (F _ (transport-fillerExt (cong B p) a Bx))

constSubstCommSlice : ∀ {ℓ ℓ'} {A : Type ℓ}
                   → (B : A → Type ℓ')
                   → (C : Type ℓ')
                   → (F : ∀ a → B a → C)
                   → {x y : A} (p : x ≡ y) (u : B x)
                   →  (F x u) ≡ F y (subst B p u)
constSubstCommSlice B C F p Bx = (sym (transportRefl (F _ Bx)) ∙ substCommSlice B (λ _ → C) F p Bx)

-- transporting over (λ i → B (p i) → C (p i)) divides the transport into
-- transports over (λ i → C (p i)) and (λ i → B (p (~ i)))
funTypeTransp : ∀ {ℓ ℓ'} {A : Type ℓ} (B C : A → Type ℓ') {x y : A} (p : x ≡ y) (f : B x → C x)
         → PathP (λ i → B (p i) → C (p i)) f (subst C p ∘ f ∘ subst B (sym p))
funTypeTransp B C {x = x} p f i b =
  transp (λ j → C (p (j ∧ i))) (~ i) (f (transp (λ j → B (p (i ∧ ~ j))) (~ i) b))

-- transports between loop spaces preserve path composition
overPathFunct : ∀ {ℓ} {A : Type ℓ} {x y : A} (p q : x ≡ x) (P : x ≡ y)
           → transport (λ i → P i ≡ P i) (p ∙ q)
            ≡ transport (λ i → P i ≡ P i) p ∙ transport (λ i → P i ≡ P i) q
overPathFunct p q =
  J (λ y P → transport (λ i → P i ≡ P i) (p ∙ q) ≡ transport (λ i → P i ≡ P i) p ∙ transport (λ i → P i ≡ P i) q)
    (transportRefl (p ∙ q) ∙ cong₂ _∙_ (sym (transportRefl p)) (sym (transportRefl q)))

-- substition over families of paths
-- theorem 2.11.3 in The Book
substInPaths : ∀ {ℓ} {A B : Type ℓ} {a a' : A}
                 → (f g : A → B) → (p : a ≡ a') (q : f a ≡ g a)
                 → subst (λ x → f x ≡ g x) p q ≡ sym (cong f p) ∙ q ∙ cong g p
substInPaths {a = a} f g p q =
  J (λ x p' → (subst (λ y → f y ≡ g y) p' q) ≡ (sym (cong f p') ∙ q ∙ cong g p'))
    p=refl p
    where
    p=refl : subst (λ y → f y ≡ g y) refl q
           ≡ refl ∙ q ∙ refl
    p=refl = subst (λ y → f y ≡ g y) refl q
           ≡⟨ substRefl {B = (λ y → f y ≡ g y)} q ⟩ q
           ≡⟨ (rUnit q) ∙ lUnit (q ∙ refl) ⟩ refl ∙ q ∙ refl ∎

-- special cases of substInPaths from lemma 2.11.2 in The Book
module _ {ℓ : Level} {A : Type ℓ} {a x1 x2 : A} (p : x1 ≡ x2) where
  substInPathsL : (q : a ≡ x1) → subst (λ x → a ≡ x) p q ≡ q ∙ p
  substInPathsL q = subst (λ x → a ≡ x) p q
    ≡⟨ substInPaths (λ _ → a) (λ x → x) p q ⟩
      sym (cong (λ _ → a) p) ∙ q ∙ cong (λ x → x) p
    ≡⟨ assoc (λ _ → a) q p ⟩
      (refl ∙ q) ∙ p
    ≡⟨ cong (_∙ p) (sym (lUnit q)) ⟩ q ∙ p ∎

  substInPathsR : (q : x1 ≡ a) → subst (λ x → x ≡ a) p q ≡ sym p ∙ q
  substInPathsR q = subst (λ x → x ≡ a) p q
    ≡⟨ substInPaths (λ x → x) (λ _ → a) p q ⟩
      sym (cong (λ x → x) p) ∙ q ∙ cong (λ _ → a) p
    ≡⟨ assoc (sym p) q refl ⟩
      (sym p ∙ q) ∙ refl
    ≡⟨ sym (rUnit (sym p ∙ q))⟩ sym p ∙ q ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Constructions.Terminal where

open import Data.Product using (proj₁ ; proj₂)
open import Level

open import Cats.Category.Base

import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Unique as Unique

module Build {lo la l≈} (Cat : Category lo la l≈) where

  open Category Cat
  open Iso.Build Cat
  open Unique.Build Cat

  IsTerminal : Obj → Set (lo ⊔ la ⊔ l≈)
  IsTerminal ⊤ = ∀ X → ∃! X ⊤

  record HasTerminal : Set (lo ⊔ la ⊔ l≈) where
    field
      ⊤ : Obj
      isTerminal : IsTerminal ⊤

    ! : ∀ X → X ⇒ ⊤
    ! X = ∃!′.arr (isTerminal X)

    !-unique : ∀ {X} (f : X ⇒ ⊤) → ! X ≈ f
    !-unique {X} f = ∃!′.unique (isTerminal X) _

    ⇒⊤-unique : ∀ {X} (f g : X ⇒ ⊤) → f ≈ g
    ⇒⊤-unique f g = ≈.trans (≈.sym (!-unique f)) (!-unique g)

    ⊤-unique : ∀ {X} → IsTerminal X → X ≅ ⊤
    ⊤-unique {X} term = record
      { forth = ! X
      ; back = term ⊤ .∃!′.arr
      ; back-forth = ≈.trans (≈.sym (term X .∃!′.unique _)) (term X .∃!′.unique _)
      ; forth-back = ⇒⊤-unique _ _
      }

  terminal-unique : ∀ {X Y} → IsTerminal X → IsTerminal Y → X ≅ Y
  terminal-unique X-term Y-term
    = HasTerminal.⊤-unique (record { isTerminal = Y-term }) X-term

open Build public using (HasTerminal)

private
  open module Build′ {lo la l≈} {C : Category lo la l≈}
    = Build C public using (IsTerminal ; terminal-unique)

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
-- 2012-10-20 Andreas
module Issue721c where

data Bool : Set where
  false true : Bool

record Foo (b : Bool) : Set where
  field
    _*_ : Bool → Bool → Bool

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

record ∃ {A : Set} (B : A → Set) : Set where
  constructor pack
  field fst : A
        snd : B fst

dontExpandTooMuch : (F : Foo false) → ∃ λ t → t ≡ t
dontExpandTooMuch F = pack t t
  where open Foo F
        d = λ x → x * x
        t = d (d (d (d true)))
-- t should not be expanded in the error message

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --no-termination-check #-}

module Lambda where

module Prelude where

  data Bool : Set where
    true  : Bool
    false : Bool

  if_then_else_ : {A : Set} -> Bool -> A -> A -> A
  if true  then x else y = x
  if false then x else y = y

  _∧_ : Bool -> Bool -> Bool
  true  ∧ y = y
  false ∧ y = false

  _∨_ : Bool -> Bool -> Bool
  true  ∨ y = true
  false ∨ y = y

  ¬_ : Bool -> Bool
  ¬ true  = false
  ¬ false = true

  data List (A : Set) : Set where
    nil    : List A
    _::_ : A -> List A -> List A

  _++_ : {A : Set} -> List A -> List A -> List A
  nil      ++ ys = ys
  (x :: xs) ++ ys = x :: xs ++ ys

  filter : {A : Set} -> (A -> Bool) -> List A -> List A
  filter p  nil      = nil
  filter p (x :: xs) = if p x then x :: filter p xs else filter p xs

  postulate
    String : Set
    Char   : Set

  {-# BUILTIN BOOL    Bool   #-}
  {-# BUILTIN FALSE   false  #-}
  {-# BUILTIN TRUE    true   #-}
  {-# BUILTIN STRING  String #-}
  {-# BUILTIN CHAR    Char   #-}
  {-# BUILTIN LIST    List   #-}
  {-# BUILTIN NIL     nil    #-}
  {-# BUILTIN CONS    _::_    #-}

  primitive
    primStringEquality : String -> String -> Bool

  _==_ = primStringEquality

  infix 10 if_then_else_
  infixr 50 _::_ _++_
  infixl 5 _∨_
  infixl 7 _∧_
  infix 50 ¬_
  infix 15 _==_

open Prelude

Name : Set
Name = String

data Exp : Set where
  var  : Name -> Exp
  ƛ_⟶_ : Name -> Exp -> Exp
  _$_  : Exp -> Exp -> Exp

infixl 50 _$_
infix  20 ƛ_⟶_

infix 80 _[_/_]
infix 15 _∈_

_∈_ : Name -> List Name -> Bool
x ∈ y :: ys = x == y ∨ x ∈ ys
x ∈ nil    = false

-- Free variables
FV : Exp -> List Name
FV (var x)   = x :: nil
FV (s $ t)   = FV s ++ FV t
FV (ƛ x ⟶ t) = filter (\y -> ¬ (x == y)) (FV t)

-- Fresh names
fresh : Name -> Exp -> Name
fresh x e = fresh' (FV e)
  where
    fresh' : List Name -> Name
    fresh' xs = "z" -- TODO

-- Substitution
_[_/_] : Exp -> Exp -> Name -> Exp
var x     [ r / z ] = if x == z then r else var x
(s $ t)   [ r / z ] = s [ r / z ] $ t [ r / z ]
(ƛ x ⟶ t) [ r / z ] =
       if x == z   then ƛ x ⟶ t
  else if x ∈ FV r then ( let y : Name
                              y = fresh x r
                          in  ƛ y ⟶ t [ var y / x ] [ r / z ]
                        )
  else                  ƛ x ⟶ t [ r / z ]


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

module Categories.Functor.Construction.LiftSetoids where

open import Level
open import Relation.Binary
open import Function.Equality
open import Function using (_$_) renaming (id to idf)

open import Categories.Category
open import Categories.Category.Instance.Setoids
open import Categories.Functor

private
  variable
    c ℓ : Level

-- Use pattern-matching (instead of explicit calls to lower) to minimize the
-- number of needed parens, and also make it syntactically apparent that
-- this is indeed just a Lift.
LiftedSetoid : ∀ c′ ℓ′ → Setoid c ℓ → Setoid (c ⊔ c′) (ℓ ⊔ ℓ′)
LiftedSetoid c′ ℓ′ S = record
  { Carrier       = Lift c′ Carrier
  ; _≈_           = λ where (lift x) (lift y) → Lift ℓ′ $ x ≈ y
  ; isEquivalence = record
    { refl  = lift refl
    ; sym   = λ where (lift eq)            → lift $ sym eq
    ; trans = λ where (lift eq) (lift eq′) → lift $ trans eq eq′
    }
  }
  where open Setoid S

LiftSetoids : ∀ c′ ℓ′ → Functor (Setoids c ℓ) (Setoids (c ⊔ c′) (ℓ ⊔ ℓ′))
LiftSetoids c′ ℓ′ = record
  { F₀           = LiftedSetoid c′ ℓ′
  ; F₁           = λ f → record
    { _⟨$⟩_  = λ where (lift x)  → lift $ f ⟨$⟩ x
    ; cong  = λ where (lift eq) → lift $ cong f eq
    }
  ; identity     = idf
  ; homomorphism = λ where {f = f} {g = g} (lift eq) → lift $ cong g $ cong f eq
  ; F-resp-≈     = λ where fx≈gy (lift x≈y)          → lift $ fx≈gy x≈y
  }

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:
{-# OPTIONS --cubical #-}

module Type.Cubical.SubtypeSet where

open import Function.Axioms
open import Functional
open import Logic.Predicate as PTLogic using () renaming ([∃]-intro to intro)
import      Lvl
open import Structure.Function.Domain using (intro ; Inverseₗ ; Inverseᵣ)
open import Structure.Relator.Properties
open import Structure.Type.Identity
open import Type.Cubical.Equiv
import      Type.Cubical.Logic as Logic
open import Type.Cubical.Path.Equality
open import Type.Cubical.Univalence
open import Type.Cubical
open import Type.Properties.MereProposition
open import Type.Properties.Singleton.Proofs
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ : Lvl.Level
private variable T A B P Q : Type{ℓ}

{-
module _ {P Q : T → Type} ⦃ prop-P : ∀{x} → MereProposition{ℓ}(P(x)) ⦄ ⦃ prop-Q : ∀{x} → MereProposition{ℓ}(Q(x)) ⦄ where
  prop-set-extensionalityₗ : (P ≡ Q) ← (∀{x} → P(x) ↔ Q(x))
  prop-set-extensionalityₗ pq = functionExtensionalityOn P Q (propositional-extensionalityₗ pq)
-}

--data Prop{ℓ} : Type{Lvl.𝐒(ℓ)} where
--  intro : (T : Type{ℓ}) → ⦃ MereProposition(T) ⦄ → Prop
Prop = \{ℓ} → PTLogic.∃{Obj = Type{ℓ}} (T ↦ MereProposition(T))

⊤ : Prop
⊤ = intro(Logic.⊤) ⦃ prop-top ⦄

⊥ : Prop
⊥ = intro(Logic.⊥) ⦃ prop-bottom ⦄

¬_ : Prop{ℓ} → Prop
¬(intro A) = intro(Logic.¬ A) ⦃ prop-negation ⦄

_⟶_ : Prop{ℓ₁} → Prop{ℓ₂} → Prop
(intro A) ⟶ (intro B) = intro(A → B) ⦃ prop-implication ⦄

_∨_ : Prop{ℓ₁} → Prop{ℓ₂} → Prop
(intro A) ∨ (intro B) = intro(A Logic.∨ B)

_∧_ : Prop{ℓ₁} → Prop{ℓ₂} → Prop
(intro A) ∧ (intro B) = intro(A Logic.∧ B) ⦃ prop-conjunction ⦄

∃ : (T → Prop{ℓ}) → Prop
∃ P = intro(Logic.∃(PTLogic.[∃]-witness ∘ P))

-- ∀ₚ : (T → Prop{ℓ}) → Prop
-- ∀ₚ P = intro(PTLogic.∀ₗ(PTLogic.[∃]-witness ∘ P)) ⦃ {!prop-universal!} ⦄

record SubtypeSet {ℓₑ ℓ} (T : Type{ℓ}) : Type{ℓ Lvl.⊔ Lvl.𝐒(ℓₑ)} where
  constructor filter
  field _∋_ : T → Prop{ℓₑ}
open SubtypeSet using (_∋_) public

{- TODO: When Structure is generalized to arbitrary logic symbols
import      Structure.Sets.Names
open        Structure.Sets.Names.From-[∋] (_∋_) public
-}

_∈_ : T → SubtypeSet{ℓ}(T) → Prop
_∈_ = swap(_∋_)

_∉_ : T → SubtypeSet{ℓ}(T) → Prop
_∉_ = (¬_) ∘₂ (_∈_)

_∌_ : SubtypeSet{ℓ}(T) → T → Prop
_∌_ = (¬_) ∘₂ (_∋_)

∅ : SubtypeSet(T)
∅ ∋ _ = ⊥

𝐔 : SubtypeSet(T)
𝐔 ∋ _ = ⊤

∁ : SubtypeSet{ℓ}(T) → SubtypeSet(T)
(∁ A) ∋ x = A ∌ x

_∪_ : SubtypeSet{ℓ₁}(T) → SubtypeSet{ℓ₂}(T) → SubtypeSet(T)
(A ∪ B) ∋ x = (A ∋ x) ∨ (B ∋ x)

_∩_ : SubtypeSet{ℓ₁}(T) → SubtypeSet{ℓ₂}(T) → SubtypeSet(T)
(A ∩ B) ∋ x = (A ∋ x) ∧ (B ∋ x)

_∖_ : SubtypeSet{ℓ₁}(T) → SubtypeSet{ℓ₂}(T) → SubtypeSet(T)
(A ∖ B) ∋ x = (A ∋ x) ∧ (B ∌ x)

unmap : (A → B) → SubtypeSet{ℓ}(B) → SubtypeSet(A)
unmap f(A) ∋ x = A ∋ f(x)

-- map : (A → B) → SubtypeSet{ℓ}(A) → SubtypeSet(B)
-- map f(A) ∋ y = ∃(x ↦ (A ∋ x) ∧ (f(x) ≡ y))

-- TODO: Maybe SubtypeSet should require that the witness is a HSet?
-- ⊶ : (A → B) → SubtypeSet(B)
-- (⊶ f) ∋ y = ∃(x ↦ PTLogic.[∃]-intro (f(x) ≡ y) ⦃ {!!} ⦄)


text:
module _ where

open import Haskell.Prelude
open import Agda.Builtin.Equality

-- ** Foreign HS code

-- language extensions
{-# FOREIGN AGDA2HS
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}
#-}

-- imports
{-# FOREIGN AGDA2HS
import Data.Monoid
#-}

-- ** Datatypes & functions

data Exp (v : Set) : Set where
  Plus : Exp v → Exp v → Exp v
  Lit : Nat → Exp v
  Var : v → Exp v
{-# COMPILE AGDA2HS Exp deriving (Show,Eq) #-}

eval : (a → Nat) → Exp a → Nat
eval env (Plus a b) = eval env a + eval env b
eval env (Lit n) = n
eval env (Var x) = env x
{-# COMPILE AGDA2HS eval #-}

-- ** Natural numbers

listSum : List Int → Int
listSum []       = 0
listSum (x ∷ xs) = x + sum xs
{-# COMPILE AGDA2HS listSum #-}

monoSum : List Integer → Integer
monoSum xs = sum xs
{-# COMPILE AGDA2HS monoSum #-}

polySum : ⦃ iNum : Num a ⦄ → List a → a
polySum xs = sum xs
{-# COMPILE AGDA2HS polySum #-}

{-# FOREIGN AGDA2HS
-- comment
-- another comment
bla :: Int -> Int
bla n = n * 4

{- multi
   line
   comment
-}
#-}

-- ** Extra builtins

ex_float : Double
ex_float = 0.0
{-# COMPILE AGDA2HS ex_float #-}

postulate
  toInteger : Word → Integer

ex_word : Word
ex_word = fromInteger 0
{-# COMPILE AGDA2HS ex_word #-}

ex_char : Char
ex_char = 'a'
{-# COMPILE AGDA2HS ex_char #-}

char_d : Char
char_d = toEnum 100
{-# COMPILE AGDA2HS char_d #-}

-- ** Polymorphic functions

_+++_ : List a → List a → List a
[]       +++ ys = ys
(x ∷ xs) +++ ys = x ∷ (xs +++ ys)
{-# COMPILE AGDA2HS _+++_ #-}

listMap : (a → b) → List a → List b
listMap f [] = []
listMap f (x ∷ xs) = f x ∷ listMap f xs
{-# COMPILE AGDA2HS listMap #-}

mapTest : List Nat → List Nat
mapTest = map (id ∘ _+_ 5)
{-# COMPILE AGDA2HS mapTest #-}

-- ** Lambdas

plus3 : List Nat → List Nat
plus3 = map (λ n → n + 3)
{-# COMPILE AGDA2HS plus3 #-}

doubleLambda : Nat → Nat → Nat
doubleLambda = λ a b → a + 2 * b
{-# COMPILE AGDA2HS doubleLambda #-}

cnst : a → b → a
cnst = λ x _ → x
{-# COMPILE AGDA2HS cnst #-}

-- ** Constraints

second : (b → c) → a × b → a × c
second f (x , y) = x , f y
{-# COMPILE AGDA2HS second #-}

doubleTake : (n m : Int) → ⦃ IsNonNegativeInt n ⦄ → ⦃ IsNonNegativeInt m ⦄ → List a → List a × List a
doubleTake n m = second (take m) ∘ splitAt n
{-# COMPILE AGDA2HS doubleTake #-}

initLast : (xs : List a) → ⦃ NonEmpty xs ⦄ → List a × a
initLast xs = init xs , last xs
{-# COMPILE AGDA2HS initLast #-}

-- ** Proofs

assoc : (a b c : Nat) → a + (b + c) ≡ (a + b) + c
assoc zero    b c = refl
assoc (suc a) b c rewrite assoc a b c = refl

thm : (xs ys : List Nat) → sum (xs ++ ys) ≡ sum xs + sum ys
thm []       ys = refl
thm (x ∷ xs) ys rewrite thm xs ys | assoc x (sum xs) (sum ys) = refl

-- (custom) Monoid class

record MonoidX (a : Set) : Set where
  field memptyX  : a
        mappendX : a → a → a

open MonoidX {{...}} public

{-# COMPILE AGDA2HS MonoidX #-}

instance
  MonoidNat : MonoidX Nat
  memptyX  {{MonoidNat}}     = 0
  mappendX {{MonoidNat}} i j = i + j

{-# COMPILE AGDA2HS MonoidNat #-}

instance
  MonoidFunNat : {a : Set} → MonoidX (a → Nat)
  memptyX  {{MonoidFunNat}}     _ = memptyX
  mappendX {{MonoidFunNat}} f g x = mappendX (f x) (g x)

{-# COMPILE AGDA2HS MonoidFunNat #-}

instance
  MonoidFun : {a b : Set} → {{MonoidX b}} → MonoidX (a → b)
  memptyX  {{MonoidFun}}     _ = memptyX
  mappendX {{MonoidFun}} f g x = mappendX (f x) (g x)
{-# COMPILE AGDA2HS MonoidFun #-}

sumMonX : ∀{a} → {{MonoidX a}} → List a → a
sumMonX []       = memptyX
sumMonX (x ∷ xs) = mappendX x (sumMonX xs)
{-# COMPILE AGDA2HS sumMonX #-}

sumMon : ∀{a} → {{Monoid a}} → List a → a
sumMon []       = mempty
sumMon (x ∷ xs) = x <> sumMon xs
{-# COMPILE AGDA2HS sumMon #-}

-- Using the Monoid class from the Prelude

data NatSum : Set where
  MkSum : Nat → NatSum

{-# COMPILE AGDA2HS NatSum #-}

instance
  SemigroupNatSum : Semigroup NatSum
  SemigroupNatSum ._<>_ (MkSum a) (MkSum b) = MkSum (a + b)

  MonoidNatSum : Monoid NatSum
  MonoidNatSum .mempty = MkSum 0

double : ⦃ Monoid a ⦄ → a → a
double x = x <> x

doubleSum : NatSum → NatSum
doubleSum = double

{-# COMPILE AGDA2HS SemigroupNatSum #-}
{-# COMPILE AGDA2HS MonoidNatSum    #-}
{-# COMPILE AGDA2HS double          #-}
{-# COMPILE AGDA2HS doubleSum       #-}

-- Instance argument proof obligation that should not turn into a class constraint
hd : (xs : List a) → ⦃ NonEmpty xs ⦄ → a
hd []      = error "hd: empty list"
hd (x ∷ _) = x
{-# COMPILE AGDA2HS hd #-}

five : Int
five = hd (5 ∷ 3 ∷ [])
{-# COMPILE AGDA2HS five #-}

-- ** Booleans

ex_bool : Bool
ex_bool = true
{-# COMPILE AGDA2HS ex_bool #-}

ex_if : Nat
ex_if = if true then 1 else 0
{-# COMPILE AGDA2HS ex_if #-}

if_over : Nat
if_over = (if true then (λ x → x) else (λ x → x + 1)) 0
{-# COMPILE AGDA2HS if_over #-}

if_partial₁ : List Nat → List Nat
if_partial₁ = map (if true then 1 else_)
{-# COMPILE AGDA2HS if_partial₁ #-}

if_partial₂ : List Nat → List (Nat → Nat)
if_partial₂ = map (if true then_else_)
{-# COMPILE AGDA2HS if_partial₂ #-}

if_partial₃ : List Bool → List (Nat → Nat → Nat)
if_partial₃ = map if_then_else_
{-# COMPILE AGDA2HS if_partial₃ #-}

if_partial₄ : List Bool → List (Nat → Nat)
if_partial₄ = map (if_then 1 else_)
{-# COMPILE AGDA2HS if_partial₄ #-}

if_partial₅ : Bool → Nat → List Nat → List Nat
if_partial₅ b f = map (if b then f else_)
{-# COMPILE AGDA2HS if_partial₅ #-}