text:
open import Function using (_$_)

open import Relation.Binary using (Setoid)

open import Data.Product using (_,_)

open import Algebra.Bundles using (RawGroup; RawRing)
open import Algebra.Structures using (IsGroup; IsAbelianGroup; IsRing; IsCommutativeRing)
open import AKS.Algebra.Structures using (IsNonZeroCommutativeRing; IsIntegralDomain)
open import AKS.Algebra.Morphism.Structures using (IsGroupHomomorphism; IsGroupMonomorphism; IsRingHomomorphism; IsRingMonomorphism)

module AKS.Algebra.Morphism.Consequences where

module GroupConsequences {c₁ c₂ ℓ₁ ℓ₂} {G₁ : RawGroup c₁ ℓ₁} {G₂ : RawGroup c₂ ℓ₂} {⟦_⟧} (isGroupMonomorphism : IsGroupMonomorphism G₁ G₂ ⟦_⟧) where
  open RawGroup G₁ using () renaming (Carrier to C₁; _∙_ to _+₁_; _⁻¹ to -₁_; ε to ε₁; _≈_ to _≈₁_; rawMonoid to +₁-rawMonoid)
  open RawGroup G₂ using () renaming (Carrier to C₂; _∙_ to _+₂_; _⁻¹ to -₂_; ε to ε₂; _≈_ to _≈₂_; rawMonoid to +₂-rawMonoid)
  open IsGroupMonomorphism isGroupMonomorphism using (injective; +-homo; -‿homo; ε-homo; +-isMonoidMonomorphism; ⟦⟧-cong)
  open import Algebra.Morphism.MonoidMonomorphism +-isMonoidMonomorphism using () renaming (isMonoid to +₂-isMonoid→+₁-isMonoid; comm to +₂-comm→+₁-comm)

  module _ (G₂-isGroup : IsGroup _≈₂_ _+₂_ ε₂ -₂_) where
    open IsGroup G₂-isGroup using (setoid) renaming (isMonoid to +₂-isMonoid; ⁻¹-cong to -‿cong₂; inverseˡ to -‿inverseˡ₂; inverseʳ to -‿inverseʳ₂; ∙-congˡ to +-congˡ; ∙-congʳ to +-congʳ)
    open Setoid setoid using (sym)
    open import Relation.Binary.Reasoning.Setoid setoid
    open import Algebra.Definitions _≈₁_ using (LeftInverse; RightInverse; Inverse; Congruent₁)

    -‿inverseˡ₁ : LeftInverse ε₁ -₁_ _+₁_
    -‿inverseˡ₁ x = injective $ begin
      ⟦ -₁ x +₁ x ⟧     ≈⟨ +-homo (-₁ x) x ⟩
      ⟦ -₁ x ⟧ +₂ ⟦ x ⟧ ≈⟨ +-congʳ (-‿homo x) ⟩
      -₂ ⟦ x ⟧ +₂ ⟦ x ⟧ ≈⟨ -‿inverseˡ₂ ⟦ x ⟧ ⟩
      ε₂                ≈⟨ sym ε-homo ⟩
      ⟦ ε₁ ⟧            ∎

    -‿inverseʳ₁ : RightInverse ε₁ -₁_ _+₁_
    -‿inverseʳ₁ x = injective $ begin
      ⟦ x +₁ -₁ x ⟧     ≈⟨ +-homo x (-₁ x) ⟩
      ⟦ x ⟧ +₂ ⟦ -₁ x ⟧ ≈⟨ +-congˡ (-‿homo x) ⟩
      ⟦ x ⟧ +₂ -₂ ⟦ x ⟧ ≈⟨ -‿inverseʳ₂ ⟦ x ⟧ ⟩
      ε₂                ≈⟨ sym ε-homo ⟩
      ⟦ ε₁ ⟧            ∎

    -‿inverse₁ : Inverse ε₁ -₁_ _+₁_
    -‿inverse₁ = -‿inverseˡ₁ , -‿inverseʳ₁

    -‿cong₁ : Congruent₁ -₁_
    -‿cong₁ {x} {y} x≈y = injective $ begin
      ⟦ -₁ x ⟧ ≈⟨ -‿homo x ⟩
      -₂ ⟦ x ⟧ ≈⟨ -‿cong₂ (⟦⟧-cong x≈y) ⟩
      -₂ ⟦ y ⟧ ≈⟨ sym (-‿homo y) ⟩
      ⟦ -₁ y ⟧ ∎

    G₂-isGroup→G₁-isGroup : IsGroup _≈₁_ _+₁_ ε₁ -₁_
    G₂-isGroup→G₁-isGroup = record
      { isMonoid = +₂-isMonoid→+₁-isMonoid +₂-isMonoid
      ; inverse = -‿inverse₁
      ; ⁻¹-cong = -‿cong₁
      }

  module _ (G₂-isAbelianGroup : IsAbelianGroup _≈₂_ _+₂_ ε₂ -₂_) where
    open IsAbelianGroup G₂-isAbelianGroup using () renaming (isGroup to G₂-isGroup; isMagma to +₂-isMagma; comm to +₂-comm)

    G₂-isAbelianGroup→G₁-isAbelianGroup : IsAbelianGroup _≈₁_ _+₁_ ε₁ -₁_
    G₂-isAbelianGroup→G₁-isAbelianGroup = record
      { isGroup = G₂-isGroup→G₁-isGroup G₂-isGroup
      ; comm = +₂-comm→+₁-comm +₂-isMagma +₂-comm
      }

module RingConsequences {c₁ c₂ ℓ₁ ℓ₂} {R₁ : RawRing c₁ ℓ₁} {R₂ : RawRing c₂ ℓ₂} {⟦_⟧} (isRingMonomorphism : IsRingMonomorphism R₁ R₂ ⟦_⟧) where
  open RawRing R₁ using () renaming (Carrier to C₁; _+_ to _+₁_; _*_ to _*₁_; -_ to -₁_; 0# to 0#₁; 1# to 1#₁; _≈_ to _≈₁_)
  open RawRing R₂ using () renaming (Carrier to C₂; _+_ to _+₂_; _*_ to _*₂_; -_ to -₂_; 0# to 0#₂; 1# to 1#₂; _≈_ to _≈₂_)
  open IsRingMonomorphism isRingMonomorphism using (injective; +-homo; *-homo; 0#-homo; 1#-homo; ⟦⟧-cong; *-isMonoidMonomorphism; +-isGroupMonomorphism)
  open import Algebra.Morphism.MonoidMonomorphism *-isMonoidMonomorphism using () renaming (isMonoid to *₂-isMonoid→*₁-isMonoid; comm to *₂-comm→*₁-comm)

  module _ (R₂-isRing : IsRing _≈₂_ _+₂_ _*₂_ -₂_ 0#₂ 1#₂) where
    open IsRing R₂-isRing using (setoid; +-cong; *-congˡ; *-congʳ) renaming (distribʳ to distribʳ₁; distribˡ to distribˡ₁; *-isMonoid to *₂-isMonoid; +-isAbelianGroup to +₂-isAbelianGroup)
    open Setoid setoid using (sym)
    open import Relation.Binary.Reasoning.Setoid setoid
    open import Algebra.Definitions _≈₁_ using (_DistributesOverʳ_; _DistributesOverˡ_; _DistributesOver_)

    distribʳ : _*₁_ DistributesOverʳ _+₁_
    distribʳ r x y = injective $ begin
      ⟦ (x +₁ y) *₁ r ⟧                ≈⟨ *-homo (x +₁ y) r ⟩
      ⟦ x +₁ y ⟧ *₂ ⟦ r ⟧              ≈⟨ *-congʳ (+-homo x y) ⟩
      (⟦ x ⟧ +₂ ⟦ y ⟧) *₂ ⟦ r ⟧        ≈⟨ distribʳ₁ ⟦ r ⟧ ⟦ x ⟧ ⟦ y ⟧ ⟩
      ⟦ x ⟧ *₂ ⟦ r ⟧ +₂ ⟦ y ⟧ *₂ ⟦ r ⟧ ≈⟨ +-cong (sym (*-homo x r )) (sym (*-homo y r)) ⟩
      ⟦ x *₁ r ⟧ +₂ ⟦ y *₁ r ⟧         ≈⟨ sym (+-homo (x *₁ r) (y *₁ r)) ⟩
      ⟦ x *₁ r +₁ y *₁ r ⟧ ∎

    distribˡ : _*₁_ DistributesOverˡ _+₁_
    distribˡ r x y = injective $ begin
      ⟦ r *₁ (x +₁ y) ⟧                ≈⟨ *-homo r (x +₁ y) ⟩
      ⟦ r ⟧ *₂ ⟦ x +₁ y ⟧              ≈⟨ *-congˡ (+-homo x y) ⟩
      ⟦ r ⟧ *₂ (⟦ x ⟧ +₂ ⟦ y ⟧)        ≈⟨ distribˡ₁ ⟦ r ⟧ ⟦ x ⟧ ⟦ y ⟧ ⟩
      ⟦ r ⟧ *₂ ⟦ x ⟧ +₂ ⟦ r ⟧ *₂ ⟦ y ⟧ ≈⟨ +-cong (sym (*-homo r x)) (sym (*-homo r y)) ⟩
      ⟦ r *₁ x ⟧ +₂ ⟦ r *₁ y ⟧         ≈⟨ sym (+-homo (r *₁ x) (r *₁ y)) ⟩
      ⟦ r *₁ x +₁ r *₁ y ⟧ ∎

    distrib : _*₁_ DistributesOver _+₁_
    distrib = distribˡ , distribʳ

    open GroupConsequences +-isGroupMonomorphism

    R₂-isRing→R₁-isRing : IsRing _≈₁_ _+₁_ _*₁_ -₁_ 0#₁ 1#₁
    R₂-isRing→R₁-isRing = record
      { +-isAbelianGroup = G₂-isAbelianGroup→G₁-isAbelianGroup +₂-isAbelianGroup
      ; *-isMonoid = *₂-isMonoid→*₁-isMonoid *₂-isMonoid
      ; distrib = distrib
      }

  module _ (R₂-isCommutativeRing : IsCommutativeRing _≈₂_ _+₂_ _*₂_ -₂_ 0#₂ 1#₂) where
    open IsCommutativeRing R₂-isCommutativeRing using () renaming (isRing to R₂-isRing; *-comm to *₂-comm; *-isMagma to *₂-isMagma)

    R₂-isCommutativeRing→R₁-isCommutativeRing : IsCommutativeRing _≈₁_ _+₁_ _*₁_ -₁_ 0#₁ 1#₁
    R₂-isCommutativeRing→R₁-isCommutativeRing = record
      { isRing = R₂-isRing→R₁-isRing R₂-isRing
      ; *-comm = *₂-comm→*₁-comm *₂-isMagma *₂-comm
      }

  module _ (R₂-isNonZeroCommutativeRing : IsNonZeroCommutativeRing C₂ _≈₂_ _+₂_ _*₂_ -₂_ 0#₂ 1#₂) where
    open IsNonZeroCommutativeRing R₂-isNonZeroCommutativeRing using (setoid) renaming (isCommutativeRing to R₂-isCommutativeRing; 0#≉1# to 0#₂≉1#₂)
    open Setoid setoid using (sym)
    open import Relation.Binary.Reasoning.Setoid setoid
    open import AKS.Algebra.Structures C₁ _≈₁_ using () renaming (_≉_ to _≉₁_)

    0#₁≉1#₁ : 0#₁ ≉₁ 1#₁
    0#₁≉1#₁ 0#₁≈1#₁ = 0#₂≉1#₂ $ begin
      0#₂     ≈⟨ sym 0#-homo ⟩
      ⟦ 0#₁ ⟧ ≈⟨ ⟦⟧-cong 0#₁≈1#₁ ⟩
      ⟦ 1#₁ ⟧ ≈⟨ 1#-homo ⟩
      1#₂ ∎

    R₂-isNonZeroCommutativeRing→R₁-isNonZeroCommutativeRing : IsNonZeroCommutativeRing C₁ _≈₁_ _+₁_ _*₁_ -₁_ 0#₁ 1#₁
    R₂-isNonZeroCommutativeRing→R₁-isNonZeroCommutativeRing = record
      { isCommutativeRing = R₂-isCommutativeRing→R₁-isCommutativeRing R₂-isCommutativeRing
      ; 0#≉1# = 0#₁≉1#₁
      }

  module _ (R₂-isIntegralDomain : IsIntegralDomain C₂ _≈₂_ _+₂_ _*₂_ -₂_ 0#₂ 1#₂) where
    open IsIntegralDomain R₂-isIntegralDomain using (setoid) renaming (isNonZeroCommutativeRing to R₂-isNonZeroCommutativeRing; *-cancelˡ to *₂-cancelˡ)
    open Setoid setoid using (sym)
    open import Relation.Binary.Reasoning.Setoid setoid
    open import AKS.Algebra.Structures C₁ _≈₁_ using () renaming (_≉_ to _≉₁_)
    open import AKS.Algebra.Structures C₂ _≈₂_ using () renaming (_≉_ to _≉₂_)

    *-cancelˡ : ∀ x {y z} → x ≉₁ 0#₁ → x *₁ y ≈₁ x *₁ z → y ≈₁ z
    *-cancelˡ x {y} {z} x≉0 x*y≈x*z = injective $ *₂-cancelˡ ⟦ x ⟧ ⟦x⟧≉0 $ begin
      ⟦ x ⟧ *₂ ⟦ y ⟧ ≈⟨ sym (*-homo x y) ⟩
      ⟦ x *₁ y ⟧     ≈⟨ ⟦⟧-cong x*y≈x*z ⟩
      ⟦ x *₁ z ⟧     ≈⟨ *-homo x z ⟩
      ⟦ x ⟧ *₂ ⟦ z ⟧ ∎
      where
      ⟦x⟧≉0 : ⟦ x ⟧ ≉₂ 0#₂
      ⟦x⟧≉0 ⟦x⟧≈0 = x≉0 $ injective $ begin
        ⟦ x ⟧   ≈⟨ ⟦x⟧≈0 ⟩
        0#₂     ≈⟨ sym 0#-homo ⟩
        ⟦ 0#₁ ⟧ ∎

    R₂-isIntegralDomain→R₁-isIntegralDomain : IsIntegralDomain C₁ _≈₁_ _+₁_ _*₁_ -₁_ 0#₁ 1#₁
    R₂-isIntegralDomain→R₁-isIntegralDomain = record
      { isNonZeroCommutativeRing = R₂-isNonZeroCommutativeRing→R₁-isNonZeroCommutativeRing R₂-isNonZeroCommutativeRing
      ; *-cancelˡ = *-cancelˡ
      }

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


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

open import lib.Basics
open import lib.types.Cospan
open import lib.types.Pullback
open import lib.types.Group
open import lib.groups.Homomorphisms

module lib.groups.PullbackGroup where

--   φ   ψ
-- H → G ← K

record Group-Cospan {i j k : ULevel} : Type (lsucc (lmax (lmax i j) k)) where
  constructor group-cospan
  field
    H : Group i
    K : Group j
    G : Group k
    φ : H →ᴳ G
    ψ : K →ᴳ G

group-cospan-out : ∀ {i j k} → Group-Cospan {i} {j} {k} → Cospan {i} {j} {k}
group-cospan-out (group-cospan H K G φ ψ) =
  cospan (Group.El H) (Group.El K) (Group.El G) (GroupHom.f φ) (GroupHom.f ψ)

module _ {i j k} (D : Group-Cospan {i} {j} {k}) where

  private
    open Group-Cospan D
    module H = Group H
    module K = Group K
    module G = Group G
    module φ = GroupHom φ
    module ψ = GroupHom ψ

    d : Cospan
    d = cospan H.El K.El G.El φ.f ψ.f

  Pullback-group-struct : GroupStructure (Pullback d)
  Pullback-group-struct = record {
    ident = pullback H.ident K.ident (φ.pres-ident ∙ ! (ψ.pres-ident));
    inv = λ {(pullback h k p) →
      pullback (H.inv h) (K.inv k)
        (φ.pres-inv h ∙ ap G.inv p ∙ ! (ψ.pres-inv k))};
    comp = λ {(pullback h₁ k₁ p₁) (pullback h₂ k₂ p₂) →
      pullback (H.comp h₁ h₂) (K.comp k₁ k₂)
        (φ.pres-comp h₁ h₂ ∙ ap2 G.comp p₁ p₂ ∙ ! (ψ.pres-comp k₁ k₂))};
    unitl = λ {(pullback h k p) →
      pullback= d (H.unitl h) (K.unitl k)
        (prop-has-all-paths (G.El-level _ _) _ _)};
    unitr = λ {(pullback h k p) →
      pullback= d (H.unitr h) (K.unitr k)
        (prop-has-all-paths (G.El-level _ _) _ _)};
    assoc = λ {(pullback h₁ k₁ p₁) (pullback h₂ k₂ p₂) (pullback h₃ k₃ p₃) →
      pullback= d (H.assoc h₁ h₂ h₃) (K.assoc k₁ k₂ k₃)
        (prop-has-all-paths (G.El-level _ _) _ _)};
    invl = λ {(pullback h k p) →
      pullback= d (H.invl h) (K.invl k)
        (prop-has-all-paths (G.El-level _ _) _ _)};
    invr = λ {(pullback h k p) →
      pullback= d (H.invr h) (K.invr k)
        (prop-has-all-paths (G.El-level _ _) _ _)}}

  Pullback-group : Group (lmax i (lmax j k))
  Pullback-group = record {
    El = Pullback d;
    El-level = pullback-level 0 H.El-level K.El-level G.El-level;
    group-struct = Pullback-group-struct}

  pfst-hom : Pullback-group →ᴳ H
  pfst-hom = record {
    f = Pullback.a;
    pres-comp = λ _ _ → idp}

  psnd-hom : Pullback-group →ᴳ K
  psnd-hom = record {
    f = Pullback.b;
    pres-comp = λ _ _ → idp}

  module _ {l} {J : Group l} (χ : J →ᴳ H) (θ : J →ᴳ K) where

    private
      module χ = GroupHom χ
      module θ = GroupHom θ

    pullback-hom : ((j : Group.El J) → φ.f (χ.f j) == ψ.f (θ.f j))
      → J →ᴳ Pullback-group
    pullback-hom p = record {
      f = λ j → pullback (χ.f j) (θ.f j) (p j);
      pres-comp = λ j₁ j₂ → pullback= (group-cospan-out D)
        (χ.pres-comp j₁ j₂)
        (θ.pres-comp j₁ j₂)
        (prop-has-all-paths (Group.El-level G _ _) _ _)}

ext: agda

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- Lemmas related to bisimilarity and CCS, implemented using the
-- classical definition of bisimilarity
------------------------------------------------------------------------

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

open import Prelude

module Bisimilarity.CCS.Classical {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

import Bisimilarity.CCS.General
import Bisimilarity.Classical.Equational-reasoning-instances
open import Equational-reasoning
open import Labelled-transition-system.CCS Name
open import Relation

open import Bisimilarity.Classical CCS

------------------------------------------------------------------------
-- Various lemmas related to _∣_

-- _∣_ is commutative.

∣-comm : ∀ {P Q} → P ∣ Q ∼ Q ∣ P
∣-comm = ⟨ R , R-is-a-bisimulation , base ⟩
  where
  data R : Rel₂ ℓ (Proc ∞) where
    base : ∀ {P Q} → R (P ∣ Q , Q ∣ P)

  R-is-symmetric : ∀ {P Q} → R (P , Q) → R (Q , P)
  R-is-symmetric base = base

  R-is-a-bisimulation : Bisimulation R
  R-is-a-bisimulation =
    ⟪ lr , (λ PRQ tr →
              Σ-map id (Σ-map id R-is-symmetric)
                (lr (R-is-symmetric PRQ) tr)) ⟫
    where
    lr : ∀ {P P′ Q μ} →
         R (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × R (P′ , Q′)
    lr base (par-left  tr)  = _ , par-right tr , base
    lr base (par-right tr)  = _ , par-left  tr , base
    lr base (par-τ tr₁ tr₂) =
        _
      , par-τ tr₂ (subst (λ a → _ [ name a ]⟶ _)
                         (sym $ co-involutive _)
                         tr₁)
      , base

-- _∣_ is associative.

∣-assoc : ∀ {P Q R} → P ∣ (Q ∣ R) ∼ (P ∣ Q) ∣ R
∣-assoc = ⟨ S , S-is-a-bisimulation , base ⟩
  where
  data S : Rel₂ ℓ (Proc ∞) where
    base : ∀ {P Q R} → S (P ∣ (Q ∣ R) , (P ∣ Q) ∣ R)

  S-is-a-bisimulation : Bisimulation S
  S-is-a-bisimulation = ⟪ lr , rl ⟫
    where
    lr : ∀ {P P′ Q μ} →
         S (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × S (P′ , Q′)
    lr base (par-left tr)               = _ , par-left (par-left tr)    , base
    lr base (par-right (par-left tr))   = _ , par-left (par-right tr)   , base
    lr base (par-right (par-right tr))  = _ , par-right tr              , base
    lr base (par-right (par-τ tr₁ tr₂)) = _ , par-τ (par-right tr₁) tr₂ , base
    lr base (par-τ tr₁ (par-left tr₂))  = _ , par-left (par-τ tr₁ tr₂)  , base
    lr base (par-τ tr₁ (par-right tr₂)) = _ , par-τ (par-left tr₁) tr₂  , base

    rl : ∀ {P Q Q′ μ} →
         S (P , Q) → Q [ μ ]⟶ Q′ →
         ∃ λ P′ → P [ μ ]⟶ P′ × S (P′ , Q′)
    rl base (par-left (par-left tr))    = _ , par-left tr               , base
    rl base (par-left (par-right tr))   = _ , par-right (par-left tr)   , base
    rl base (par-left (par-τ tr₁ tr₂))  = _ , par-τ tr₁ (par-left tr₂)  , base
    rl base (par-right tr)              = _ , par-right (par-right tr)  , base
    rl base (par-τ (par-left tr₁) tr₂)  = _ , par-τ tr₁ (par-right tr₂) , base
    rl base (par-τ (par-right tr₁) tr₂) = _ , par-right (par-τ tr₁ tr₂) , base

-- ∅ is a left identity of _∣_.

∣-left-identity : ∀ {P} → ∅ ∣ P ∼ P
∣-left-identity = ⟨ R , R-is-a-bisimulation , base ⟩
  where
  data R : Rel₂ ℓ (Proc ∞) where
    base : ∀ {P} → R (∅ ∣ P , P)

  R-is-a-bisimulation : Bisimulation R
  R-is-a-bisimulation = ⟪ lr , rl ⟫
    where
    lr : ∀ {P P′ Q μ} →
         R (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × R (P′ , Q′)
    lr base (par-right tr) = _ , tr , base
    lr base (par-left ())
    lr base (par-τ () _)

    rl : ∀ {P Q Q′ μ} →
         R (P , Q) → Q [ μ ]⟶ Q′ →
         ∃ λ P′ → P [ μ ]⟶ P′ × R (P′ , Q′)
    rl base tr = _ , par-right tr , base

-- ∅ is a right identity of _∣_.

∣-right-identity : ∀ {P} → P ∣ ∅ ∼ P
∣-right-identity {P} =
  P ∣ ∅  ∼⟨ ∣-comm ⟩
  ∅ ∣ P  ∼⟨ ∣-left-identity ⟩■
  P

-- _∣_ preserves bisimilarity.

_∣-cong_ : ∀ {P P′ Q Q′} → P ∼ P′ → Q ∼ Q′ → P ∣ Q ∼ P′ ∣ Q′
P∼P′ ∣-cong Q∼Q′ with _⇔_.to (Bisimilarity↔ _) P∼P′
                    | _⇔_.to (Bisimilarity↔ _) Q∼Q′
... | L , L-bisim , PLP′
    | R , R-bisim , QRQ′ = ⟨ LR , ⟪ lr , rl ⟫ , base PLP′ QRQ′ ⟩
  where
  data LR : Rel₂ ℓ (Proc ∞) where
    base : ∀ {P P′ Q Q′} →
           L (P , P′) → R (Q , Q′) → LR (P ∣ Q , P′ ∣ Q′)

  lr : ∀ {P P′ Q μ} →
       LR (P , Q) → P [ μ ]⟶ P′ →
       ∃ λ Q′ → Q [ μ ]⟶ Q′ × LR (P′ , Q′)
  lr (base PLP′ QRQ′) (par-left tr) =
    Σ-map (_∣ _) (Σ-map par-left (flip base QRQ′))
      (left-to-right L-bisim PLP′ tr)

  lr (base PLP′ QRQ′) (par-right tr) =
    Σ-map (_ ∣_) (Σ-map par-right (base PLP′))
      (left-to-right R-bisim QRQ′ tr)

  lr (base PLP′ QRQ′) (par-τ tr₁ tr₂) =
    Σ-zip _∣_ (Σ-zip par-τ base)
      (left-to-right L-bisim PLP′ tr₁)
      (left-to-right R-bisim QRQ′ tr₂)

  rl : ∀ {P Q Q′ μ} →
       LR (P , Q) → Q [ μ ]⟶ Q′ →
       ∃ λ P′ → P [ μ ]⟶ P′ × LR (P′ , Q′)
  rl (base PLP′ QRQ′) (par-left tr) =
    Σ-map (_∣ _) (Σ-map par-left (flip base QRQ′))
      (right-to-left L-bisim PLP′ tr)

  rl (base PLP′ QRQ′) (par-right tr) =
    Σ-map (_ ∣_) (Σ-map par-right (base PLP′))
      (right-to-left R-bisim QRQ′ tr)

  rl (base PLP′ QRQ′) (par-τ tr₁ tr₂) =
    Σ-zip _∣_ (Σ-zip par-τ base)
      (right-to-left L-bisim PLP′ tr₁)
      (right-to-left R-bisim QRQ′ tr₂)

------------------------------------------------------------------------
-- Exercise 6.1.2 from "Enhancements of the bisimulation proof method"
-- by Pous and Sangiorgi

6-1-2 : ∀ {P} → ! P ∣ P ∼ ! P
6-1-2 {P} = ⟨ R , R-is-a-bisimulation , base ⟩
  where
  data R : Rel₂ ℓ (Proc ∞) where
    base : R (! P ∣ P , ! P)
    refl : ∀ {P} → R (P , P)

  R-is-a-bisimulation : Bisimulation R
  R-is-a-bisimulation = ⟪ lr , rl ⟫
    where
    lr : ∀ {P P′ Q μ} →
         R (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × R (P′ , Q′)
    lr base tr = _ , replication tr , refl
    lr refl tr = _ , tr             , refl

    rl : ∀ {P Q Q′ μ} →
         R (P , Q) → Q [ μ ]⟶ Q′ →
         ∃ λ P′ → P [ μ ]⟶ P′ × R (P′ , Q′)
    rl base (replication tr) = _ , tr , refl
    rl refl tr               = _ , tr , refl

------------------------------------------------------------------------
-- Exercise 6.1.3 (2) from "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi

open Bisimilarity.CCS.General.6-1-3-2 (record
       { _∼_       = _∼_
       ; step-∼    = step-∼
       ; finally-∼ = Equational-reasoning.finally₂
       ; reflexive = reflexive
       ; symmetric = symmetric
       ; ∣-comm    = ∣-comm
       ; ∣-assoc   = ∣-assoc
       ; _∣-cong_  = _∣-cong_
       ; 6-1-2     = 6-1-2
       })
       public using (swap-rightmost; 6-1-3-2)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

module Cubical.Categories.Functors.HomFunctor where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Constructions.BinProduct renaming (_×_ to _×C_)

private
  variable
    ℓC ℓC' : Level

module _ (C : Category ℓC ℓC') where

  open Functor
  open Category C

  HomFunctor : Functor (C ^op ×C C) (SET ℓC')
  F-ob HomFunctor (x , y) = Hom[ x , y ] , isSetHom
  F-hom HomFunctor {x , y} {x' , y'} (φ , ψ) θ = ψ ∘ (θ ∘ φ)
  F-id HomFunctor = funExt λ θ → ⋆IdR (id ⋆ θ) ∙ ⋆IdL θ
  F-seq HomFunctor {x , y} {x' , y'} {x'' , y''} (φ , ψ) (φ' , ψ') = funExt λ θ →
    ((φ' ⋆ φ) ⋆ θ) ⋆ (ψ ⋆ ψ')
      ≡⟨ sym (⋆Assoc ((φ' ⋆ φ) ⋆ θ) ψ ψ') ⟩
    (((φ' ⋆ φ) ⋆ θ) ⋆ ψ) ⋆ ψ'
      ≡⟨ cong (_⋆ ψ') (
        ((φ' ⋆ φ) ⋆ θ) ⋆ ψ
          ≡⟨ cong (_⋆ ψ) (⋆Assoc φ' φ θ) ⟩
        (φ' ⋆ (φ ⋆ θ)) ⋆ ψ
          ≡⟨ ⋆Assoc φ' (φ ⋆ θ) ψ ⟩
        φ' ⋆ ((φ ⋆ θ) ⋆ ψ) ∎
      ) ⟩
    (φ' ⋆ ((φ ⋆ θ) ⋆ ψ)) ⋆ ψ' ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --allow-exec #-}

module ExecAgda where

open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)

postulate
  execTC : String → List String → String → TC (Σ Nat (λ _ → Σ String (λ _ → String)))

{-# BUILTIN AGDATCMEXEC execTC #-}

macro
  test : Term → TC ⊤
  test hole = execTC "agda" ("-v0" ∷ "-i" ∷ "test/Succeed" ∷ "test/Succeed/exec-tc/empty.agda" ∷ []) ""
          >>= λ{(exitCode , (stdOut , stdErr)) → unify hole (lit (string stdOut))}

_ : test ≡ ""
_ = refl

max_stars_repo_name: Saizan/agda

max_issues_repo_name: Saizan/agda

max_forks_repo_name: Saizan/agda


text:
module Nat where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

infixl 60 _+_
infixl 70 _*_

_+_ : Nat -> Nat -> Nat
n + zero  = n
n + suc m = suc (n + m)

_*_ : Nat -> Nat -> Nat
n * zero  = zero
n * suc m = n * m + n

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}
{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
open import Prelude

module Implicits.Resolution.Termination.Lemmas.SizeMeasures
  where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Vec
open import Data.Fin.Substitution
open import Extensions.Vec
open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl)
open import Extensions.Nat
open import Implicits.Resolution.Termination.SizeMeasures

-- we can show that our size measure a ρ< b is well founded
-- by relating it to the well-foundedness proof of _<'_
open import Induction.WellFounded
ρ<-well-founded : Well-founded _ρ<_
ρ<-well-founded = sub.well-founded (image.well-founded <-well-founded)
    where
        open import Induction.Nat
        open import Data.Nat
        open import Data.Nat.Properties
        module sub = Inverse-image (λ{ (_ , a ) → || a ||})
        module image = Subrelation {A = ℕ} {_<_} {_<′_} ≤⇒≤′

open import Induction.WellFounded
hρ<-well-founded : Well-founded _hρ<_
hρ<-well-founded = sub.well-founded (image.well-founded <-well-founded)
  where
    open import Induction.Nat
    open import Data.Nat
    open import Data.Nat.Properties
    module sub = Inverse-image (λ{ (_ , a ) → h|| a ||})
    module image = Subrelation {A = ℕ} {_<_} {_<′_} ≤⇒≤′

m<-well-founded : Well-founded _m<_
m<-well-founded = sub.well-founded (image.well-founded <-well-founded)
    where
        module sub = Inverse-image (λ{ (_ , _ , a) → m|| a ||})
        module image = Subrelation {A = ℕ} {_<_} {_<′_} ≤⇒≤′

module TypeSubstSizeLemmas where
  open MetaTypeTypeSubst

  mutual
    ||a/Var|| : ∀ {m ν μ} (a : MetaType m ν) (s : Sub Fin ν μ) →
                m|| a /Var s || ≡ m|| a ||
    ||a/Var|| (a ⇒ b) s = cong₂ (λ u v → 1 + u + v) (||a/Var|| a s) (||a/Var|| b s)
    ||a/Var|| (∀' a) s = cong (λ u → 1 + u) (||a/Var|| a (s VarSubst.↑))
    ||a/Var|| (simpl (tvar x)) s = refl
    ||a/Var|| (simpl (mvar x)) s = refl
    ||a/Var|| (simpl (a →' b)) s = cong₂ (λ u v → 1 + u + v) (||a/Var|| a s) (||a/Var|| b s)
    ||a/Var|| (simpl (tc c)) s = refl

    ||weaken-a|| : ∀ {m ν} (a : MetaType m ν) → m|| weaken a || ≡ m|| a ||
    ||weaken-a|| {m} {ν} a = begin
      m|| weaken a ||
        ≡⟨ refl ⟩
      m|| a /Var VarSubst.wk ||
        ≡⟨ ||a/Var|| a VarSubst.wk ⟩
      m|| a || ∎

    ||s↑|| : ∀ {m ν μ} (s : Sub (MetaType m) ν μ) →
                       (∀ (x : Fin ν) → m|| lookup x s || ≡ 1) →
                       ∀ y → m|| lookup y (s ↑) || ≡ 1
    ||s↑|| s p zero = refl
    ||s↑|| s p (suc y) = begin
      m|| lookup y (map weaken s) ||
        ≡⟨ cong m||_|| (sym $ lookup⋆map s weaken y) ⟩
      m|| weaken (lookup y s) ||
        ≡⟨ ||weaken-a|| (lookup y s) ⟩
      m|| (lookup y s) ||
        ≡⟨ p y ⟩
      1 ∎

    ||a/s|| : ∀ {m ν μ} (a : MetaType m ν) (s : Sub (MetaType m) ν μ) →
             (∀ x → m|| lookup x s || ≡ 1) →
             m|| a / s || ≡ m|| a ||
    ||a/s|| (a ⇒ b) s p = cong₂ (λ u v → 1 + u + v) (||a/s|| a s p) (||a/s|| b s p)
    ||a/s|| (∀' a) s p = cong (λ u → 1 + u) (||a/s|| a (s ↑) (||s↑|| s p))
    ||a/s|| {m} {ν} (simpl (tvar x)) s p = begin
      m|| (simpl (tvar x)) / s ||
        ≡⟨ cong m||_|| (MetaTypeTypeLemmas.var-/ {x = x}) ⟩
      m|| lookup x s ||
        ≡⟨ p x ⟩
      1 ∎
    ||a/s|| (simpl (mvar x)) s p = refl
    ||a/s|| (simpl (a →' b)) s p = cong₂ (λ u v → 1 + u + v) (||a/s|| a s p) (||a/s|| b s p)
    ||a/s|| (simpl (tc c)) s p = refl

module MetaSubstSizeLemmas where
  open MetaTypeMetaSubst hiding (open-meta)

  mutual
    ||a/Var|| : ∀ {ν m n} (a : MetaType m ν) (s : Sub Fin m n) →
                m|| a /Var s || ≡ m|| a ||
    ||a/Var|| (a ⇒ b) s = cong₂ (λ u v → 1 + u + v) (||a/Var|| a s) (||a/Var|| b s)
    ||a/Var|| {ν = ν} (∀' a) s =
      cong (λ u → 1 + u) (||a/Var|| a ((varLift MetaLift.↑tp) {ν = ν} s))
    ||a/Var|| (simpl (tvar x)) s = refl
    ||a/Var|| (simpl (mvar x)) s = refl
    ||a/Var|| (simpl (a →' b)) s = cong₂ (λ u v → 1 + u + v) (||a/Var|| a s) (||a/Var|| b s)
    ||a/Var|| (simpl (tc c)) s = refl

    ||weaken-a|| : ∀ {m ν} (a : MetaType m ν) → m|| weaken a || ≡ m|| a ||
    ||weaken-a|| {m} {ν} a = begin
      m|| weaken a ||
        ≡⟨ refl ⟩
      m|| a /Var VarSubst.wk ||
        ≡⟨ ||a/Var|| a VarSubst.wk ⟩
      m|| a || ∎

    ||s↑|| : ∀ {m ν μ} (s : Sub (MetaType m) ν μ) →
                       (∀ (x : Fin ν) → m|| lookup x s || ≡ 1) →
                       ∀ y → m|| lookup y (s ↑) || ≡ 1
    ||s↑|| s p zero = refl
    ||s↑|| s p (suc y) = begin
      m|| lookup y (map weaken s) ||
        ≡⟨ cong m||_|| (sym $ lookup⋆map s weaken y) ⟩
      m|| weaken (lookup y s) ||
        ≡⟨ ||weaken-a|| (lookup y s) ⟩
      m|| (lookup y s) ||
        ≡⟨ p y ⟩
      1 ∎

    ||a/s|| : ∀ {m ν n} (a : MetaType m ν) (s : Sub (flip MetaType ν) m n) →
             (∀ x → m|| lookup x s || ≡ 1) →
             m|| a / s || ≡ m|| a ||
    ||a/s|| (a ⇒ b) s p = cong₂ (λ u v → 1 + u + v) (||a/s|| a s p) (||a/s|| b s p)
    ||a/s|| (∀' a) s p = cong (λ u → 1 + u) (||a/s|| a (map MetaTypeTypeSubst.weaken s) lem)
      where
        lem : ∀ x → m|| lookup x (map MetaTypeTypeSubst.weaken s) || ≡ 1
        lem x = begin
          m|| lookup x (map MetaTypeTypeSubst.weaken s) ||
            ≡⟨ cong m||_|| (sym $ lookup⋆map s _ x) ⟩
          m|| MetaTypeTypeSubst.weaken (lookup x s) ||
            ≡⟨ TypeSubstSizeLemmas.||weaken-a|| (lookup x s) ⟩
          m|| lookup x s ||
            ≡⟨ p x ⟩
          1 ∎
    ||a/s|| {m} {ν} (simpl (mvar x)) s p = begin
      m|| (simpl (mvar x)) / s ||
        ≡⟨ cong m||_|| (MetaTypeTypeLemmas.var-/ {x = x}) ⟩
      m|| lookup x s ||
        ≡⟨ p x ⟩
      1 ∎
    ||a/s|| (simpl (tvar x)) s p = refl
    ||a/s|| (simpl (a →' b)) s p = cong₂ (λ u v → 1 + u + v) (||a/s|| a s p) (||a/s|| b s p)
    ||a/s|| (simpl (tc c)) s p = refl

    ||open-meta-a||≡a : ∀ {m ν} (a : MetaType m (suc ν)) → m|| open-meta a || ≡ m|| a ||
    ||open-meta-a||≡a {m} {ν} a = begin
      m|| open-meta a ||
        ≡⟨ TypeSubstSizeLemmas.||a/s|| (MMS.weaken a) (MTS.sub (simpl (mvar zero))) lem ⟩
      m|| (MMS.weaken a) ||
        ≡⟨ ||weaken-a|| a ⟩
      m|| a || ∎
        where
          module MMS = MetaTypeMetaSubst
          module MTS = MetaTypeTypeSubst
          lem : ∀ (x : Fin (suc ν)) → m|| lookup x (MetaTypeTypeSubst.sub (simpl (mvar zero))) || ≡ 1
          lem zero = refl
          lem (suc x) =
            cong m||_|| (MetaTypeTypeLemmas.lookup-sub-↑⋆ {t = (simpl (mvar zero))} zero x)

module SubstSizeLemmas where
  open TypeLemmas

  mutual
    ||a|| : ∀ {ν} (a : Type ν) → || a || ≥ 1
    ||a|| (simpl (tc x)) = s≤s z≤n
    ||a|| (simpl (tvar n)) = s≤s z≤n
    ||a|| (simpl (a →' b)) = s≤s z≤n
    ||a|| (a ⇒ b) = s≤s z≤n
    ||a|| (∀' a) = s≤s z≤n

    ||a/Var|| : ∀ {ν μ} (a : Type ν) (s : Sub Fin ν μ) → || a /Var s || ≡ || a ||
    ||a/Var|| (a ⇒ b) s = cong₂ (λ u v → 1 + u + v) (||a/Var|| a s) (||a/Var|| b s)
    ||a/Var|| (∀' a) s = cong (λ u → 1 + u) (||a/Var|| a (s VarSubst.↑))
    ||a/Var|| (simpl (tvar x)) s = refl
    ||a/Var|| (simpl (a →' b)) s = cong₂ (λ u v → 1 + u + v) (||a/Var|| a s) (||a/Var|| b s)
    ||a/Var|| (simpl (tc c)) s = refl

    ||weaken-a|| : ∀ {ν} (a : Type ν) → || weaken a || ≡ || a ||
    ||weaken-a|| {ν} a = begin
      || weaken a ||
        ≡⟨ refl ⟩
      || a /Var VarSubst.wk ||
        ≡⟨ ||a/Var|| a VarSubst.wk ⟩
      || a || ∎

    ||s↑|| : ∀ {ν μ} (s : Sub Type ν μ) →
                       (∀ (x : Fin ν) → || lookup x s || ≡ 1) →
                       ∀ y → || lookup y (s ↑) || ≡ 1
    ||s↑|| s p zero = refl
    ||s↑|| s p (suc y) = begin
      || lookup y (map weaken s) ||
        ≡⟨ cong ||_|| (sym $ lookup⋆map s weaken y) ⟩
      || weaken (lookup y s) ||
        ≡⟨ ||weaken-a|| (lookup y s) ⟩
      || (lookup y s) ||
        ≡⟨ p y ⟩
      1 ∎

    ||a/s|| : ∀ {ν μ} (a : Type ν) (s : Sub Type ν μ) →
             (∀ x → || lookup x s || ≡ 1) →
             || a / s || ≡ || a ||
    ||a/s|| (a ⇒ b) s p = cong₂ (λ u v → 1 + u + v) (||a/s|| a s p) (||a/s|| b s p)
    ||a/s|| (∀' a) s p = cong (λ u → 1 + u) (||a/s|| a (s ↑) (||s↑|| s p))
    ||a/s|| {m} {ν} (simpl (tvar x)) s p = begin
      || (simpl (tvar x)) / s ||
        ≡⟨ cong ||_|| (var-/ {x = x}) ⟩
      || lookup x s ||
        ≡⟨ p x ⟩
      1 ∎
    ||a/s|| (simpl (a →' b)) s p = cong₂ (λ u v → 1 + u + v) (||a/s|| a s p) (||a/s|| b s p)
    ||a/s|| (simpl (tc c)) s p = refl

    ||a/wk↑k|| : ∀ {ν} k (a : Type (k + ν)) → || a / wk ↑⋆ k || ≡ || a ||
    ||a/wk↑k|| k a = ||a/s|| a (wk ↑⋆ k) (λ x → cong ||_|| (lookup-wk-↑⋆ k x))

    ||a/s||' : ∀ {ν μ} (a : Type ν) (s : Sub Type ν μ) → || a || ≤ || a / s ||
    ||a/s||' (simpl (tc x)) s = s≤s z≤n
    ||a/s||' (simpl (tvar n)) s = ||a|| (lookup n s)
    ||a/s||' (simpl (a →' b)) s = s≤s (<-+ (||a/s||' a s) (||a/s||' b s))
    ||a/s||' (a ⇒ b) s = s≤s (<-+ (||a/s||' a s) (||a/s||' b s))
    ||a/s||' (∀' b) s = s≤s (||a/s||' b (s TypeSubst.↑))

    h||a/s|| : ∀ {ν μ} (a : Type ν) (s : Sub Type ν μ) → (, a) hρ≤ (, a / s)
    h||a/s|| (simpl (tc x)) s = s≤s z≤n
    h||a/s|| (simpl (tvar n)) s = ||a|| (proj₂ (lookup n s ◁))
    h||a/s|| (simpl (a →' b)) s = s≤s (<-+ (||a/s||' a s) (||a/s||' b s))
    h||a/s|| (a ⇒ b) s = h||a/s|| b s
    h||a/s|| (∀' b) s = h||a/s|| b (s TypeSubst.↑)

a-ρ<-∀a : ∀ {n} a → (suc n , a) ρ< (, ∀' a)
a-ρ<-∀a _ = ≤-refl

b-ρ<-a⇒b : ∀ {ν} (a b : Type ν) → (_ , b) ρ< (_ , a ⇒ b)
b-ρ<-a⇒b a b = s≤s (≤-steps || a || ≤-refl)

b-hρ≤-a⇒b : ∀ {ν} (a b : Type ν) → (_ , b) hρ≤ (_ , a ⇒ b)
b-hρ≤-a⇒b a b = subst (λ u → u ≤ h|| a ⇒ b ||) refl ≤-refl

a-m<-∀a : ∀ {m ν} a → (m , suc ν , a) m< (m , ν , ∀' a)
a-m<-∀a a = ≤-refl

b-m<-a⇒b : ∀ {m ν} a b → (m , ν , b) m< (m , ν , a ⇒ b)
b-m<-a⇒b a b = s≤s (≤-steps m|| a || ≤-refl)

open-meta-a-m<-∀'a : ∀ {m ν} a → (suc m , ν , open-meta a) m< (m , ν , ∀' a)
open-meta-a-m<-∀'a a = subst (λ x → x < m||  ∀' a ||)
  (sym $ MetaSubstSizeLemmas.||open-meta-a||≡a a) (a-m<-∀a a)


text:
module Thesis.ANormalCTerm where

open import Thesis.ANormalDTerm

-- OK, this is all cool, but let's drop all this typing.
data CType : Set where
  cache : CType
  input : Type → CType

open import Data.Product

⟦_⟧CType : CType → Set
-- This is a lie, since we might need to store more complex values in there,
-- including caches...
⟦ cache ⟧CType = Σ[ τ ∈ Type ] ⟦ τ ⟧Type
-- However, this is more correct but is not recognized as terminating.
-- ⟦ cache ⟧CType = Σ[ τ ∈ CType ] ⟦ τ ⟧CType
-- Finally, this definition is too impredicative for Agda to accept it. If
-- ⟦_⟧CType lived in Set₁, it could still not contain values of itself.
-- ⟦ cache ⟧CType = Σ[ S ∈ Set ] S
⟦ input τ ⟧CType = ⟦ τ ⟧Type

-- Maybe step-indexing to the rescue. Really not sure how to step-index the theorems?
-- Maybe compute the needed index while running the base program?
open import Data.Nat
⟦_⟧CTypeN : CType → ℕ → Set
⟦ input τ ⟧CTypeN n = ⟦ τ ⟧Type
⟦ cache ⟧CTypeN 0 = ⊤
⟦ cache ⟧CTypeN (suc n) = Σ[ τ ∈ CType ] ⟦ τ ⟧CTypeN n

-- To top it off, maybe add constructor tcache : CType × ℕ → Type t? Hm, guess
-- that would loop. Just use big-step semantics then.

open import Base.Syntax.Context CType using () renaming (Context to CCtx)
open import Base.Denotation.Environment CType ⟦_⟧CType using () renaming (⟦_⟧Context to ⟦_⟧CCtx)

-- I must merge caches and normal types. So I must step-index types?
data CTerm : (C CFin : CCtx) (Δ : Context) (τ : Type) → Set where
  cvar : ∀ {CFin Δ τ} (x : Var Δ τ) →
    CTerm CFin CFin Δ τ
  clett : ∀ {C CFin Δ τ σ τ₁} →
    (f : Var Δ (σ ⇒ τ₁)) →
     -- XXX: (f : Var Δ (σ ⇒ (pair τ₁ cache))) →
    (x : Var Δ σ) →
    -- XXX pretend we only store integers. We should instead use a separate type of caches.
    (ct : CTerm (cache • C) CFin (τ₁ • Δ) τ) →
    CTerm C CFin Δ τ

-- Rather bogus: the contexts are unchanged. Our functions have a different type here!
⟦_⟧CTerm : ∀ {C CFin Δ τ} → CTerm C CFin Δ τ → ⟦ Δ ⟧Context → ⟦ C ⟧CCtx → (⟦ τ ⟧Type × ⟦ CFin ⟧CCtx)
⟦ cvar x ⟧CTerm ρ c = ⟦ x ⟧Var ρ , c
⟦ clett f x ct ⟧CTerm ρ c =
  let v = ⟦ f ⟧Var ρ (⟦ x ⟧Var ρ)
  in ⟦ ct ⟧CTerm (v • ρ) ((_ , v) • c)

cache-term-cps : ∀ {Δ σ} {Z : Set} → (t : Term Δ σ) → ∀ C → (∀ CFin → CTerm C CFin Δ σ → Z) → Z
cache-term-cps (var x) C k = k C (cvar x)
cache-term-cps (lett f x t) C k = cache-term-cps t (cache • C) (λ CFin ct → k CFin (clett f x ct))

cache-term-Σ : ∀ {Δ σ} → (t : Term Δ σ) → ∀ C → Σ[ CFin ∈ CCtx ] CTerm C CFin Δ σ
cache-term-Σ (var x) CFin = CFin , cvar x
cache-term-Σ (lett f x t) C =
  let CFin , ct = cache-term-Σ t (cache • C)
  in CFin , clett f x ct
-- clett f x (cache-term t)
-- -- ⟦_⟧CType : Type → Context → Set
-- -- ⟦ σ ⇒ τ ⟧CType C = {!!}
-- -- ⟦ pair σ τ ⟧CType C = {!!}
-- -- ⟦ sum σ τ ⟧CType C = {!!}
-- -- ⟦ unit ⟧CType C = ⟦ unit ⟧Type × ⟦ C ⟧Context
-- -- ⟦ int ⟧CType C = {!!}

-- data CFun (C CFin : Context) : (Δ : Context) (τ : Type) → Set where
--   cabs : ∀ {σ τ Δ} → CFun (σ • C) CFin (σ • Δ) τ → CFun C CFin Δ (σ ⇒ τ)
--   cterm : ∀ {τ Δ} → CTerm C CFin Δ τ → CFun C CFin Δ τ

-- -- Ouch, this is a lie.... We'd need a different type structure.
-- ⟦_⟧CFun : ∀ {C CFin Δ τ} → CFun C CFin Δ τ → ⟦ Δ ⟧Context → ⟦ C ⟧Context → (⟦ τ ⟧Type × ⟦ CFin ⟧Context)
-- ⟦ cabs cf ⟧CFun ρ c = (λ v → proj₁ (⟦ cf ⟧CFun (v • ρ) (v • c))) , {!!}
-- ⟦ cterm ct ⟧CFun ρ c = ⟦ ct ⟧CTerm ρ c

-- ⟦_⟧CFun2 : ∀ {C CFin Δ σ τ} → CFun C CFin Δ (σ ⇒ τ) → ⟦ Δ ⟧Context → ⟦ C ⟧Context → ⟦ σ ⟧Type → (⟦ τ ⟧Type × ⟦ CFin ⟧Context)
-- ⟦ cabs cf ⟧CFun2 ρ c = λ v → (⟦ cf ⟧CFun (v • ρ) (v • c))
-- -- (λ v → proj₁ (⟦ cf ⟧CFun (v • ρ) (v • c))) , {!!}
-- ⟦ cterm ct ⟧CFun2 ρ c = {! ⟦ ct ⟧CTerm ρ c!}

-- Above we run into the usual problems with nested caching.
data CFunR (C CFin : CCtx) : (Δ : Context) (τ : Type) → Set where
  cabsterm : ∀ {σ τ Δ} → CTerm (input σ • C) CFin (σ • Δ) τ → CFunR C CFin Δ (σ ⇒ τ)

⟦_⟧CFunR : ∀ {C CFin Δ σ τ} → CFunR C CFin Δ (σ ⇒ τ) → ⟦ Δ ⟧Context → ⟦ C ⟧CCtx → ⟦ σ ⟧Type → (⟦ τ ⟧Type × ⟦ CFin ⟧CCtx)
⟦ cabsterm ct ⟧CFunR ρ c v = ⟦ ct ⟧CTerm (v • ρ) (v • c)

-- IMPORTANT: Here we need different change types:
ΔτC : Type → Type
ΔτC (σ ⇒ τ) = ΔτC σ ⇒ ΔτC τ
ΔτC unit = unit
ΔτC int = int
ΔτC (pair σ τ) = pair (ΔτC σ) (ΔτC τ)
ΔτC (sum σ τ) = sum (sum (ΔτC σ) (ΔτC τ)) (sum σ τ)

ΔΔC : Context → Context
ΔΔC ∅ = ∅
ΔΔC (τ • Γ) = ΔτC τ • ΔΔC Γ

derive-dcvar : ∀ {Δ σ} → (x : Var Δ σ) → Var (ΔΔC Δ) (ΔτC σ)
derive-dcvar this = this
derive-dcvar (that x) = that (derive-dcvar x)

-- REAL BULLSHIT
-- XXX Not accounted for: derivatives also take caches!
-- C: accumulated caches. CFin: the ones we have at the end.
data CDTerm : (C CFin : CCtx) (Δ : Context) (τ : Type) → Set where
  cdvar : ∀ {CFin Δ τ} (x : Var (ΔΔC Δ) (ΔτC τ)) →
    CDTerm CFin CFin Δ τ
  cdlett : ∀ {C CFin Δ τ σ τ₁} →
    -- Here, we also need to pass (and update) the RIGHT cache. Otherwise
    -- there's no point.
    (df : Var (ΔΔC Δ) (ΔτC (σ ⇒ τ₁))) →
    (dx : Var (ΔΔC Δ) (ΔτC σ)) →
    (dt : CDTerm (cache • C) CFin (τ₁ • Δ) τ) →
    CDTerm C CFin Δ τ

der-cache-term-Σ : ∀ {Δ σ} → (t : Term Δ σ) → ∀ C → Σ[ CFin ∈ CCtx ] CDTerm C CFin Δ σ
der-cache-term-Σ (var x) CFin = CFin , cdvar (derive-dcvar x)
der-cache-term-Σ (lett f x t) C =
  let CFin , cdt = der-cache-term-Σ t (cache • C)
  in CFin , cdlett (derive-dcvar f) (derive-dcvar x) cdt

--⟦_⟧DTerm : ∀ {Δ τ} → DTerm Δ τ → ⟦ Δ ⟧Context → ⟦ ΔΔ Δ ⟧Context → ⟦ Δt τ ⟧Type
⟦_⟧CDTerm : ∀ {C CFin Δ τ} → CDTerm C CFin Δ τ → ⟦ ΔΔC Δ ⟧Context → ⟦ C ⟧CCtx → (⟦ ΔτC τ ⟧Type × ⟦ CFin ⟧CCtx)
⟦ cdvar x ⟧CDTerm dρ c = ⟦ x ⟧Var dρ , c
⟦ cdlett df dx cdt ⟧CDTerm dρ c =
  let dv = ⟦ df ⟧Var dρ (⟦ dx ⟧Var dρ)
  in ⟦ cdt ⟧CDTerm (dv • dρ) ((_ , dv) • c)

-- ⟦ cvar x ⟧CTerm ρ c = ⟦ x ⟧Var ρ , c
-- ⟦ clett f x ct ⟧CTerm ρ c =
--   let v = ⟦ f ⟧Var ρ (⟦ x ⟧Var ρ)
--   in ⟦ ct ⟧CTerm (v • ρ) ((_ , v) • c)

-- At the top, C is empty.
data CDFun (C CFin : CCtx) : (Δ : Context) (τ : Type) → Set where
  cdabs : ∀ {σ τ Δ} → CDFun (input σ • C) CFin (σ • Δ) τ → CDFun C CFin Δ (σ ⇒ τ)
  cdterm : ∀ {τ Δ} → CDTerm C CFin Δ τ → CDFun C CFin Δ τ

data CDFunR (C CFin : CCtx) : (Δ : Context) (τ : Type) → Set where
  cdabsterm : ∀ {σ τ Δ} → CDTerm (input σ • C) CFin (σ • Δ) τ → CDFunR C CFin Δ (σ ⇒ τ)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Int where

open import Data.Product
open import Data.Sum as S
open import Relation.Binary.PropositionalEquality as Eq
open import Relation.Binary.Core
open import Relation.Binary
open import Function.Equality hiding (cong)
open import Data.Empty
import Level
open import Nat

open Eq.≡-Reasoning

ℤb : Set
ℤb = ℕ × ℕ

_≡ℤ_ : ℤb → ℤb → Set
(a , b) ≡ℤ (c , d) = a + d ≡ b + c

reflexive : {x : ℤb} → x ≡ℤ x
reflexive {a , b} = +-comm a b
symmetric : (x y : ℤb) → x ≡ℤ y → y ≡ℤ x
symmetric (a , b) (c , d) a+d≡b+c = begin
        c + b
    ≡⟨ +-comm c b ⟩
        b + c
    ≡⟨ sym a+d≡b+c ⟩
        a + d
    ≡⟨ +-comm a d ⟩
        d + a
    ∎
transitive : ∀ {x y z : ℤb} → x ≡ℤ y → y ≡ℤ z → x ≡ℤ z
transitive {a , b} {c , d} {e , f} a+d≡b+c c+f≡d+e = lem (begin
        a + ((d + c) + f)
    ≡⟨ cong (λ x → a + x) (sym (+-assoc d c f)) ⟩
        a + (d + (c + f))
    ≡⟨ +-assoc a d (c + f) ⟩
        (a + d) + (c + f)
    ≡⟨ cong (λ x → x + (c + f)) a+d≡b+c ⟩
        (b + c) + (c + f)
    ≡⟨ cong (λ x → (b + c) + x) c+f≡d+e ⟩
        (b + c) + (d + e)
    ≡⟨ sym (+-assoc b c (d + e)) ⟩
        b + (c + (d + e))
    ≡⟨ cong (λ x → b + x) (+-assoc c d e) ⟩
        b + ((c + d) + e)
    ∎)
    where
    lem : (a + ((d + c) + f)) ≡ (b + ((c + d) + e)) → (a + f) ≡ (b + e)
    lem p = +-rCancel (a + f) (b + e) (d + c) (begin
            (a + f) + (d + c)
        ≡⟨ sym (+-assoc a f (d + c)) ⟩
            a + (f + (d + c))
        ≡⟨ cong (λ x → a + x) (+-comm f (d + c)) ⟩
            a + ((d + c) + f)
        ≡⟨ p ⟩
            b + ((c + d) + e)
        ≡⟨ cong (λ x → b + x) (cong (λ x → x + e) (+-comm c d)) ⟩
            b + ((d + c) + e)
        ≡⟨ cong (λ x → b + x) (+-comm (d + c) e) ⟩
            b + (e + (d + c))
        ≡⟨ +-assoc b e (d + c) ⟩
            (b + e) + (d + c)
        ∎)

≡ℤ-eq : IsEquivalence _≡ℤ_
≡ℤ-eq = record
        { refl = λ {x} → reflexive {x}
        ; sym = λ {x y} → symmetric x y
        ; trans = λ {x y z} → transitive {x} {y} {z} }

ℤ : Setoid (Level.zero) (Level.zero)
ℤ = record { Carrier = ℤb ; _≈_ = _≡ℤ_ ; isEquivalence = ≡ℤ-eq }

≡ℤ-≡ : {a b : ℤb} → a ≡ b → a ≡ℤ b
≡ℤ-≡ {x , y} {.(x , y)} refl = +-comm x y

import Relation.Binary.EqReasoning as EqR
open EqR ℤ renaming
    ( begin_ to beginℤ_
    ; _≡⟨_⟩_ to _≡ℤ⟨_⟩_
    ; _∎ to _ℤ∎
    )

_+ℤ_ : ℤb → ℤb → ℤb
(a , b) +ℤ (c , d) = (a + c , b + d)

_*ℤ_ : ℤb → ℤb → ℤb
(a , b) *ℤ (c , d) = ((a * c) + (b * d) , (a * d) + (b * c))

+ℤ-lUniv : (a b c : ℤb) → a ≡ℤ b → (a +ℤ c) ≡ℤ (b +ℤ c)
+ℤ-lUniv (a₁ , a₂) (b₁ , b₂) (c₁ , c₂) a₁+b₂≡a₂+b₁ = lem
    where
        lem : (a₁ + c₁) + (b₂ + c₂) ≡ (a₂ + c₂) + (b₁ + c₁)
        lem = begin
                (a₁ + c₁) + (b₂ + c₂)
            ≡⟨ sym (+-assoc a₁ c₁ (b₂ + c₂)) ⟩
                a₁ + (c₁ + (b₂ + c₂))
            ≡⟨ cong (λ x → a₁ + x) (+-assoc c₁ b₂ c₂) ⟩
                a₁ + ((c₁ + b₂) + c₂)
            ≡⟨ cong (λ x → a₁ + x) (cong (λ x → x + c₂) (+-comm c₁ b₂)) ⟩
                a₁ + ((b₂ + c₁) + c₂)
            ≡⟨ cong (λ x → a₁ + x) (sym (+-assoc b₂ c₁ c₂)) ⟩
                a₁ + (b₂ + (c₁ + c₂))
            ≡⟨ +-assoc a₁ b₂ (c₁ + c₂) ⟩
                (a₁ + b₂) + (c₁ + c₂)
            ≡⟨ cong (λ x → x + (c₁ + c₂)) a₁+b₂≡a₂+b₁ ⟩
                (a₂ + b₁) + (c₁ + c₂)
            ≡⟨ sym (+-assoc a₂ b₁ (c₁ + c₂)) ⟩
                a₂ + (b₁ + (c₁ + c₂))
            ≡⟨ cong (λ x → a₂ + x) (+-assoc b₁ c₁ c₂) ⟩
                a₂ + ((b₁ + c₁) + c₂)
            ≡⟨ cong (λ x → a₂ + x) (+-comm (b₁ + c₁) c₂) ⟩
                a₂ + (c₂ + (b₁ + c₁))
            ≡⟨ +-assoc a₂ c₂ (b₁ + c₁) ⟩
                (a₂ + c₂) + (b₁ + c₁)
            ∎

-- c +ℤ a = (c₁ + a₁ , c₂ + a₂)
-- c +ℤ b = (c₁ + b₁ , c₂ + b₂)
-- (c₁ + a₁) + (c₂ + b₂) ≡ (c₂ + a₂) + (c₁ + b₁)
+ℤ-rUniv : (a b c : ℤb) → a ≡ℤ b → (c +ℤ a) ≡ℤ (c +ℤ b)
+ℤ-rUniv (a₁ , a₂) (b₁ , b₂) (c₁ , c₂) a₁+b₂≡a₂+b₁ = begin
        (c₁ + a₁) + (c₂ + b₂)
    ≡⟨ cong (λ x → (c₁ + a₁) + x) (+-comm c₂ b₂) ⟩
        (c₁ + a₁) + (b₂ + c₂)
    ≡⟨ sym (+-assoc c₁ a₁ (b₂ + c₂)) ⟩
        c₁ + (a₁ + (b₂ + c₂))
    ≡⟨ cong (λ x → c₁ + x) (+-assoc a₁ b₂ c₂) ⟩
        c₁ + ((a₁ + b₂) + c₂)
    ≡⟨ cong (λ x → c₁ + (x + c₂)) a₁+b₂≡a₂+b₁ ⟩
        c₁ + ((a₂ + b₁) + c₂)
    ≡⟨ +-comm c₁ ((a₂ + b₁) + c₂) ⟩
        ((a₂ + b₁) + c₂) + c₁
    ≡⟨ cong (λ x → x + c₁) (+-comm (a₂ + b₁) c₂) ⟩
        (c₂ + (a₂ + b₁)) + c₁
    ≡⟨ sym (+-assoc c₂ (a₂ + b₁) c₁) ⟩
        c₂ + ((a₂ + b₁) + c₁)
    ≡⟨ cong (λ x → c₂ + x) (sym (+-assoc a₂ b₁ c₁)) ⟩
        c₂ + (a₂ + (b₁ + c₁))
    ≡⟨ cong (λ x → c₂ + (a₂ + x)) (+-comm b₁ c₁) ⟩
        c₂ + (a₂ + (c₁ + b₁))
    ≡⟨ +-assoc c₂ a₂ (c₁ + b₁) ⟩
        (c₂ + a₂) + (c₁ + b₁)
    ∎

*ℤ-lUniv : (a b c : ℤb) → a ≡ℤ b → (a *ℤ c) ≡ℤ (b *ℤ c)
*ℤ-lUniv (a₁ , a₂) (b₁ , b₂) (c₁ , c₂) a₁+b₂≡a₂+b₁ = lem
    where
        -- a *ℤ c = (a₁ * c₁ + a₂ * c₂ , a₁ * c₂ + a₂ * c₁)
        -- b *ℤ c = (b₁ * c₁ + b₂ * c₂ , b₁ * c₂ + b₂ * c₁)
        lem : ((a₁ * c₁) + (a₂ * c₂)) + ((b₁ * c₂) + (b₂ * c₁))
                ≡ ((a₁ * c₂) + (a₂ * c₁)) + ((b₁ * c₁) + (b₂ * c₂))
        lem = begin
                ((a₁ * c₁) + (a₂ * c₂)) + ((b₁ * c₂) + (b₂ * c₁))
            ≡⟨ cong (λ x → ((a₁ * c₁) + (a₂ * c₂)) + x) (+-comm (b₁ * c₂) (b₂ * c₁)) ⟩
                ((a₁ * c₁) + (a₂ * c₂)) + ((b₂ * c₁) + (b₁ * c₂))
            ≡⟨ sym (+-assoc (a₁ * c₁) (a₂ * c₂) ((b₂ * c₁) + (b₁ * c₂))) ⟩
                (a₁ * c₁) + ((a₂ * c₂) + ((b₂ * c₁) + (b₁ * c₂)))
            ≡⟨ cong (λ x → (a₁ * c₁) + x) (+-assoc (a₂ * c₂) (b₂ * c₁) (b₁ * c₂)) ⟩
                (a₁ * c₁) + (((a₂ * c₂) + (b₂ * c₁)) + (b₁ * c₂))
            ≡⟨ cong (λ x → (a₁ * c₁) + x) (cong (λ x → x + (b₁ * c₂)) (+-comm (a₂ * c₂) (b₂ * c₁))) ⟩
                (a₁ * c₁) + (((b₂ * c₁) + (a₂ * c₂)) + (b₁ * c₂))
            ≡⟨ cong (λ x → (a₁ * c₁) + x) (sym (+-assoc (b₂ * c₁) (a₂ * c₂) (b₁ * c₂))) ⟩
                (a₁ * c₁) + ((b₂ * c₁) + ((a₂ * c₂) + (b₁ * c₂)))
            ≡⟨ +-assoc (a₁ * c₁) (b₂ * c₁) ((a₂ * c₂) + (b₁ * c₂)) ⟩
                ((a₁ * c₁) + (b₂ * c₁)) + ((a₂ * c₂) + (b₁ * c₂))
            ≡⟨ cong (λ x → x + ((a₂ * c₂) + (b₁ * c₂))) (sym (+*-rDist a₁ b₂ c₁))  ⟩
                ((a₁ + b₂) * c₁) + ((a₂ * c₂) + (b₁ * c₂))
            ≡⟨ cong (λ x → ((a₁ + b₂) * c₁) + x) (sym (+*-rDist a₂ b₁ c₂)) ⟩
                ((a₁ + b₂) * c₁) + ((a₂ + b₁) * c₂)
            ≡⟨ cong (λ x → x + ((a₂ + b₁) * c₂)) (cong (λ x → x * c₁) a₁+b₂≡a₂+b₁) ⟩
                ((a₂ + b₁) * c₁) + ((a₂ + b₁) * c₂)
            ≡⟨ cong (λ x → ((a₂ + b₁) * c₁) + x) (cong (λ x → x * c₂) (sym a₁+b₂≡a₂+b₁)) ⟩
                ((a₂ + b₁) * c₁) + ((a₁ + b₂) * c₂)
            ≡⟨ cong (λ x → x + ((a₁ + b₂) * c₂)) (+*-rDist a₂ b₁ c₁) ⟩
                ((a₂ * c₁) + (b₁ * c₁)) + ((a₁ + b₂) * c₂)
            ≡⟨ cong (λ x → ((a₂ * c₁) + (b₁ * c₁)) + x) (+*-rDist a₁ b₂ c₂) ⟩
                ((a₂ * c₁) + (b₁ * c₁)) + ((a₁ * c₂) + (b₂ * c₂))
            ≡⟨ sym (+-assoc (a₂ * c₁) (b₁ * c₁) ((a₁ * c₂) + (b₂ * c₂))) ⟩
                (a₂ * c₁) + ((b₁ * c₁) + ((a₁ * c₂) + (b₂ * c₂)))
            ≡⟨ cong (λ x → (a₂ * c₁) + x) (+-assoc (b₁ * c₁) (a₁ * c₂) (b₂ * c₂)) ⟩
                (a₂ * c₁) + (((b₁ * c₁) + (a₁ * c₂)) + (b₂ * c₂))
            ≡⟨ cong (λ x → (a₂ * c₁) + x) (cong (λ x → x + (b₂ * c₂)) (+-comm (b₁ * c₁) (a₁ * c₂))) ⟩
                (a₂ * c₁) + (((a₁ * c₂) + (b₁ * c₁)) + (b₂ * c₂))
            ≡⟨ cong (λ x → (a₂ * c₁) + x) (sym (+-assoc (a₁ * c₂) (b₁ * c₁) (b₂ * c₂))) ⟩
                (a₂ * c₁) + ((a₁ * c₂) + ((b₁ * c₁) + (b₂ * c₂)))
            ≡⟨ +-assoc (a₂ * c₁) (a₁ * c₂) ((b₁ * c₁) + (b₂ * c₂)) ⟩
                ((a₂ * c₁) + (a₁ * c₂)) + ((b₁ * c₁) + (b₂ * c₂))
            ≡⟨ cong (λ x → x + ((b₁ * c₁) + (b₂ * c₂))) (+-comm (a₂ * c₁) (a₁ * c₂)) ⟩
                ((a₁ * c₂) + (a₂ * c₁)) + ((b₁ * c₁) + (b₂ * c₂))
            ∎

-- c *ℤ a = (c₁ * a₁) + (c₂ * a₂) , (c₁ * a₂) + (c₂ * a₁)
-- c *ℤ b = (c₁ * b₁) + (c₂ * b₂) , (c₁ * b₂) + (c₂ * b₁)
*ℤ-rUniv : (a b c : ℤb) → a ≡ℤ b → (c *ℤ a) ≡ℤ (c *ℤ b)
*ℤ-rUniv (a₁ , a₂) (b₁ , b₂) (c₁ , c₂) a₁+b₂≡a₂+b₁ = begin
        ((c₁ * a₁) + (c₂ * a₂)) + ((c₁ * b₂) + (c₂ * b₁))
    ≡⟨ +-assoc ((c₁ * a₁) + (c₂ * a₂)) (c₁ * b₂) (c₂ * b₁) ⟩
        (((c₁ * a₁) + (c₂ * a₂)) + (c₁ * b₂)) + (c₂ * b₁)
    ≡⟨ cong (λ x → x + (c₂ * b₁)) (sym (+-assoc (c₁ * a₁) (c₂ * a₂) (c₁ * b₂))) ⟩
        ((c₁ * a₁) + ((c₂ * a₂) + (c₁ * b₂))) + (c₂ * b₁)
    ≡⟨ cong (λ z → ((c₁ * a₁) + z) + (c₂ * b₁)) (+-comm (c₂ * a₂) (c₁ * b₂)) ⟩
        ((c₁ * a₁) + ((c₁ * b₂) + (c₂ * a₂))) + (c₂ * b₁)
    ≡⟨ cong (λ z → z + (c₂ * b₁)) (+-assoc (c₁ * a₁) (c₁ * b₂) (c₂ * a₂)) ⟩
        (((c₁ * a₁) + (c₁ * b₂)) + (c₂ * a₂)) + (c₂ * b₁)
    ≡⟨ sym (+-assoc ((c₁ * a₁) + (c₁ * b₂)) (c₂ * a₂) (c₂ * b₁)) ⟩
        ((c₁ * a₁) + (c₁ * b₂)) + ((c₂ * a₂) + (c₂ * b₁))
    ≡⟨ cong (λ z → z + ((c₂ * a₂) + (c₂ * b₁))) (sym (+*-lDist a₁ b₂ c₁)) ⟩
        (c₁ * (a₁ + b₂)) + ((c₂ * a₂) + (c₂ * b₁))
    ≡⟨ cong (λ z → (c₁ * (a₁ + b₂)) + z) (sym (+*-lDist a₂ b₁ c₂)) ⟩
        (c₁ * (a₁ + b₂)) + (c₂ * (a₂ + b₁))
    ≡⟨ cong (λ z → (c₁ * z) + (c₂ * (a₂ + b₁))) a₁+b₂≡a₂+b₁ ⟩
        (c₁ * (a₂ + b₁)) + (c₂ * (a₂ + b₁))
    ≡⟨ cong (λ z → (c₁ * (a₂ + b₁)) + (c₂ * z)) (sym a₁+b₂≡a₂+b₁) ⟩
        (c₁ * (a₂ + b₁)) + (c₂ * (a₁ + b₂))
    ≡⟨ cong (λ z → z + (c₂ * (a₁ + b₂))) (+*-lDist a₂ b₁ c₁) ⟩
        ((c₁ * a₂) + (c₁ * b₁)) + (c₂ * (a₁ + b₂))
    ≡⟨ cong (λ z → ((c₁ * a₂) + (c₁ * b₁)) + z) (+*-lDist a₁ b₂ c₂) ⟩
        ((c₁ * a₂) + (c₁ * b₁)) + ((c₂ * a₁) + (c₂ * b₂))
    ≡⟨ sym (+-assoc (c₁ * a₂) (c₁ * b₁) ((c₂ * a₁) + (c₂ * b₂))) ⟩
        (c₁ * a₂) + ((c₁ * b₁) + ((c₂ * a₁) + (c₂ * b₂)))
    ≡⟨ cong (λ z → (c₁ * a₂) + z) (+-assoc (c₁ * b₁) (c₂ * a₁) (c₂ * b₂)) ⟩
        (c₁ * a₂) + (((c₁ * b₁) + (c₂ * a₁)) + (c₂ * b₂))
    ≡⟨ cong (λ z → (c₁ * a₂) + (z + (c₂ * b₂))) (+-comm (c₁ * b₁) (c₂ * a₁)) ⟩
        (c₁ * a₂) + (((c₂ * a₁) + (c₁ * b₁)) + (c₂ * b₂))
    ≡⟨ cong (λ z → (c₁ * a₂) + z) (sym (+-assoc (c₂ * a₁) (c₁ * b₁) (c₂ * b₂))) ⟩
        (c₁ * a₂) + ((c₂ * a₁) + ((c₁ * b₁) + (c₂ * b₂)))
    ≡⟨ +-assoc (c₁ * a₂) (c₂ * a₁) ((c₁ * b₁) + (c₂ * b₂)) ⟩
        ((c₁ * a₂) + (c₂ * a₁)) + ((c₁ * b₁) + (c₂ * b₂))
    ∎

+ℤ-rUnit : (a b : ℕ) → ((a , b) +ℤ (zero , zero)) ≡ (a , b)
+ℤ-rUnit a b = begin
        (a , b) +ℤ (zero , zero)
    ≡⟨ refl ⟩
        (a + zero , b + zero)
    ≡⟨ cong (λ x → x , (b + zero)) (+-rUnit a) ⟩
        (a , b + zero)
    ≡⟨ cong (λ x → a , x) (+-rUnit b) ⟩
        (a , b)
    ∎

+ℤ-lUnit : (a b : ℕ) → ((zero , zero) +ℤ (a , b)) ≡ (a , b)
+ℤ-lUnit a b = begin
        (zero , zero) +ℤ (a , b)
    ≡⟨ refl ⟩
        (zero + a , zero + b)
    ≡⟨ refl ⟩
        (a , b)
    ∎

-- (a , b) *ℤ (succ zero , zero) = (a * succ zero + b * zero , a * zero + b * succ zero)
-- a + (a * zero + b * succ zero) = b + (a * succ zero + b * zero)
*ℤ-rUnit : (a b : ℕ) → ((a , b) *ℤ (succ zero , zero)) ≡ (a , b)
*ℤ-rUnit a b = begin
        ((a * succ zero) + (b * zero) , ((a * zero) + (b * succ zero)))
    ≡⟨ cong (λ x → x , ((a * zero) + (b * succ zero))) lem1 ⟩
        (a , ((a * zero) + (b * succ zero)))
    ≡⟨ cong (λ x → a , x) lem2 ⟩
        (a , b)
    ∎
    where
        lem1 : (a * succ zero) + (b * zero) ≡ a
        lem1 = begin
                (a * succ zero) + (b * zero)
            ≡⟨ cong (λ x → x + (b * zero)) (*-rUnit a) ⟩
                a + (b * zero)
            ≡⟨ cong (λ x → a + x) (*-rAbsorp b) ⟩
                a + zero
            ≡⟨ +-rUnit a ⟩
                a
            ∎
        lem2 : (a * zero) + (b * succ zero) ≡ b
        lem2 = begin
                (a * zero) + (b * succ zero)
            ≡⟨ cong (λ x → (a * zero) + x) (*-rUnit b) ⟩
                (a * zero) + b
            ≡⟨ cong (λ x → x + b) (*-rAbsorp a) ⟩
                zero + b
            ≡⟨ refl ⟩
                b
            ∎

-- ((succ zero * a) + (zero * b) , (succ zero * b) + (zero * a))
*ℤ-lUnit : (a b : ℕ) → ((succ zero , zero) *ℤ (a , b)) ≡ (a , b)
*ℤ-lUnit a b = begin
        ((succ zero * a) + (zero * b) , (succ zero * b) + (zero * a))
    ≡⟨ cong (λ x → x , ((succ zero * b) + (zero * a))) lem1 ⟩
        (a , (succ zero * b) + (zero * a))
    ≡⟨ cong (λ x → a , x) lem2 ⟩
        (a , b)
    ∎
    where
        lem1 : (succ zero * a) + (zero * b) ≡ a
        lem1 = begin
                (succ zero * a) + (zero * b)
            ≡⟨ cong (λ x → x + (zero * b)) (*-lUnit a) ⟩
                a + (zero * b)
            ≡⟨ cong (λ x → a + x) refl ⟩
                a + zero
            ≡⟨ +-rUnit a ⟩
                a
            ∎
        lem2 : (succ zero * b) + (zero * a) ≡ b
        lem2 = begin
                (succ zero * b) + (zero * a)
            ≡⟨ cong (λ x → x + (zero * a)) (*-lUnit b) ⟩
                b + (zero * a)
            ≡⟨ cong (λ x → b + x) refl ⟩
                b + zero
            ≡⟨ +-rUnit b ⟩
                b
            ∎

-- (b +ℤ c) = (b₁ + c₁) , (b₂ + c₂)
-- a +ℤ (b +ℤ c) = a₁ + (b₁ + c₁) , a₂ + (b₂ + c₂)
-- (a +ℤ b) = a₁ + b₁ , a₂ + b₂
-- (a +ℤ b) + c = (a₁ + b₁) + c₁ , (a₂ + b₂) + c₂
-- (a₁ + (b₁ + c₁)) + ((a₂ + b₂) + c₂) ≡ (a₂ + (b₂ + c₂)) + ((a₁ + b₁) + c₁)
+ℤ-assoc : (a b c : ℤb) → (a +ℤ (b +ℤ c)) ≡ℤ ((a +ℤ b) +ℤ c)
+ℤ-assoc (a₁ , a₂) (b₁ , b₂) (c₁ , c₂) = begin
        (a₁ + (b₁ + c₁)) + ((a₂ + b₂) + c₂)
    ≡⟨ +-comm (a₁ + (b₁ + c₁)) ((a₂ + b₂) + c₂) ⟩
        ((a₂ + b₂) + c₂) + (a₁ + (b₁ + c₁))
    ≡⟨ cong (λ x → x + (a₁ + (b₁ + c₁))) (sym (+-assoc a₂ b₂ c₂)) ⟩
        (a₂ + (b₂ + c₂)) + (a₁ + (b₁ + c₁))
    ≡⟨ cong (λ x → (a₂ + (b₂ + c₂)) + x) (+-assoc a₁ b₁ c₁) ⟩
        (a₂ + (b₂ + c₂)) + ((a₁ + b₁) + c₁)
    ∎

-- a +ℤ b = a + c , b + d
-- b +ℤ a = c + a , d + b
-- (a + c) + (d + b) = (b + d) + (c + a)
+ℤ-comm : (a b : ℤb) → (a +ℤ b) ≡ℤ (b +ℤ a)
+ℤ-comm (a , b) (c , d) = begin
        (a + c) + (d + b)
    ≡⟨ +-comm (a + c) (d + b) ⟩
        (d + b) + (a + c)
    ≡⟨ cong (λ x → x + (a + c)) (+-comm d b) ⟩
        (b + d) + (a + c)
    ≡⟨ cong (λ x → (b + d) + x) (+-comm a c) ⟩
        (b + d) + (c + a)
    ∎

-- b *ℤ c = (b₁ * c₁) + (b₂ * c₂) , (b₁ * c₂) + (b₂ * c₁)
-- a *ℤ (b *ℤ c) = (a₁ * ((b₁ * c₁) + (b₂ * c₂))) + (a₂ * ((b₁ * c₂) + (b₂ * c₁)))
--               , (a₁ * ((b₁ * c₂) + (b₂ * c₁))) + (a₂ * ((b₁ * c₁) + (b₂ * c₂)))
-- a *ℤ b = (a₁ * b₁) + (a₂ * b₂) , (a₁ * b₂) + (a₂ * b₁)
-- (a *ℤ b) *ℤ c = (((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) + (a₂ * b₁)) * c₂)
--               , (((a₁ * b₂) + (a₂ * b₁)) * c₁) + (((a₁ * b₁) + (a₂ * b₂)) * c₂)
-- (a₁ * ((b₁ * c₁) + (b₂ * c₂))) + (a₂ * ((b₁ * c₂) + (b₂ * c₁)))
-- + (((a₁ * b₂) + (a₂ * b₁)) * c₁) + (((a₁ * b₁) + (a₂ * b₂)) * c₂)
-- ≡
-- (a₁ * ((b₁ * c₂) + (b₂ * c₁))) + (a₂ * ((b₁ * c₁) + (b₂ * c₂)))
-- + (((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) + (a₂ * b₁)) * c₂)
*ℤ-assoc : (a b c : ℤb) → (a *ℤ (b *ℤ c)) ≡ℤ ((a *ℤ b) *ℤ c)
*ℤ-assoc a@(a₁ , a₂) b@(b₁ , b₂) c@(c₁ , c₂) = ≡ℤ-≡ (begin
        a *ℤ (b *ℤ c)
    ≡⟨ cong (λ x → a *ℤ x) refl ⟩
        a *ℤ ((b₁ * c₁) + (b₂ * c₂) , (b₁ * c₂) + (b₂ * c₁))
    ≡⟨ refl ⟩
        ((a₁ * ((b₁ * c₁) + (b₂ * c₂))) + (a₂ * ((b₁ * c₂) + (b₂ * c₁))) ,
            ((a₁ * ((b₁ * c₂) + (b₂ * c₁))) + (a₂ * ((b₁ * c₁) + (b₂ * c₂)))))
    ≡⟨ cong (λ z → z , (((a₁ * ((b₁ * c₂) + (b₂ * c₁))) + (a₂ * ((b₁ * c₁) + (b₂ * c₂)))))) lem1 ⟩
        ((((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) + (a₂ * b₁)) * c₂)) ,
            ((a₁ * ((b₁ * c₂) + (b₂ * c₁))) + (a₂ * ((b₁ * c₁) + (b₂ * c₂))))
    ≡⟨ cong (λ z → (((((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) + (a₂ * b₁)) * c₂))) , z) lem2 ⟩
        ((((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) + (a₂ * b₁)) * c₂)) ,
         ((((a₁ * b₁) + (a₂ * b₂)) * c₂) + (((a₁ * b₂) + (a₂ * b₁)) * c₁))
    ≡⟨ refl ⟩
        ((a₁ * b₁) + (a₂ * b₂) , (a₁ * b₂) + (a₂ * b₁)) *ℤ c
    ≡⟨ cong (λ z → z *ℤ c) t-lem ⟩
        (a *ℤ b) *ℤ c
    ∎)
    where
        t-lem : ((a₁ * b₁) + (a₂ * b₂) , (a₁ * b₂) + (a₂ * b₁)) ≡ (a *ℤ b)
        t-lem = refl
        lem1 : ((a₁ * ((b₁ * c₁) + (b₂ * c₂))) + (a₂ * ((b₁ * c₂) + (b₂ * c₁)))) ≡
                ((((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) + (a₂ * b₁)) * c₂))
        lem1 = begin
                ((a₁ * ((b₁ * c₁) + (b₂ * c₂))) + (a₂ * ((b₁ * c₂) + (b₂ * c₁))))
            ≡⟨ cong (λ z → z + (a₂ * ((b₁ * c₂) + (b₂ * c₁)))) (+*-lDist (b₁ * c₁) (b₂ * c₂) a₁) ⟩
                ((a₁ * (b₁ * c₁)) + (a₁ * (b₂ * c₂))) + (a₂ * ((b₁ * c₂) + (b₂ * c₁)))
            ≡⟨ cong (λ z → (((a₁ * (b₁ * c₁)) + (a₁ * (b₂ * c₂)))) + z) (+*-lDist (b₁ * c₂) (b₂ * c₁) a₂) ⟩
                ((a₁ * (b₁ * c₁)) + (a₁ * (b₂ * c₂))) + ((a₂ * (b₁ * c₂)) + (a₂ * (b₂ * c₁)))
            ≡⟨ cong (λ z → (((a₁ * (b₁ * c₁)) + (a₁ * (b₂ * c₂)))) + z) (+-comm (a₂ * (b₁ * c₂)) (a₂ * (b₂ * c₁))) ⟩
                ((a₁ * (b₁ * c₁)) + (a₁ * (b₂ * c₂))) + ((a₂ * (b₂ * c₁)) + (a₂ * (b₁ * c₂)))
            ≡⟨ sym (+-assoc (a₁ * (b₁ * c₁)) (a₁ * (b₂ * c₂)) ((a₂ * (b₂ * c₁)) + (a₂ * (b₁ * c₂)))) ⟩
                (a₁ * (b₁ * c₁)) + ((a₁ * (b₂ * c₂)) + (((a₂ * (b₂ * c₁)) + (a₂ * (b₁ * c₂)))))
            ≡⟨ cong (λ z → (a₁ * (b₁ * c₁)) + z) (+-assoc (a₁ * (b₂ * c₂)) (a₂ * (b₂ * c₁)) (a₂ * (b₁ * c₂))) ⟩
                (a₁ * (b₁ * c₁)) + (((a₁ * (b₂ * c₂)) + (a₂ * (b₂ * c₁))) + (a₂ * (b₁ * c₂)))
            ≡⟨ cong (λ z → (a₁ * (b₁ * c₁)) + (z + (a₂ * (b₁ * c₂)))) (+-comm (a₁ * (b₂ * c₂)) (a₂ * (b₂ * c₁))) ⟩
                (a₁ * (b₁ * c₁)) + (((a₂ * (b₂ * c₁)) + (a₁ * (b₂ * c₂))) + (a₂ * (b₁ * c₂)))
            ≡⟨ cong (λ z → (a₁ * (b₁ * c₁)) + z) (sym (+-assoc (a₂ * (b₂ * c₁)) (a₁ * (b₂ * c₂)) (a₂ * (b₁ * c₂)))) ⟩
                (a₁ * (b₁ * c₁)) + ((a₂ * (b₂ * c₁)) + ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂))))
            ≡⟨ +-assoc (a₁ * (b₁ * c₁)) (a₂ * (b₂ * c₁)) ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂))) ⟩
                ((a₁ * (b₁ * c₁)) + (a₂ * (b₂ * c₁))) + ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂)))
            ≡⟨ cong (λ z → (z + (a₂ * (b₂ * c₁))) + ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂)))) (*-assoc a₁ b₁ c₁) ⟩
                (((a₁ * b₁) * c₁) + (a₂ * (b₂ * c₁))) + ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂)))
            ≡⟨ cong (λ z → (((a₁ * b₁) * c₁) + z) + ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂)))) (*-assoc a₂ b₂ c₁) ⟩
                (((a₁ * b₁) * c₁) + ((a₂ * b₂) * c₁)) + ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂)))
            ≡⟨ cong (λ z → z + ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂)))) (sym (+*-rDist (a₁ * b₁) (a₂ * b₂) c₁)) ⟩
                (((a₁ * b₁) + (a₂ * b₂)) * c₁) + ((a₁ * (b₂ * c₂)) + (a₂ * (b₁ * c₂)))
            ≡⟨ cong (λ z → ((((a₁ * b₁) + (a₂ * b₂)) * c₁)) + (z + (a₂ * (b₁ * c₂)))) (*-assoc a₁ b₂ c₂) ⟩
                (((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) * c₂) + (a₂ * (b₁ * c₂)))
            ≡⟨ cong (λ z → (((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) * c₂) + z)) (*-assoc a₂ b₁ c₂) ⟩
                (((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) * c₂) + ((a₂ * b₁) * c₂))
            ≡⟨ cong (λ z → ((((a₁ * b₁) + (a₂ * b₂)) * c₁)) + z) (sym (+*-rDist (a₁ * b₂) (a₂ * b₁) c₂)) ⟩
                (((a₁ * b₁) + (a₂ * b₂)) * c₁) + (((a₁ * b₂) + (a₂ * b₁)) * c₂)
            ∎
        lem2 : ((a₁ * ((b₁ * c₂) + (b₂ * c₁))) + (a₂ * ((b₁ * c₁) + (b₂ * c₂)))) ≡
                ((((a₁ * b₁) + (a₂ * b₂)) * c₂) + (((a₁ * b₂) + (a₂ * b₁)) * c₁))
        lem2 = begin
                (a₁ * ((b₁ * c₂) + (b₂ * c₁))) + (a₂ * ((b₁ * c₁) + (b₂ * c₂)))
            ≡⟨ cong (λ x → x + (a₂ * ((b₁ * c₁) + (b₂ * c₂)))) (+*-lDist (b₁ * c₂) (b₂ * c₁) a₁) ⟩
                ((a₁ * (b₁ * c₂)) + (a₁ * (b₂ * c₁))) + (a₂ * ((b₁ * c₁) + (b₂ * c₂)))
            ≡⟨ cong (λ x → (((a₁ * (b₁ * c₂)) + (a₁ * (b₂ * c₁)))) + x) (+*-lDist (b₁ * c₁) (b₂ * c₂) a₂) ⟩
                ((a₁ * (b₁ * c₂)) + (a₁ * (b₂ * c₁))) + ((a₂ * (b₁ * c₁)) + (a₂ * (b₂ * c₂)))
            ≡⟨ cong (λ x → (x + ((a₁ * (b₂ * c₁)))) + (((a₂ * (b₁ * c₁)) + (a₂ * (b₂ * c₂))))) (*-assoc a₁ b₁ c₂) ⟩
                (((a₁ * b₁) * c₂) + (a₁ * (b₂ * c₁))) + ((a₂ * (b₁ * c₁)) + (a₂ * (b₂ * c₂)))
            ≡⟨ cong (λ x → ((((a₁ * b₁) * c₂)) + x) + (((a₂ * (b₁ * c₁)) + (a₂ * (b₂ * c₂))))) (*-assoc a₁ b₂ c₁) ⟩
                (((a₁ * b₁) * c₂) + ((a₁ * b₂) * c₁)) + ((a₂ * (b₁ * c₁)) + (a₂ * (b₂ * c₂)))
            ≡⟨ cong (λ x → ((((a₁ * b₁) * c₂) + ((a₁ * b₂) * c₁))) + (x + (a₂ * (b₂ * c₂)))) (*-assoc a₂ b₁ c₁) ⟩
                (((a₁ * b₁) * c₂) + ((a₁ * b₂) * c₁)) + (((a₂ * b₁) * c₁) + (a₂ * (b₂ * c₂)))
            ≡⟨ cong (λ x → ((((a₁ * b₁) * c₂) + ((a₁ * b₂) * c₁))) + (((a₂ * b₁) * c₁) + x)) (*-assoc a₂ b₂ c₂) ⟩
                (((a₁ * b₁) * c₂) + ((a₁ * b₂) * c₁)) + (((a₂ * b₁) * c₁) + ((a₂ * b₂) * c₂))
            ≡⟨ sym (+-assoc ((a₁ * b₁) * c₂) ((a₁ * b₂) * c₁) (((a₂ * b₁) * c₁) + ((a₂ * b₂) * c₂))) ⟩
                ((a₁ * b₁) * c₂) + (((a₁ * b₂) * c₁) + (((a₂ * b₁) * c₁) + ((a₂ * b₂) * c₂)))
            ≡⟨ cong (λ x → (((a₁ * b₁) * c₂)) + x) (+-assoc ((a₁ * b₂) * c₁) ((a₂ * b₁) * c₁) ((a₂ * b₂) * c₂)) ⟩
                ((a₁ * b₁) * c₂) + ((((a₁ * b₂) * c₁) + ((a₂ * b₁) * c₁)) + ((a₂ * b₂) * c₂))
            ≡⟨ cong (λ x → (((a₁ * b₁) * c₂)) + x) (+-comm (((a₁ * b₂) * c₁) + ((a₂ * b₁) * c₁)) ((a₂ * b₂) * c₂)) ⟩
                ((a₁ * b₁) * c₂) + (((a₂ * b₂) * c₂) + (((a₁ * b₂) * c₁) + ((a₂ * b₁) * c₁)))
            ≡⟨ +-assoc ((a₁ * b₁) * c₂) ((a₂ * b₂) * c₂) (((a₁ * b₂) * c₁) + ((a₂ * b₁) * c₁)) ⟩
                (((a₁ * b₁) * c₂) + ((a₂ * b₂) * c₂)) + (((a₁ * b₂) * c₁) + ((a₂ * b₁) * c₁))
            ≡⟨ cong (λ x → x + (((a₁ * b₂) * c₁) + ((a₂ * b₁) * c₁))) (sym (+*-rDist (a₁ * b₁) (a₂ * b₂) c₂)) ⟩
                (((a₁ * b₁) + (a₂ * b₂)) * c₂) + (((a₁ * b₂) * c₁) + ((a₂ * b₁) * c₁))
            ≡⟨ cong (λ x → ((((a₁ * b₁) + (a₂ * b₂)) * c₂)) + x) (sym (+*-rDist (a₁ * b₂) (a₂ * b₁) c₁)) ⟩
                (((a₁ * b₁) + (a₂ * b₂)) * c₂) + (((a₁ * b₂) + (a₂ * b₁)) * c₁)
            ∎

-- a *ℤ b = a₁ * b₁ + a₂ * b₂ , a₁ * b₂ + a₂ * b₁
-- b *ℤ a = b₁ * a₁ + b₂ * a₂ , b₁ * a₂ + b₂ * a₁
*ℤ-comm : (a b : ℤb) → (a *ℤ b) ≡ℤ (b *ℤ a)
*ℤ-comm (a₁ , a₂) (b₁ , b₂) = begin
        ((a₁ * b₁) + (a₂ * b₂)) + ((b₁ * a₂) + (b₂ * a₁))
    ≡⟨ +-comm ((a₁ * b₁) + (a₂ * b₂)) ((b₁ * a₂) + (b₂ * a₁)) ⟩
        ((b₁ * a₂) + (b₂ * a₁)) + ((a₁ * b₁) + (a₂ * b₂))
    ≡⟨ cong (λ z → z + ((a₁ * b₁) + (a₂ * b₂))) (+-comm (b₁ * a₂) (b₂ * a₁)) ⟩
        ((b₂ * a₁) + (b₁ * a₂)) + ((a₁ * b₁) + (a₂ * b₂))
    ≡⟨ cong (λ z → (z + (b₁ * a₂)) + ((a₁ * b₁) + (a₂ * b₂))) (*-comm b₂ a₁) ⟩
        ((a₁ * b₂) + (b₁ * a₂)) + ((a₁ * b₁) + (a₂ * b₂))
    ≡⟨ cong (λ z → ((a₁ * b₂) + z) + ((a₁ * b₁) + (a₂ * b₂))) (*-comm b₁ a₂) ⟩
        ((a₁ * b₂) + (a₂ * b₁)) + ((a₁ * b₁) + (a₂ * b₂))
    ≡⟨ cong (λ z → ((a₁ * b₂) + (a₂ * b₁)) + (z + (a₂ * b₂))) (*-comm a₁ b₁) ⟩
        ((a₁ * b₂) + (a₂ * b₁)) + ((b₁ * a₁) + (a₂ * b₂))
    ≡⟨ cong (λ z → ((a₁ * b₂) + (a₂ * b₁)) + ((b₁ * a₁) + z)) (*-comm a₂ b₂) ⟩
        ((a₁ * b₂) + (a₂ * b₁)) + ((b₁ * a₁) + (b₂ * a₂))
    ∎

ℕ-ℤ : ℕ → ℤb
ℕ-ℤ n = (n , zero)

ℕ-ℤ-monic : (m n : ℕ) → ℕ-ℤ m ≡ℤ ℕ-ℤ n → m ≡ n
ℕ-ℤ-monic m n m+0≡0+n = begin
        m
    ≡⟨ sym (+-rUnit m) ⟩
        m + zero
    ≡⟨ m+0≡0+n ⟩
        zero + n
    ≡⟨ refl ⟩
        n
    ∎

-- (n , zero) +ℤ (zero , n) = n + zero , zero + n
-- (n + zero) + zero = (zero + n) + zero
+ℤ-invℕ : (n : ℕ) → ((n , zero) +ℤ (zero , n)) ≡ℤ (zero , zero)
+ℤ-invℕ n = begin
        (n + zero) + zero
    ≡⟨ cong (λ x → x + zero) (+-comm n zero) ⟩
        (zero + n) + zero
    ∎

-- (a , b) +ℤ (b , a) = a + b , b + a
-- (a + b) + zero = (b + a) + zero
+ℤ-inv : (a : ℤb) → ∃ λ b → (a +ℤ b) ≡ℤ (zero , zero)
+ℤ-inv (a , b) = (b , a) , (begin
        (a + b) + zero
    ≡⟨ cong (λ x → x + zero) (+-comm a b) ⟩
        (b + a) + zero
    ∎)

-ℤ_ : ℤb → ℤb
-ℤ (a , b) = (b , a)

_-ℤ_ : ℤb → ℤb → ℤb
a -ℤ b = a +ℤ (-ℤ b)

-ℤ-inv : (a : ℤb) → (a -ℤ a) ≡ℤ (zero , zero)
-ℤ-inv (a , b) = begin
        (a + b) + zero
    ≡⟨ cong (λ x → x + zero) (+-comm a b) ⟩
        (b + a) + zero
    ∎

_≤ℤ_ : ℤb → ℤb → Set
a ≤ℤ b = ∃ λ l → (a +ℤ (l , zero)) ≡ℤ b

≤ℤ-refl : (a : ℤb) → a ≤ℤ a
≤ℤ-refl (a , b) = zero , ≡ℤ-≡ (+ℤ-rUnit a b)

-- p : (a₁ , a₂) +ℤ (x , zero) ≡ℤ (b₁ , b₂)
-- (a₁ + x , a₂ + zero) ≡ℤ (b₁ , b₂)
-- (a₁ + x) + b₂ = (a₂ + zero) + b₁
-- q : (b₁ , b₂) +ℤ (x , zero) ≡ℤ (c₁ , c₂)
-- (b₁ + y , b₂ + zero) ≡ℤ (c₁ , c₂)
-- (b₁ + y) + c₂ = (b₂ + zero) + c₁
-- goal : (a₁ , a₂) +ℤ (z , zero) ≡ℤ (c₁ , c₂)
-- (a₁ + z , a₂ + zero) ≡ℤ (c₁ , c₂)
-- (a₁ + z) + c₂ ≡ (a₂ + zero) + c₁
≤ℤ-trans : (a b c : ℤb) → a ≤ℤ b → b ≤ℤ c → a ≤ℤ c
≤ℤ-trans (a₁ , a₂) (b₁ , b₂) (c₁ , c₂) (x , p) (y , q) = (x + y) ,
    +-rCancel ((a₁ + (x + y)) + c₂) ((a₂ + zero) + c₁) b₂ (begin
            ((a₁ + (x + y)) + c₂) + b₂
        ≡⟨ cong (λ z → z + b₂) (sym (+-assoc a₁ (x + y) c₂)) ⟩
            (a₁ + ((x + y) + c₂)) + b₂
        ≡⟨ sym (+-assoc a₁ ((x + y) + c₂) b₂) ⟩
            a₁ + (((x + y) + c₂) + b₂)
        ≡⟨ cong (λ z → a₁ + z) (sym (+-assoc (x + y) c₂ b₂)) ⟩
            a₁ + ((x + y) + (c₂ + b₂))
        ≡⟨ cong (λ z → a₁ + ((x + y) + z)) (+-comm c₂ b₂) ⟩
            a₁ + ((x + y) + (b₂ + c₂))
        ≡⟨ cong (λ z → a₁ + z) (sym (+-assoc x y (b₂ + c₂))) ⟩
            a₁ + (x + (y + (b₂ + c₂)))
        ≡⟨ cong (λ z → a₁ + (x + z)) (+-assoc y b₂ c₂) ⟩
            a₁ + (x + ((y + b₂) + c₂))
        ≡⟨ cong (λ z → a₁ + (x + (z + c₂))) (+-comm y b₂) ⟩
            a₁ + (x + ((b₂ + y) + c₂))
        ≡⟨ cong (λ z → a₁ + (x + z)) (sym (+-assoc b₂ y c₂)) ⟩
            a₁ + (x + (b₂ + (y + c₂)))
        ≡⟨ +-assoc a₁ x (b₂ + (y + c₂)) ⟩
            ((a₁ + x) + (b₂ + (y + c₂)))
        ≡⟨ +-assoc (a₁ + x) b₂ (y + c₂) ⟩
            ((a₁ + x) + b₂) + (y + c₂)
        ≡⟨ cong (λ z → z + (y + c₂)) p ⟩
            ((a₂ + zero) + b₁) + (y + c₂)
        ≡⟨ sym (+-assoc (a₂ + zero) b₁ (y + c₂)) ⟩
            (a₂ + zero) + (b₁ + (y + c₂))
        ≡⟨ cong (λ z → (a₂ + zero) + z) (+-assoc b₁ y c₂) ⟩
            (a₂ + zero) + ((b₁ + y) + c₂)
        ≡⟨ cong (λ z → (a₂ + zero) + z) q ⟩
            (a₂ + zero) + ((b₂ + zero) + c₁)
        ≡⟨ cong (λ z → (a₂ + zero) + z) (+-comm (b₂ + zero) c₁) ⟩
            (a₂ + zero) + (c₁ + (b₂ + zero))
        ≡⟨ cong (λ z → (a₂ + zero) + (c₁ + z)) (+-rUnit b₂) ⟩
            (a₂ + zero) + (c₁ + b₂)
        ≡⟨ +-assoc (a₂ + zero) c₁ b₂ ⟩
            ((a₂ + zero) + c₁) + b₂
        ∎)

-- p : (a₁ + x , a₂ + zero) ≡ℤ (b₁ , b₂)
-- (a₁ + x) + b₂ ≡ (a₂ + zero) + b₁
-- q : (b₁ + y , b₂ + zero) ≡ℤ (a₁ , a₂)
-- (b₁ + y) + a₂ ≡ (b₂ + zero) + a₁
≤ℤ-antisym : (a b : ℤb) → a ≤ℤ b → b ≤ℤ a → a ≡ℤ b
≤ℤ-antisym (a₁ , a₂) (b₁ , b₂) (x , p) (y , q) = begin
        a₁ + b₂
    ≡⟨ sym (+-rUnit (a₁ + b₂)) ⟩
        (a₁ + b₂) + zero
    ≡⟨ cong (λ z → (a₁ + b₂) + z) (sym x≡0) ⟩
        (a₁ + b₂) + x
    ≡⟨ sym (+-assoc a₁ b₂ x) ⟩
        a₁ + (b₂ + x)
    ≡⟨ cong (λ z → a₁ + z) (+-comm b₂ x) ⟩
        a₁ + (x + b₂)
    ≡⟨ +-assoc a₁ x b₂ ⟩
        (a₁ + x) + b₂
    ≡⟨ p ⟩
        (a₂ + zero) + b₁
    ≡⟨ cong (λ z → z + b₁) (+-rUnit a₂) ⟩
        a₂ + b₁
    ∎
    where
        x≡0 : x ≡ zero
        x≡0 = +-lZero x y (+-lCancel (x + y) zero ((a₁ + b₂) + a₂) (begin
                ((a₁ + b₂) + a₂) + (x + y)
            ≡⟨ sym (+-assoc (a₁ + b₂) a₂ (x + y)) ⟩
                (a₁ + b₂) + (a₂ + (x + y))
            ≡⟨ cong (λ x₁ → (a₁ + b₂) + x₁) (+-assoc a₂ x y) ⟩
                (a₁ + b₂) + ((a₂ + x) + y)
            ≡⟨ cong (λ z → (a₁ + b₂) + (z + y)) (+-comm a₂ x) ⟩
                (a₁ + b₂) + ((x + a₂) + y)
            ≡⟨ cong (λ z → (a₁ + b₂) + z) (sym (+-assoc x a₂ y)) ⟩
                (a₁ + b₂) + (x + (a₂ + y))
            ≡⟨ +-assoc (a₁ + b₂) x (a₂ + y) ⟩
                ((a₁ + b₂) + x) + (a₂ + y)
            ≡⟨ cong (λ z → z + (a₂ + y)) (sym (+-assoc a₁ b₂ x)) ⟩
                (a₁ + (b₂ + x)) + (a₂ + y)
            ≡⟨ cong (λ z → (a₁ + z) + (a₂ + y)) (+-comm b₂ x) ⟩
                (a₁ + (x + b₂)) + (a₂ + y)
            ≡⟨ cong (λ z → z + (a₂ + y)) (+-assoc a₁ x b₂) ⟩
                ((a₁ + x) + b₂) + (a₂ + y)
            ≡⟨ cong (λ z → z + (a₂ + y)) p ⟩
                ((a₂ + zero) + b₁) + (a₂ + y)
            ≡⟨ sym (+-assoc (a₂ + zero) b₁ (a₂ + y)) ⟩
                (a₂ + zero) + (b₁ + (a₂ + y))
            ≡⟨ cong (λ z → (a₂ + zero) + (b₁ + z)) (+-comm a₂ y) ⟩
                (a₂ + zero) + (b₁ + (y + a₂))
            ≡⟨ cong (λ z → (a₂ + zero) + z) (+-assoc b₁ y a₂) ⟩
                (a₂ + zero) + ((b₁ + y) + a₂)
            ≡⟨ cong (λ z → (a₂ + zero) + z) q ⟩
                (a₂ + zero) + ((b₂ + zero) + a₁)
            ≡⟨ +-comm (a₂ + zero) ((b₂ + zero) + a₁) ⟩
                ((b₂ + zero) + a₁) + (a₂ + zero)
            ≡⟨ cong (λ z → z + (a₂ + zero)) (+-comm (b₂ + zero) a₁) ⟩
                (a₁ + (b₂ + zero)) + (a₂ + zero)
            ≡⟨ cong (λ z → (a₁ + z) + (a₂ + zero)) (+-rUnit b₂) ⟩
                (a₁ + b₂) + (a₂ + zero)
            ≡⟨ +-assoc (a₁ + b₂) a₂ zero ⟩
                ((a₁ + b₂) + a₂) + zero
            ∎))

-- (a₁ , a₂) ≤ℤ (b₁ , b₂)
-- (a₁ + l , a₂ + zero) ≡ℤ (b₁ , b₂)
-- (a₁ + l) + b₂ ≡ (a₂ + zero) + b₁
≤ℤ-all : (a b : ℤb) → a ≤ℤ b ⊎ b ≤ℤ a
≤ℤ-all a@(a₁ , a₂) b@(b₁ , b₂) = S.map lem1 lem2 (≤-all (a₁ + b₂) (a₂ + b₁))
    where
        lem1 : (a₁ + b₂) ≤ (a₂ + b₁) → a ≤ℤ b
        lem1 (x , p) = x , (begin
                (a₁ + x) + b₂
            ≡⟨ sym (+-assoc a₁ x b₂) ⟩
                a₁ + (x + b₂)
            ≡⟨ cong (λ z → a₁ + z) (+-comm x b₂) ⟩
                a₁ + (b₂ + x)
            ≡⟨ +-assoc a₁ b₂ x ⟩
                (a₁ + b₂) + x
            ≡⟨ p ⟩
                a₂ + b₁
            ≡⟨ cong (λ z → z + b₁) (sym (+-rUnit a₂)) ⟩
                (a₂ + zero) + b₁
            ∎)
        lem2 : (a₂ + b₁) ≤ (a₁ + b₂) → b ≤ℤ a
        lem2 (x , p) = x , (begin
                (b₁ + x) + a₂
            ≡⟨ sym (+-assoc b₁ x a₂) ⟩
                b₁ + (x + a₂)
            ≡⟨ cong (λ z → b₁ + z) (+-comm x a₂) ⟩
                b₁ + (a₂ + x)
            ≡⟨ +-assoc b₁ a₂ x ⟩
                (b₁ + a₂) + x
            ≡⟨ cong (λ z → z + x) (+-comm b₁ a₂) ⟩
                (a₂ + b₁) + x
            ≡⟨ p ⟩
                a₁ + b₂
            ≡⟨ +-comm a₁ b₂ ⟩
                b₂ + a₁
            ≡⟨ cong (λ z → z + a₁) (sym (+-rUnit b₂)) ⟩
                (b₂ + zero) + a₁
            ∎)

max_stars_repo_name: karrym/NatToReal

max_issues_repo_name: karrym/NatToReal

max_forks_repo_name: karrym/NatToReal


text:
module Issue215 where

open import Imports.Bool

{-# COMPILE GHC Bool = data Bool (True | False) #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Example of lambda-lifting
------------------------------------------------------------------------------

{-# OPTIONS --exact-split                    #-}
{-# OPTIONS --no-universe-polymorphism       #-}
{-# OPTIONS --universal-quantified-functions #-}
{-# OPTIONS --without-K                      #-}

module LambdaLifting where

infixl 9 _·_
infix  8 if_then_else_
infix  7 _≡_

infixl 10 _*_
infixl 9  _+_

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

postulate
  D                : Set
  zero true false  : D
  succ iszero pred : D → D
  _·_              : D → D → D
  if_then_else_    : D → D → D → D
  lam fix          : (D → D) → D

data _≡_ (x : D) : D → Set where
  refl : x ≡ x

-- Conversion rules

-- Conversion rules for Booleans.
postulate
  if-true  : ∀ d₁ {d₂} → if true then d₁ else d₂  ≡ d₁
  if-false : ∀ {d₁} d₂ → if false then d₁ else d₂ ≡ d₂
{-# ATP axioms if-true if-false #-}

-- Conversion rules for pred.
postulate
  -- N.B. We don't need this equation.
  -- pred-0 :       pred zero     ≡ zero
  pred-S : ∀ d → pred (succ d) ≡ d
{-# ATP axiom pred-S #-}

-- Conversion rules for iszero.
postulate
  iszero-0 :       iszero zero     ≡ true
  iszero-S : ∀ d → iszero (succ d) ≡ false
{-# ATP axioms iszero-0 iszero-S #-}

-- Conversion rule for the λ-abstraction and the application.
postulate beta : ∀ f a → lam f · a ≡ f a
{-# ATP axiom beta #-}

-- Conversion rule for the fixed-pointed operator.
postulate fix-eq : ∀ f → fix f ≡ f (fix  f)
{-# ATP axiom fix-eq #-}

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

postulate
  _*_  : D → D → D
  *-0x : ∀ d → zero * d ≡ zero
  *-Sx : ∀ d e → succ d * e ≡ e + d * e
{-# ATP axioms *-0x *-Sx #-}

------------------------------------------------------------------------------
-- The original fach
-- fach : D → D
-- fach f = lam (λ n → if (iszero n) then (succ zero) else n * (f · (pred n)))

-- Lambda-lifting via super-combinators (Hughes. Super-combinators. 1982).

α : D → D → D
α f n = if (iszero n) then (succ zero) else n * (f · (pred n))
{-# ATP definition α #-}

fach : D → D
fach f = lam (α f)
{-# ATP definition fach #-}

fac : D → D
fac n = fix fach · n
{-# ATP definition fac #-}

postulate fac0 : fac zero ≡ succ zero
{-# ATP prove fac0 #-}

postulate fac1 : fac (succ zero) ≡ succ zero
{-# ATP prove fac1 #-}

postulate fac2 : fac (succ (succ zero)) ≡ succ (succ zero)
{-# ATP prove fac2 #-}

------------------------------------------------------------------------------
-- Ouput:
--
-- $ apia -inotes --non-fol-function notes/LambdaLifting.agda
-- Proving the conjecture in /tmp/LambdaLifting/95-fac1.tptp ...
-- E 1.6 Tiger Hill proved the conjecture in /tmp/LambdaLifting/95-fac1.tptp
-- Proving the conjecture in /tmp/LambdaLifting/99-fac2.tptp ...
-- E 1.6 Tiger Hill proved the conjecture in /tmp/LambdaLifting/99-fac2.tptp
-- Proving the conjecture in /tmp/LambdaLifting/91-fac0.tptp ...
-- Vampire 0.6 (revision 903) proved the conjecture in /tmp/LambdaLifting/91-fac0.tptp

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

module Ch2 where

-- open import lib.Base
open import Base

module Ex2-1 where
  {-
  Lemma 2.1.2. For every type A and every x, y, z : A there is a function
  (x = y) → (y = z) → (x = z)
  written p → q → p ∙ q, such that reflx ∙ reflx ≡ reflx for any x : A.

  We call p ∙ q the concatenation or composite of p and q.
  -}

  {-
  Exercise 2.1 Show that the three obvious proofs of Lemma 2.1.2 are pairwise equal.
  -}

  -- (proof(s) of 2.1.2 are the inhabitants of the type corresponding to the
  -- statement of the lemma)

  {- The versions of concat below WITHOUT the primes 's are proved using Agda's
  'internal J rule', whatever that might be.

  (And there is no --without-J option to turn it off!)

  In the HoTT-Agda lib, there is a
  comment that:

  concat1' and concat3' are proved using ind== which is the closest I could get
  to free path induction (as in the book), but unfortunately this didn't work out
  for concat2' which had to use left-based path induction, ie ind=' (J in the
  HoTT-Agda libs)
  -}

  concat1 : ∀ {i} {A : Type i} {x y z : A} → x == y → y == z → x == z
  concat1 idp q = q

  concat1' : ∀ {i} {A : Type i} {x y z : A} → x == y → y == z → x == z
  concat1' {i} {A} {_} {_} {z} = ind== D d where
    D : (x y : A) → (p : x == y) → Type i
    D x y _ = y == z → x == z

    d : (x₁ : A) → D x₁ x₁ idp
    d _ = λ q → q

  concat2 : ∀ {i} {A : Type i} {x y z : A} → x == y → y == z → x == z
  concat2 p idp = p

  -- uses based path induction, because I couldn't get free path induction to work
  -- at first
  concat2' : ∀ {i} {A : Type i} {x y z : A} → x == y → y == z → x == z
  concat2' {i} {A} {x} {y} {_} p = ind=' D d where
    D : (z : A) → y == z → Type i
    D z _ = x == z

    d : D _ idp
    d = p

  -- here is the free path induction version which relies upon a 'twist' of
  -- the paths p and q in order to 'line up the end points' of the idp base
  -- case of q (Dustin Mulcahey of HoTT-NYC group noticed this trick)
  concat2'' : ∀ {i} {A : Type i} {x y z : A} → x == y → y == z → x == z
  concat2'' {i} {A} {x} {_} {_} p q = ind== D d q p where
    D : (y z : A) → (q : y == z) → Type i
    D y z _ = x == y → x == z

    d : (y : A) → D y y idp
    d _ = λ p → p

  concat3 : ∀ {i} {A : Type i} {x y z : A} → x == y → y == z → x == z
  concat3 idp idp = idp

  concat3' : ∀ {i} {A : Type i} {x y z : A} → x == y → y == z → x == z
  concat3' {i} {A} {_} {_} {z} = ind== D d where
    D : (x y : A) → (p : x == y) → Type i
    D x y _ = y == z → x == z

    d : (x₁ : A) → D x₁ x₁ idp
    d _ = ind== E e where
      E : (y z : A) (q : y == z) → Type i
      E y z _ = y == z

      e : (x : A) → E x x idp
      e _ = idp

  concat1=concat2 : ∀ {i} {A : Type i} {x y z : A}
    (p : x == y) (q : y == z) → concat1 p q == concat2 p q
  concat1=concat2 idp idp = idp

  concat1'=concat2' : ∀ {i} {A : Type i} {x y z : A}
    (p : x == y) (q : y == z) → concat1' p q == concat2' p q
  concat1'=concat2' {i} {A} {_} {_} {z} = ind== D d where
    D : (x y : A) → x == y → Type i
    D _ y p = (q : y == z) → concat1' p q == concat2' p q

    d : (x : A) → D x x idp
    d _ = ind== E e where
      E : (y₁ z₁ : A) → y₁ == z₁ → Type i
      E _ _ q = concat1' idp q == concat2' idp q

      e : (x₁ : A) → E x₁ x₁ idp
      e _ = idp -- : concat1' idp idp == concat2' idp idp   ⇓'p'
                -- > (ind== D1 d1) idp idp == (ind== D2 d2) idp idp
                -- > (d1 q) idp == (d2 x) idp
                -- > (λ q → q) idp == 'p' (aka idp)
                -- > idp == idp -- (this being the type of the inhabitant value idp of e x)

  concat2=concat3 : ∀ {i} {A : Type i} {x y z : A}
    (p : x == y) (q : y == z) → concat2 p q == concat3 p q
  concat2=concat3 idp idp = idp

  concat2'=concat3' : ∀ {i} {A : Type i} {x y z : A}
    (p : x == y) (q : y == z) → concat2' p q == concat3' p q
  concat2'=concat3' {i} {A} {x} {y} {z} = ind== D d where
    D : (x y : A) → x == y → Type i
    D _ y p = (q : y == z) → concat2' p q == concat3' p q

    d : (x : A) → D x x idp
    d x = ind== E e where
      E : (y₁ z₁ : A) → y₁ == z₁ → Type i
      E _ _ q = concat2' idp q == concat3' idp q

      e : (x₁ : A) → E x₁ x₁ idp
      e _ = idp -- : concat2' idp idp == concat3' idp idp

  concat1=concat3 : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z) → concat1 p q == concat3 p q
  concat1=concat3 idp idp = idp

  concat1'=concat3' : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z) → concat1' p q == concat3' p q
  concat1'=concat3' {i} {A} {_} {_} {z} = ind== D d where
    D : (x y : A) → x == y → Type i
    D x y p = (q : y == z) → concat1' p q == concat3' p q

    d : (x : A) → D x x idp
    d _ = ind== E e where
      E : (y z : A) → (q : y == z) → Type i
      E _ _ q = concat1' idp q == concat3' idp q

      e : (y : A) → E y y idp
      e _ = idp -- : concat1' idp idp == concat3' idp idp

module Ex2-2 where

  open Ex2-1

  {-
  Show that the three equalities of proofs constructed in the previous exercise form a
  commutative triangle. In other words, if the three definitions of concatenation are denoted
  by (p 􏰂1 q), (p 􏰂2 q), and (p 􏰂3 q), then the concatenated equality
  (p 􏰂1 q) = (p 􏰂2 q) = (p 􏰂3 q)
  is equal to the equality
  (p 􏰂1 q) = (p 􏰂3 q).
  -}

  -- Choice of which 'concat' we use for the statement of the proof type; we use the book one
  concat = concat3

  concat-commutative-triangle : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z) →
    concat (concat1=concat2 p q) (concat2=concat3 p q) == concat1=concat3 p q
  concat-commutative-triangle idp idp = idp

  -- likewise, the ind== version of the book concat operator
  concat' = concat3'

  concat-commutative-triangle' : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z) →
    concat' (concat1'=concat2' p q) (concat2'=concat3' p q) == concat1'=concat3' p q
  concat-commutative-triangle' {i} {A} {_} {_} {z} = ind== D d where
    D : (x y : A) → x == y → Type i
    D _ y p = (q : y == z) →
      concat' (concat1'=concat2' p q) (concat2'=concat3' p q) == concat1'=concat3' p q

    d : (x : A) → D x x idp
    d _ = ind== E e where
      E : (y z : A) → (q : y == z) → Type i
      E _ _ q =
        concat' (concat1'=concat2' idp q) (concat2'=concat3' idp q) == concat1'=concat3' idp q

      e : (y : A) → E y y idp
      e _ = idp -- : concat' (concat1'=concat2' idp idp) (concat2'=concat3' idp idp) == concat1'=concat3' idp idp

module Ex2-3 where

  -- use another of the based path inductions

module Ex2-4 where

{- Define, by induction on n, a general notion of n-dimensional path in a type A,
simultaneously with the type of boundaries for such paths. -}

max_stars_repo_name: aerskine/hott-ex

max_issues_repo_name: aerskine/hott-ex

max_forks_repo_name: aerskine/hott-ex


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

module Algebra.Construct.Free.Semilattice.Relation.Unary.All.Dec where

open import Prelude hiding (⊥; ⊤)
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Definition
open import Cubical.Foundations.HLevels
open import Data.Empty.UniversePolymorphic
open import HITs.PropositionalTruncation.Sugar
open import HITs.PropositionalTruncation.Properties
open import HITs.PropositionalTruncation
open import Data.Unit.UniversePolymorphic
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Def
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Decidable.Properties
open import Relation.Nullary.Decidable.Logic

private
  variable p : Level

◻′? : ∀ {P : A → Type p} → (∀ x → Dec (P x)) → xs ∈𝒦 A ⇒∥ Dec (◻ P xs) ∥
∥ ◻′? {P = P} P? ∥-prop {xs} = isPropDec (isProp-◻ {P = P} {xs = xs})
∥ ◻′? P? ∥[] = yes tt
∥ ◻′? P? ∥ x ∷ xs ⟨ Pxs ⟩ = map-dec ∣_∣ refute-trunc (P? x) && Pxs

◻? : ∀ {P : A → Type p} → (∀ x → Dec (P x)) → ∀ xs → Dec (◻ P xs)
◻? P? = ∥ ◻′? P? ∥⇓

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path

-- Works:

data Truncate (A : Set) : Set where
  [_] : A → Truncate A
  sq  : ∀{x y} (p q : PathP (λ _  → Truncate A) x y)
         → PathP (λ _ → PathP (λ _ → Truncate A) x y) p q

data Truncat (A : Set) : Set where
  [_] : A → Truncat A
  sq  : ∀{x y : Truncat A} (p q : x ≡ y) → p ≡ q

-- Fails:

data Trunc (A : Set) : Set where
  [_] : A → Trunc A
  sq  : ∀{x y} (p q : PathP (λ _  → Trunc A) x y)
         → PathP _ p q

-- The failure is expected, but it shouldn't give a non-obligated
-- equality constraint as the reason for the failure.


text:
{-

This file contains:

- Definition of groupoid truncations

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.GroupoidTruncation.Base where

open import Cubical.Core.Primitives

-- groupoid truncation as a higher inductive type:

data ∥_∥₃ {ℓ} (A : Type ℓ) : Type ℓ where
  ∣_∣₃ : A → ∥ A ∥₃
  squash₃ : ∀ (x y : ∥ A ∥₃) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Congruity
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transitivity
open import Oscar.Data.Proposequality
import Oscar.Class.Congruity.Proposequality

module Oscar.Class.Transextensionality.Proposequality where

instance

  𝓣ransextensionalityProposequality : ∀
    {a} {A : Ø a}
    {m} {_⊸_ : A → A → Ø m}
    ⦃ _ : Transitivity.class _⊸_ ⦄
    → Transextensionality.class _⊸_ Proposequality transitivity
  𝓣ransextensionalityProposequality .⋆ = congruity₂ _


text:
------------------------------------------------------------------------------
-- Note on the equality type class using instance arguments
------------------------------------------------------------------------------

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

-- Adapted from: On the Bright Side of Type Classes: Instances
-- Arguments in Agda (ICFP'11).

module FOT.FOTC.TypeClasses.EqualityInstanceArguments where

open import FOTC.Base
open import FOTC.Data.Bool
open import FOTC.Data.Bool.Type
open import FOTC.Data.Nat.Type

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

∃-proj₁ : ∀ {A} → ∃ A → D
∃-proj₁ (x , _) = x

record Eq (P : D → Set) : Set₁ where
  field equal : ∀ {t₁ t₂} → P t₁ → P t₂ → Set

equal : {P : D → Set}{t₁ t₂ : D} → {{eqT : Eq P}} → P t₁ → P t₂ → Set
equal {{eqT}} = Eq.equal eqT

boolEq : ∀ {b₁ b₂} → Bool b₁ → Bool b₂ → Set
boolEq btrue  btrue  = Bool true
boolEq bfalse bfalse = Bool true
{-# CATCHALL #-}
boolEq _      _      = Bool false

nEq : ∀ {m n} → N m → N n → Set
nEq nzero      nzero      = Bool true
nEq (nsucc Nm) (nsucc Nn) = Bool true
{-# CATCHALL #-}
nEq _          _          = Bool false

instance
  eqInstanceBool : Eq Bool
  eqInstanceBool = record { equal = boolEq }

  eqInstanceN : Eq N
  eqInstanceN = record { equal = nEq }

test₁ : Set
test₁ = equal nzero (nsucc nzero)

test₂ : Set
test₂ = equal bfalse bfalse

eqN-sym : ∀ {m n} → (Nm : N m) → (Nn : N n) → equal Nm Nn → equal Nn Nm
eqN-sym nzero      nzero      h = h
eqN-sym nzero      (nsucc Nn) h = h
eqN-sym (nsucc Nm) nzero      h = h
eqN-sym (nsucc Nm) (nsucc Nn) h = h

postulate eqN-sym' : ∀ {m n} → (Nm : N m) → (Nn : N n) → equal Nm Nn → equal Nn Nm
-- {-# ATP prove eqN-sym' #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Limits.Terminal where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
-- open import Cubical.Categories.Limits.Base
open import Cubical.Categories.Category
open import Cubical.Categories.Functor

private
  variable
    ℓ ℓ' : Level

module _ (C : Precategory ℓ ℓ') where
  open Precategory C

  isInitial : (x : ob) → Type (ℓ-max ℓ ℓ')
  isInitial x = ∀ (y : ob) → isContr (C [ x , y ])

  isFinal : (x : ob) → Type (ℓ-max ℓ ℓ')
  isFinal x = ∀ (y : ob) → isContr (C [ y , x ])

  hasFinalOb : Type (ℓ-max ℓ ℓ')
  hasFinalOb = Σ[ x ∈ ob ] isFinal x


text:
module MLib.Semirings where

open import MLib.Prelude
open Algebra using (Semiring)

module _ {ℓ p} (semiring : Semiring ℓ p) where
  open Semiring semiring renaming (Carrier to S)

  pow : ℕ → S → S
  pow Nat.zero x = 1#
  pow (Nat.suc n) x = x * pow n x

  powsum : ℕ → S → S
  powsum Nat.zero x = 1#
  powsum (Nat.suc n) x = pow (Nat.suc n) x + powsum n x

  Q-stable : ℕ → S → Set p
  Q-stable q x = powsum (1 Nat.+ q) x ≈ powsum q x


text:
-- Andreas, 2016-12-30, issue #2368 reported by m0davis

-- {-# OPTIONS -v interaction.give:100 -v tc.constr:30 #-}

open import Agda.Builtin.Reflection

macro
  mac : Term → Term → TC _
  mac = {!!}

foo : Set → Set → Set
foo = mac (foo {!Term!} {!Term!})  -- give both solutions

-- WAS: internal error after giving the second `Term`

-- Expected: yellow

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 Pi-reasoning where

open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Bool hiding (_≟_)
open import Data.Nat
open import Data.List
open import Data.Sum hiding (map)
open import Data.Product hiding (map)
open import Level hiding (suc)
open import Relation.Nullary
open import Relation.Binary
open import Algebra
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Binary.PropositionalEquality as PropEq using(sym; trans)
import Algebra.FunctionProperties as FunctionProperties
-- open import Algebra.FunctionProperties
open import Algebra.Structures

open import Pi-abstract-machine

------------------------------------------------------------------------------
-- Decidable equality

-- normalize a type to a natural number

size : B → ℕ
size ZERO = 0
size ONE = 1
size (PLUS b₁ b₂) = size b₁ + size b₂
size (TIMES b₁ b₂) = size b₁ * size b₂

-- normalize a value to a number

normalize : {b : B} → VB b → ℕ
normalize {ZERO} ()
normalize {ONE} unitB = 0
normalize {PLUS b₁ b₂} (inlB v) = normalize {b₁} v
normalize {PLUS b₁ b₂} (inrB v) = size b₁ + normalize {b₂} v
normalize {TIMES b₁ b₂} (pairB v₁ v₂) = size b₂ * normalize {b₁} v₁ + normalize {b₂} v₂

-- decidable equality of our values: normalize and compare the
-- underlying natural numbers. This is justified by the fact that the
-- natural numbers are a model of commutative semirings.
-- Note that we can't compare at different types so easily, they have
-- to have the same size, something not worth dealing with right now
vb= : {b : B} → (v₁ : VB b) → (v₂ : VB b) → Set
vb= {b} v₁ v₂ = (normalize {b} v₁) ≡ (normalize {b} v₂)

vb-Equivalence : {b : B} → IsEquivalence (vb= {b})
vb-Equivalence = record
  { refl = refl
  ; sym = PropEq.sym
  ; trans = PropEq.trans }

vb== : {b : B} → Decidable {A = VB b} vb=
vb== {b} x y = (normalize {b} x) ≟ (normalize {b} y)

-- generate all values of a type

values : (b : B) → List (VB b)
values ZERO = []
values ONE = [ unitB ]
values (PLUS b₁ b₂) = map inlB (values b₁) ++ map inrB (values b₂)
values (TIMES b₁ b₂) = concatMap (λ v₁ → map (pairB v₁) (values b₂)) (values b₁)

-- B is a Setoid

VB-is-Setoid : {b : B} → Setoid Level.zero Level.zero
VB-is-Setoid {b} = record
  { Carrier = VB b
  ; _≈_ = vb=
  ; isEquivalence = vb-Equivalence
  }

-- equality of combinators:
-- two combinators are equal if they map equal values to equal values
-- best do this via proving that vb= generates a decidable equivalence
{-
⟺=bool : {b₁ b₂ : B} → (b₁ ⟺ b₂) → (b₁ ⟺ b₂) → Bool
⟺=bool {b₁} {b₂} f g =
  and (zipWith vb= (map (eval f) vs) (map (eval g) vs))
  where vs = values b₁

data _⟺=_ : {b₁ b₂ : B} → (b₁ ⟺ b₂) → (b₁ ⟺ b₂) → Set where
  id⟺= : {b₁ b₂ : B} → (f : b₁ ⟺ b₂) → (f ⟺= f)
  sym⟺= : {b₁ b₂ : B} → (f : b₁ ⟺ b₂) → (g : b₁ ⟺ b₂) → ( f ⟺= g ) → (g ⟺= f)

-- verifies that the given combinators relates the given values

data _s⟷_ : B → B → Set where
  sid⟷ : {b : B} {v₁ : VB b} {v₂ : VB b} {p : T (vb= (eval (iso id⟷) v₁) v₂)} → (b s⟷ b)

⟺=IsEquivalence : IsEquivalence _s⟷_
⟺=IsEquivalence = record {
    refl = srefl ;
    sym = {!!} ;
    trans = {!!}
  }
  where srefl : {b : B} {v : VB b} → b s⟷ b
        srefl {b} {v} = sid⟷ {b} {v} {v} {{!!}}

-- <-> : B -> B -> Set with constructors id : {b : B} -> (b <-> b)
-- IsEquivalence <->
--   refl = id

-- R= : B -> B -> Set with constructos
-}

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

{--
testT = PLUS ONE (PLUS ONE ONE)
test1 = normalize {testT} (inlB unitB)
test2 = normalize {testT} (inrB (inlB unitB))
test3 = normalize {testT} (inrB (inrB unitB))

testT = PLUS ZERO (PLUS ONE ONE)
test1 = normalize {testT} (inrB (inlB unitB))
test2 = normalize {testT} (inrB (inrB unitB))

testT = TIMES (PLUS ONE ONE) ZERO
test1 = size testT

testT = TIMES (PLUS ONE ONE) (PLUS ONE (PLUS ONE ONE))
test1 = normalize {testT} (pairB (inlB unitB) (inlB unitB))
test2 = normalize {testT} (pairB (inrB unitB) (inlB unitB))
test3 = normalize {testT} (pairB (inlB unitB) (inrB (inlB unitB)))
test4 = normalize {testT} (pairB (inrB unitB) (inrB (inlB unitB)))
test5 = normalize {testT} (pairB (inlB unitB) (inrB (inrB unitB)))
test6 = normalize {testT} (pairB (inrB unitB) (inrB (inrB unitB)))

BOOL = PLUS ONE ONE
test = ⟺= {BOOL} {BOOL} (iso swap₊ ◎ iso swap₊) (iso id⟷)

test1 : (iso swap₊) ⟺= (iso swap₊)
test1 = check
          {PLUS ONE ONE} {PLUS ONE ONE}
          (iso swap₊) (iso swap₊)
          tt

The following does NOT typecheck which is good. Agda rejected my
nonsense claim that id is equivalent to swap+

test2 : (iso swap₊) ⟺= (iso id⟷)
test2 = check
          {PLUS ONE ONE} {PLUS ONE ONE}
          (iso swap₊) (iso id⟷)
          tt

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-----------------------------------------------------------------------
-- This file formalizes the proof that Dial₂(Sets) is indeed a model --
-- of Full Tensorial Logic.  See Lemma 16 and Lemma 17 of the paper. --
-----------------------------------------------------------------------
module Tensorial where

open import prelude
open import Dial2Sets

-- We first must prove that Dial₂(Sets) is a dialogue category.  The
-- defining feature is that we use primarily implication for this.

-- This defines the negation functor: ¬ : Dial₂(Sets) → Dial₂ᵒᵖ(Sets)
¬ₒ : Obj → Obj
¬ₒ A = A ⊸ₒ J

¬ₐ-aux : ∀{U V Y X : Set}{f : U → V}{F : Y → X}
  → Σ (V → ⊤) (λ x → ⊤ → Y)
  → Σ (U → ⊤) (λ x → ⊤ → X)
¬ₐ-aux {f = f}{F}(j₁ , j₂) = (λ u → j₁ (f u)) , (λ t → F (j₂ t))

¬ₐ-aux' : ∀{U V : Set}{f : U → V}
  → Σ U (λ x → ⊤)
  → Σ V (λ x → ⊤)
¬ₐ-aux' {f = f} (u , triv) = f u , triv

¬ₐ : {A B : Obj} → Hom A B → Hom (¬ₒ B) (¬ₒ A)
¬ₐ {(U , X , α)}{(V , Y , β)} (f , F , p) = ¬ₐ-aux , ¬ₐ-aux' , ¬ₐ-cond
 where
   ¬ₐ-cond : {u : Σ (V → ⊤) (λ x → ⊤ → Y)} {y : Σ U (λ x → ⊤)}
     → ⊸-cond β (λ x y₁ → ⊥) u (¬ₐ-aux' y)
     → ⊸-cond α (λ x y₁ → ⊥) (¬ₐ-aux {f = f}{F} u) y
   ¬ₐ-cond {j₁ , j₂}{u , triv} p₁ p₂ = p₁ (p p₂)

-- At this point we must show that the required family of bijections
-- exist.
--
-- The bijection φ turns out to be a simple use of the combination of
-- currying and associativity:
--
--   Hom(A ⊗ B,¬ C) = Hom(A ⊗ B,C ⊸ ⊥)
--                  ≅ Hom((A ⊗ B) ⊗ C, ⊥)
--                  ≅ Hom(A ⊗ (B ⊗ C), ⊥)
--                  ≅ Hom(A, (B ⊗ C) ⊸ ⊥)
--                  = Hom(A, ¬ (B ⊗ C))
--
-- Note that the previous string of isomorphisms do not depend on the
-- fact that ⊥ is the intial object.  In fact, we can replace ⊥ with
-- any object at all, and the result still holds.

φ : {A B C : Obj}
  → Hom (A ⊗ₒ B) (¬ₒ C)
  → Hom A (¬ₒ (B ⊗ₒ C))
φ {A}{B}{C} f = cur ((α⊗-inv {A}{B}{C}) ○ (uncur f))

φ-inv : {A B C : Obj}
  → Hom A (¬ₒ (B ⊗ₒ C))
  → Hom (A ⊗ₒ B) (¬ₒ C)
φ-inv {A}{B}{C} g = cur ((α⊗ {A}{B}{C}) ○ (uncur g))

φ-bij₁ : ∀{A B C : Obj}{f : Hom (A ⊗ₒ B) (¬ₒ C)}
  → φ-inv (φ f) ≡h f
φ-bij₁ {A}{B}{C}{f} with
    (cur-uncur-bij₁ {A}{B ⊗ₒ C}{J}{comp (α⊗-inv {A}{B}{C}) (uncur {A ⊗ₒ B}{C}{J} f)})
... | eq₁ with
    cur-≡h (≡h-subst-○ {(A ⊗ₒ B) ⊗ₒ C}{A ⊗ₒ (B ⊗ₒ C)}{J}{α⊗}{α⊗}
      {j = uncur f} (≡h-refl {(A ⊗ₒ B) ⊗ₒ C}{A ⊗ₒ (B ⊗ₒ C)} {f = α⊗}) eq₁
      (≡h-trans (○-assoc {f = α⊗ {A} {B} {C}} {α⊗-inv} {uncur f})
      (≡h-subst-○ {f₁ = α⊗ {A} {B} {C} ○ α⊗-inv} {id} {uncur f} {uncur f}
      {uncur f} α⊗-id₁ ≡h-refl ○-idl)))
... | eq₂ = ≡h-trans eq₂ cur-uncur-bij₂

φ-bij₂ : ∀{A B C : Obj}{f : Hom A (¬ₒ (B ⊗ₒ C))}
  → φ (φ-inv f) ≡h f
φ-bij₂ {A}{B}{C}{f} with
  cur-uncur-bij₁ {f = comp (α⊗ {A}{B}{C}) (uncur f)}
... | eq₁ with
  cur-cong (≡h-subst-○ {f₁ = α⊗-inv {A}{B}{C}}{α⊗-inv {A}{B}{C}}
                       {j = comp α⊗-inv (comp α⊗ (uncur f))} ≡h-refl eq₁ ≡h-refl)
... | eq₂ with
  (cur-cong (○-assoc {f = α⊗-inv {A} {B} {C}} {α⊗} {uncur f}))
... | eq₃ with
  cur-cong (≡h-subst-○ {f₁ = comp (α⊗-inv {A}{B}{C}) α⊗}{id}
                       {uncur f}{uncur f}{comp id (uncur f)} α⊗-id₂ ≡h-refl ≡h-refl)
... | eq₄ = ≡h-trans eq₂ (≡h-trans eq₃ (≡h-trans eq₄ (≡h-trans
                     (cur-cong (○-idl {f = uncur f})) (cur-uncur-bij₂ {g = f}))))

-- The following shows that Dial₂(Sets)! is cartesian.

Jₒ = !ₒ

-- First, we define the cartesian product in Dial₂(Sets), and then use
-- Jₒ to put us inside of Dial₂(Sets)!.
_&ᵣ_ : {U X V Y : Set}
  → (α : U → X → Set)
  → (β : V → Y → Set)
  → Σ U (λ x → V)
  → X ⊎ Y
  → Set
_&ᵣ_ α β (u , v) (inj₁ x) = α u x
_&ᵣ_ α β (u , v) (inj₂ y) = β v y

_&ₒ_ : (A B : Obj) → Obj
(U , X , α) &ₒ (V , Y , β) = (U × V) , (X ⊎ Y) , α &ᵣ β

-- The remainder of this file will work under the Jₒ functor which
-- will put us inside of Dial₂(Sets)!.

-- This defines the projection morphism: π₁ : F(A & B) → F(A).
π₁ : {A B : Obj} → Hom (Jₒ (A &ₒ B)) (Jₒ A)
π₁ {U , X , α}{V , Y , β} =
  fst ,
  (λ (f : U → (X *)) (p : U × V) → map inj₁ (f (fst p))) ,
  λ {u}{y} p → π₁-cond {u}{y} p
 where
  π₁-cond : {u : Σ U (λ x → V)} {y : U → 𝕃 X} →
      all-pred ((α &ᵣ β) u) (map inj₁ (y (fst u))) →
      all-pred (α (fst u)) (y (fst u))
  π₁-cond {u , v} y = aux y
   where
     aux : {l : X *}
       → all-pred ((α &ᵣ β) (u , v)) (map inj₁ l) → all-pred (α u) l
     aux {[]} triv = triv
     aux {x :: l} (j₁ , j₂) = j₁ , aux j₂

-- This defines the projection morphism: π₂ : A & B → B.
π₂ : {A B : Obj} → Hom (Jₒ (A &ₒ B)) (Jₒ B)
π₂ {U , X , α}{V , Y , β} =
  snd , (λ f p → map inj₂ (f (snd p))) , λ {u}{y} p → π₂-cond {u}{y} p
 where
  π₂-cond : {u : Σ U (λ x → V)} {y : V → 𝕃 Y} →
      all-pred ((α &ᵣ β) u) (map inj₂ (y (snd u))) →
      all-pred (β (snd u)) (y (snd u))
  π₂-cond {u , v} y = aux y
   where
     aux : {l : Y *}
       → all-pred ((α &ᵣ β) (u , v)) (map inj₂ l) → all-pred (β v) l
     aux {[]} triv = triv
     aux {x :: l} (j₁ , j₂) = j₁ , aux j₂

cart-ar-crt : {U X V Y W Z : Set}
  → {α : U → X → Set}
  → {β : V → Y → Set}
  → {γ : W → Z → Set}
  → Hom (Jₒ (W , Z , γ)) (Jₒ (U , X , α))
  → Hom (Jₒ (W , Z , γ)) (Jₒ (V , Y , β))
  → (Σ U (λ x → V) → 𝕃 (X ⊎ Y)) → W → 𝕃 Z
cart-ar-crt  (f , F , p₁) (g , G , p₂) j w
  with (λ u → (proj-⊎₁ (j (u , g w)))) | (λ v → (proj-⊎₂ (j (f w , v))))
... | j₁ | j₂ = F j₁ w ++ G j₂ w

-- This takes two morphisms f : C → A and g : C → B, and constructs
-- a morphism (f,g) : C → A & B.
cart-ar : {C A B : Obj}
  → Hom (Jₒ C) (Jₒ A)
  → Hom (Jₒ C) (Jₒ B)
  → Hom (Jₒ C) (Jₒ (A &ₒ B))
cart-ar {W , Z , γ}{U , X , α}{V , Y , β} (f , F , p₁) (g , G , p₂)
  = (λ w → (f w , g w)) ,
    cart-ar-crt {α = α}{β}{γ} (f , F , p₁) (g , G , p₂) ,
    (λ {u}{y} p → cart-ar-cond {u}{y} p)
  where
    cart-ar-cond : {u : W} {y : Σ U (λ x → V) → 𝕃 (X ⊎ Y)} →
      all-pred (γ u)
      (F (λ u₁ → proj-⊎₁ (y (u₁ , g u))) u ++
       G (λ v → proj-⊎₂ (y (f u , v))) u) →
      all-pred ((α &ᵣ β) (f u , g u)) (y (f u , g u))
    cart-ar-cond {u}{j} p
      rewrite
        all-pred-append
          {f = γ u}
          {F (λ u₁ → (proj-⊎₁ (j (u₁ , g u)))) u}
          {G (λ v → (proj-⊎₂ (j (f u , v)))) u}
          ∧-unit ∧-assoc
     with p
    ... | (r₁ , r₂) = aux (p₁ r₁) (p₂ r₂)
     where
       aux : ∀{l}
         → all-pred (α (f u)) ((proj-⊎₁ l))
         → all-pred (β (g u)) ((proj-⊎₂ l))
         → all-pred ((α &ᵣ β) (f u , g u)) l
       aux {[]} _ _ = triv
       aux {inj₁ x :: l} (s₁ , s₂) x₂ = s₁ , aux {l} s₂ x₂
       aux {inj₂ y :: l} x₁ (s₁ , s₂) = s₁ , aux {l} x₁ s₂

-- This shows that f ≡ (f,g);π₁.
cart-diag₁ : {A B C : Obj}
  → {f : Hom C A}
  → {g : Hom C B}
  → _≡h_ { Jₒ C}{ Jₒ A}
    (!ₐ {C}{A} f)
    (comp { Jₒ C}
          {(Jₒ (A &ₒ B))}
          { Jₒ A}
          (cart-ar
            (!ₐ {C}{A} f) (!ₐ {C}{B} g))
          π₁)
cart-diag₁ {U , X , α}{V , Y , β}{W , Z , γ}{f = f , F , p₁}{g , G , p₂}
  = refl , ext-set (λ {j₁} → ext-set (λ {w} → aux))
  where
    aux : ∀{l : X *} →
      map F l ≡
      map F (proj-⊎₁ {_}{_}{X}{Y} (map inj₁ l)) ++
      map G (proj-⊎₂ (map inj₁ l))
    aux {l} rewrite
      map-proj-⊎₁ {_}{_}{X}{Y} l |
      map-proj-⊎₂-[] {_}{_}{X}{Y} l = sym (++[] (map F l))

-- This shows that g ≡ (f,g);π₂.
cart-diag₂ : {A B C : Obj}
  → {f : Hom C A}
  → {g : Hom C B}
  → _≡h_ { Jₒ C}{ Jₒ B}
    (!ₐ {C}{B} g)
    (comp { Jₒ C}
          {(Jₒ (A &ₒ B))}
          { Jₒ B}
          (cart-ar
            (!ₐ {C}{A} f) (!ₐ {C}{B} g))
          π₂)
cart-diag₂ {U , X , α}{V , Y , β}{W , Z , γ}{f = f , F , p₁}{g , G , p₂}
  = refl , ext-set (λ {j₁} → ext-set (λ {w} → aux))
  where
    aux : ∀{l : Y *} →
      map G l ≡
      map F (proj-⊎₁ {_}{_}{X}{Y} (map inj₂ l)) ++
      map G (proj-⊎₂ {_}{_}{X}{Y} (map inj₂ l))
    aux {l} rewrite map-proj-⊎₂ {_}{_}{X}{Y} l |
                    map-proj-⊎₁-[] {_}{_}{X}{Y} l = refl

term-diag : ∀{A : Obj} → Hom (Jₒ A) (Jₒ (⊤ , ⊥ , λ x y → ⊤))
term-diag {U , X , α} =
  (λ x → triv) , (λ f u → aux (f triv) u) , (λ {u}{y} → aux' {u}{y triv})
 where
   aux : 𝕃 ⊥ → U → 𝕃 X
   aux [] u = []
   aux (x :: l) u = ⊥-elim x :: aux l u

   aux' : {u : U} {l : 𝕃 ⊥} → all-pred (α u) (aux l u) → all-pred (λ y₁ → ⊤) l
   aux' {u}{l = []} p = p
   aux' {u}{l = x :: l} (p , p') = triv , aux' {u}{l} p'

term-cart-crt₁ : {X : Set} → 𝕃 (X ⊎ ⊥) → 𝕃 X
term-cart-crt₁ [] = []
term-cart-crt₁ (inj₁ x :: l) = x :: term-cart-crt₁ l
term-cart-crt₁ (inj₂ y :: l) = ⊥-elim y :: term-cart-crt₁ l

term-cart₁ : ∀{A : Obj} → Hom (Jₒ A) (Jₒ (A &ₒ (⊤ , ⊥ , λ x y → ⊤)))
term-cart₁ {U , X , α} =
  (λ x → x , triv) , (λ f u → term-cart-crt₁ (f (u , triv))) , cond
 where
   cond : {u : U} {l : 𝕃 (X ⊎ ⊥)} →
      all-pred (α u) (term-cart-crt₁ l) →
      all-pred ((α &ᵣ (λ x y₁ → ⊤)) (u , triv)) l
   cond {u}{[]} p = triv
   cond {u}{inj₁ x :: l} (p , p') = p , cond p'
   cond {u}{inj₂ y :: l} (p , p') = triv , cond p'

term-cart₂ : ∀{A : Obj} → Hom (Jₒ (A &ₒ (⊤ , ⊥ , λ x y → ⊤))) (Jₒ A)
term-cart₂ {U , X , α} = π₁

term-cart-iso₁ : ∀{A : Obj}
  → _≡h_ {Jₒ A} {Jₒ A} (comp {Jₒ A}{Jₒ (A &ₒ (⊤ , ⊥ , λ x y → ⊤))}
                             {Jₒ A} term-cart₁ term-cart₂) id
term-cart-iso₁ {U , X , α} = refl , ext-set (λ {f} → ext-set (λ {u} → aux))
 where
   aux : ∀{l : X *} → term-cart-crt₁ (map inj₁ l) ≡ l
   aux {[]} = refl
   aux {x :: l} rewrite aux {l} = refl

term-cart-iso₂ : ∀{A : Obj}
  → _≡h_ {Jₒ (A &ₒ (⊤ , ⊥ , λ x y → ⊤))}
         {Jₒ (A &ₒ (⊤ , ⊥ , λ x y → ⊤))}
         (comp {Jₒ (A &ₒ (⊤ , ⊥ , λ x y → ⊤))}{Jₒ A}
         {Jₒ (A &ₒ (⊤ , ⊥ , λ x y → ⊤))}
         term-cart₂ term-cart₁) id
term-cart-iso₂ {U , X , α} =
  ext-set aux , ext-set (λ {f} → ext-set (aux' {f}))
 where
   aux : {a : Σ U (λ x → ⊤)} → (fst a , triv) ≡ a
   aux {u , triv} = refl

   aux' : {f : Σ U (λ x → ⊤)
     → 𝕃 (X ⊎ ⊥)}{a : Σ U (λ x → ⊤)}
     → map inj₁ (term-cart-crt₁ (f (fst a , triv))) ≡ f a
   aux' {f}{u , triv} = aux''
    where
      aux'' : ∀{l : (X ⊎ ⊥) *} → map inj₁ (term-cart-crt₁ l) ≡ l
      aux'' {[]} = refl
      aux'' {inj₁ x :: l} rewrite aux'' {l} = refl
      aux'' {inj₂ y :: l} = ⊥-elim y

twist-cart : ∀{A B : Obj}
  → Hom (Jₒ (A &ₒ B)) (Jₒ (B &ₒ A))
twist-cart {A}{B} = cart-ar {A &ₒ B} {B} {A} π₂ π₁

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL