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

open import Prelude
open import Algebra

module Data.Maybe.Monoid {ℓ} (sgr : Semigroup ℓ) where

open import Data.Maybe

open Semigroup sgr

_«∙»_ : Maybe 𝑆 → Maybe 𝑆 → Maybe 𝑆
nothing «∙» y = y
just x «∙» nothing = just x
just x «∙» just y = just (x ∙ y)

maybeMonoid : Monoid ℓ
maybeMonoid .Monoid.𝑆 = Maybe 𝑆
maybeMonoid .Monoid._∙_ = _«∙»_
maybeMonoid .Monoid.ε = nothing
maybeMonoid .Monoid.assoc nothing y z = refl
maybeMonoid .Monoid.assoc (just x) nothing z = refl
maybeMonoid .Monoid.assoc (just x) (just x₁) nothing = refl
maybeMonoid .Monoid.assoc (just x) (just y) (just z) = cong just (assoc x y z)
maybeMonoid .Monoid.ε∙ _ = refl
maybeMonoid .Monoid.∙ε nothing = refl
maybeMonoid .Monoid.∙ε (just x) = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{- Copyright © 2015 Benjamin Barenblat

Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
this file except in compliance with the License.  You may obtain a copy of the
License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed
under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
CONDITIONS OF ANY KIND, either express or implied.  See the License for the
specific language governing permissions and limitations under the License. -}

module B.Prelude.Number where

import Algebra
import Data.Integer
import Data.Integer.Properties
import Data.Nat
import Data.Nat.Properties
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open Data.Integer using (ℤ) public
open Data.Nat using (ℕ) public

record NearSemiring {c} {ℓ} (A : Set c) : Set (Level.suc (c ⊔ ℓ)) where
  field
    structure : Algebra.NearSemiring c ℓ
    typeEquality : A ≡ Algebra.NearSemiring.Carrier structure

NearSemiringInstance : ∀ {c ℓ}
                     → (structure : Algebra.NearSemiring c ℓ)
                     → NearSemiring (Algebra.NearSemiring.Carrier structure)
NearSemiringInstance structure =
  record { structure = structure; typeEquality = refl }

private
  change₂ : ∀ {c ℓ A′}
          → ⦃ witness : NearSemiring {c} {ℓ} A′ ⦄
          → ((r : Algebra.NearSemiring c ℓ)
             → let A = Algebra.NearSemiring.Carrier r in
               A → A → A)
          → A′ → A′ → A′
  change₂ ⦃ witness ⦄ f rewrite NearSemiring.typeEquality witness =
    f (NearSemiring.structure witness)

_*_ : ∀ {c ℓ A} → ⦃ _ : NearSemiring {c} {ℓ} A ⦄ → A → A → A
_*_ = change₂ Algebra.NearSemiring._*_

instance
  NearSemiring-ℕ : NearSemiring ℕ
  NearSemiring-ℕ =
    NearSemiringInstance (Algebra.CommutativeSemiring.nearSemiring
                            Data.Nat.Properties.commutativeSemiring)

  NearSemiring-ℤ : NearSemiring ℤ
  NearSemiring-ℤ =
    NearSemiringInstance (Algebra.CommutativeRing.nearSemiring
                            Data.Integer.Properties.commutativeRing)

ext: agda

max_stars_repo_name: bbarenblat/B

max_issues_repo_name: bbarenblat/B

max_forks_repo_name: bbarenblat/B


text:
postulate
  foo : Set
  bar : Set

baz : Set → Set
baz fooo = Fooo

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Dodo.Unary.Union where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; cong)
open import Level using (Level; _⊔_)
open import Function using (_∘_; _∘₂_)
open import Data.Sum using (_⊎_; inj₁; inj₂; swap)
open import Data.Product using (_,_)
open import Data.Empty using (⊥-elim)
open import Relation.Unary using (Pred)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Unary.Unique
open import Dodo.Unary.Disjoint

-- # Definitions

infixl 30 _∪₁_

_∪₁_ : {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → Pred A ℓ₁
  → Pred A ℓ₂
  → Pred A (ℓ₁ ⊔ ℓ₂)
_∪₁_ p q x = p x ⊎ q x

-- # Properties

module _ {a ℓ : Level} {A : Set a} {R : Pred A ℓ} where

  ∪₁-idem : (R ∪₁ R) ⇔₁ R
  ∪₁-idem = ⇔: ⊆-proof (λ _ → inj₁)
    where
    ⊆-proof : (R ∪₁ R) ⊆₁' R
    ⊆-proof _ (inj₁ Rx) = Rx
    ⊆-proof _ (inj₂ Rx) = Rx

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} where

  ∪₁-comm : (P ∪₁ Q) ⇔₁ (Q ∪₁ P)
  ∪₁-comm = ⇔: (λ _ → swap) (λ _ → swap)

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃} where

  ∪₁-assoc : (P ∪₁ Q) ∪₁ R ⇔₁ P ∪₁ (Q ∪₁ R)
  ∪₁-assoc = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : ((P ∪₁ Q) ∪₁ R) ⊆₁' (P ∪₁ (Q ∪₁ R))
    ⊆-proof _ (inj₁ (inj₁ Px)) = inj₁ Px
    ⊆-proof _ (inj₁ (inj₂ Qx)) = inj₂ (inj₁ Qx)
    ⊆-proof _ (inj₂ Rx)        = inj₂ (inj₂ Rx)
    ⊇-proof : (P ∪₁ (Q ∪₁ R)) ⊆₁' ((P ∪₁ Q) ∪₁ R)
    ⊇-proof _ (inj₁ Px)        = inj₁ (inj₁ Px)
    ⊇-proof _ (inj₂ (inj₁ Qx)) = inj₁ (inj₂ Qx)
    ⊇-proof _ (inj₂ (inj₂ Rx)) = inj₂ Rx

-- # Operations

-- ## Operations: General

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} where

  ∪₁-unique-pred :
      Disjoint₁ P Q
    → UniquePred P
    → UniquePred Q
    → UniquePred (P ∪₁ Q)
  ∪₁-unique-pred _     uniqueP _       x (inj₁ Px₁) (inj₁ Px₂) = cong inj₁ (uniqueP x Px₁ Px₂)
  ∪₁-unique-pred disPQ _       _       x (inj₁ Px)  (inj₂ Qx)  = ⊥-elim (disPQ x (Px , Qx))
  ∪₁-unique-pred disPQ _       _       x (inj₂ Qx)  (inj₁ Px)  = ⊥-elim (disPQ x (Px , Qx))
  ∪₁-unique-pred _     _       uniqueQ x (inj₂ Qx₁) (inj₂ Qx₂) = cong inj₂ (uniqueQ x Qx₁ Qx₂)

-- ## Operations: ⊆₁

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃} where

  ∪₁-combine-⊆₁ : P ⊆₁ Q → R ⊆₁ Q → (P ∪₁ R) ⊆₁ Q
  ∪₁-combine-⊆₁ (⊆: P⊆Q) (⊆: R⊆Q) = ⊆: lemma
    where
    lemma : (P ∪₁ R) ⊆₁' Q
    lemma x (inj₁ Px) = P⊆Q x Px
    lemma x (inj₂ Rx) = R⊆Q x Rx

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} where

  ∪₁-introˡ : P ⊆₁ (Q ∪₁ P)
  ∪₁-introˡ = ⊆: λ{_ → inj₂}

  ∪₁-introʳ : P ⊆₁ (P ∪₁ Q)
  ∪₁-introʳ = ⊆: λ{_ → inj₁}

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃} where

  ∪₁-introˡ-⊆₁ : P ⊆₁ R → P ⊆₁ (Q ∪₁ R)
  ∪₁-introˡ-⊆₁ (⊆: P⊆R) = ⊆: (inj₂ ∘₂ P⊆R)

  ∪₁-introʳ-⊆₁ : P ⊆₁ Q → P ⊆₁ (Q ∪₁ R)
  ∪₁-introʳ-⊆₁ (⊆: P⊆Q) = ⊆: (inj₁ ∘₂ P⊆Q)

  ∪₁-elimˡ-⊆₁ : (P ∪₁ Q) ⊆₁ R → Q ⊆₁ R
  ∪₁-elimˡ-⊆₁ (⊆: [P∪Q]⊆R) = ⊆: (λ x → [P∪Q]⊆R x ∘ inj₂)

  ∪₁-elimʳ-⊆₁ : (P ∪₁ Q) ⊆₁ R → P ⊆₁ R
  ∪₁-elimʳ-⊆₁ (⊆: [P∪Q]⊆R) = ⊆: (λ x → [P∪Q]⊆R x ∘ inj₁)

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃} where

  ∪₁-substˡ-⊆₁ : P ⊆₁ Q → (P ∪₁ R) ⊆₁ (Q ∪₁ R)
  ∪₁-substˡ-⊆₁ (⊆: P⊆Q) = ⊆: lemma
    where
    lemma : (P ∪₁ R) ⊆₁' (Q ∪₁ R)
    lemma x (inj₁ Px) = inj₁ (P⊆Q x Px)
    lemma x (inj₂ Rx) = inj₂ Rx

  ∪₁-substʳ-⊆₁ : P ⊆₁ Q → (R ∪₁ P) ⊆₁ (R ∪₁ Q)
  ∪₁-substʳ-⊆₁ (⊆: P⊆Q) = ⊆: lemma
    where
    lemma : (R ∪₁ P) ⊆₁' (R ∪₁ Q)
    lemma x (inj₁ Rx) = inj₁ Rx
    lemma x (inj₂ Px) = inj₂ (P⊆Q x Px)

-- ## Operations: ⇔₂

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃} where

  ∪₁-substˡ : P ⇔₁ Q → (P ∪₁ R) ⇔₁ (Q ∪₁ R)
  ∪₁-substˡ = ⇔₁-compose ∪₁-substˡ-⊆₁ ∪₁-substˡ-⊆₁

  ∪₁-substʳ : P ⇔₁ Q → (R ∪₁ P) ⇔₁ (R ∪₁ Q)
  ∪₁-substʳ = ⇔₁-compose ∪₁-substʳ-⊆₁ ∪₁-substʳ-⊆₁

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
module Recutter where

open import Basics
open import All
open import Cutting
open import Perm

module RECUTTER {I}(C : I |> I) where

  open _|>_

  CutKit : (I -> Set) -> Set
  CutKit P = (i : I)(c : Cuts C i) -> P i -> All P (inners C c)

  Subs : List I -> Set
  Subs = All (\ i -> One + Cuts C i)
  subCollect : (is : List I) -> Subs is -> List I
  subCollect is cs = collect is (all (\ i -> (\ _ -> i ,- []) <+> inners C) is cs)

  Sub : I |> Sg I (Cuts C)
  Cuts   Sub (i , c) = Subs (inners C c)
  inners Sub {i , c} cs = subCollect (inners C c) cs

  Recutter : Set
  Recutter = (i : I)(c c' : Cuts C i) ->
             Sg (Cuts Sub (i , c)) \ d -> Sg (Cuts Sub (i , c')) \ d' ->
             inners Sub d ~ inners Sub d'

module NATRECUT where

  open RECUTTER NatCut

  data CutCompare (x x' y y' n : Nat) : Set where
    cutLt : (d : Nat) -> (x +N suc d) == y -> (suc d +N y') == x' ->
      CutCompare x x' y y' n
    cutEq : x == y -> x' == y' ->
      CutCompare x x' y y' n
    cutGt : (d : Nat) -> (y +N suc d) == x -> (suc d +N x') == y' ->
      CutCompare x x' y y' n

  sucInj : {x y : Nat} -> suc x == suc y -> x == y
  sucInj (refl (suc _)) = refl _

  cutCompare : (x x' y y' n : Nat) -> (x +N x') == n -> (y +N y') == n ->
               CutCompare x x' y y' n
  cutCompare zero .n zero .n n (refl _) (refl _)
    = cutEq (refl _) (refl _)
  cutCompare zero .(suc (y +N y')) (suc y) y' .(suc (y +N y')) (refl _) (refl _)
    = cutLt y (refl _) (refl _)
  cutCompare (suc x) x' zero .(suc (x +N x')) .(suc (x +N x')) (refl _) (refl _)
    = cutGt x (refl _) (refl _)
  cutCompare (suc x) x' (suc y) y' zero () ()
  cutCompare (suc x) x' (suc y) y' (suc n) xq yq
    with cutCompare x x' y y' n (sucInj xq) (sucInj yq)
  cutCompare (suc x) x' (suc .(x +N suc d)) y' (suc n) xq yq
    | cutLt d (refl _) bq = cutLt d (refl _) bq
  cutCompare (suc x) x' (suc .x) y' (suc n) xq yq
    | cutEq (refl _) bq = cutEq (refl _) bq
  cutCompare (suc .(y +N suc d)) x' (suc y) y' (suc n) xq yq
    | cutGt d (refl _) bq = cutGt d (refl _) bq

  NatRecut : Recutter
  NatRecut n (a , b , qab) (c , d , qcd) with cutCompare a b c d n qab qcd
  NatRecut n (a , b , qab) (c , d , qcd) | cutLt e q0 q1
    = (inl <> , inr (suc e , d , q1) , <>)
    , (inr (a , suc e , q0) , inl <> , <>)
    , reflP _
  NatRecut n (a , b , qab) (.a , .b , qcd) | cutEq (refl .a) (refl .b)
    = (inl <> , inl <> , <>)
    , (inl <> , inl <> , <>)
    , reflP _
  NatRecut n (a , b , qab) (c , d , qcd) | cutGt e q0 q1
    = (inr (c , suc e , q0) , inl <> , <>)
    , (inl <> , inr (suc e , b , q1) , <>)
    , reflP _

module SUBCOLLECTLEMMA where

  open _|>_
  open RECUTTER

  subCollectLemma : forall {I J}(C : I |> I)(D : J |> J)
                    (f : I -> J)(g : (i : I) -> Cuts C i -> Cuts D (f i)) ->
                    (q : (i : I)(c : Cuts C i) -> inners D (g i c) == list f (inners C c)) ->
                    (is : List I)(ps : All (\ i -> One + Cuts C i) is) ->
                    subCollect D (list f is) (allRe f is (all (\ i -> id +map g i) is ps)) ==
                    list f (subCollect C is ps)
  subCollectLemma C D f g q [] <> = refl []
  subCollectLemma C D f g q (i ,- is) (inl <> , ps) =
    refl (f i ,-_) =$= subCollectLemma C D f g q is ps
  subCollectLemma C D f g q (i ,- is) (inr c , ps) =
    (inners D (g i c) +L
     subCollect D (list f is) (allRe f is (allAp is (allPu (\ i -> id +map g i) is) ps)))
      =[ refl _+L_ =$= q i c =$= subCollectLemma C D f g q is ps >=
    (list f (inners C c) +L list f (subCollect C is ps))
      =[ catNatural f (inners C c) (subCollect C is ps) >=
    list f (inners C c +L subCollect C is ps)
      [QED]

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


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

open import Definition.Typed.EqualityRelation

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

open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution

open import Tools.Product

-- Conversion from left to right of valid terms.
convᵛ : ∀ {t A B Γ l}
        ([Γ] : ⊩ᵛ Γ)
        ([A]  : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
        ([B]  : Γ ⊩ᵛ⟨ l ⟩ B / [Γ])
      → Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A]
      → Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A]
      → Γ ⊩ᵛ⟨ l ⟩ t ∷ B / [Γ] / [B]
convᵛ [Γ] [A] [B] [A≡B] [t] ⊢Δ [σ] =
  let [σA]     = proj₁ ([A] ⊢Δ [σ])
      [σB]     = proj₁ ([B] ⊢Δ [σ])
      [σA≡σB]  = irrelevanceEq [σA] [σA] ([A≡B] ⊢Δ [σ])
      [σt]     = proj₁ ([t] ⊢Δ [σ])
      [σt≡σ′t] = λ σ′ → proj₂ ([t] ⊢Δ [σ]) {σ′ = σ′}
  in  convTerm₁ [σA] [σB] [σA≡σB] [σt]
  ,   λ [σ′] [σ≡σ′] → convEqTerm₁ [σA] [σB] [σA≡σB] (([σt≡σ′t] _) [σ′] [σ≡σ′])

-- Conversion from right to left of valid terms.
conv₂ᵛ : ∀ {t A B Γ l}
         ([Γ] : ⊩ᵛ Γ)
         ([A]  : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
         ([B]  : Γ ⊩ᵛ⟨ l ⟩ B / [Γ])
       → Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A]
       → Γ ⊩ᵛ⟨ l ⟩ t ∷ B / [Γ] / [B]
       → Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A]
conv₂ᵛ [Γ] [A] [B] [A≡B] [t] ⊢Δ [σ] =
  let [σA]     = proj₁ ([A] ⊢Δ [σ])
      [σB]     = proj₁ ([B] ⊢Δ [σ])
      [σA≡σB]  = irrelevanceEq [σA] [σA] ([A≡B] ⊢Δ [σ])
      [σt]     = proj₁ ([t] ⊢Δ [σ])
      [σt≡σ′t] = λ σ′ → (proj₂ ([t] ⊢Δ [σ]) {σ′ = σ′})
  in  convTerm₂ [σA] [σB] [σA≡σB] [σt]
  ,   λ [σ′] [σ≡σ′] → convEqTerm₂ [σA] [σB] [σA≡σB] (([σt≡σ′t] _) [σ′] [σ≡σ′])

-- Conversion from left to right of valid term equality.
convEqᵛ : ∀ {t u A B Γ l}
        ([Γ] : ⊩ᵛ Γ)
        ([A]  : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
        ([B]  : Γ ⊩ᵛ⟨ l ⟩ B / [Γ])
      → Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A]
      → Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A]
      → Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ B / [Γ] / [B]
convEqᵛ [Γ] [A] [B] [A≡B] [t≡u] ⊢Δ [σ] =
  let [σA]     = proj₁ ([A] ⊢Δ [σ])
      [σB]     = proj₁ ([B] ⊢Δ [σ])
      [σA≡σB]  = irrelevanceEq [σA] [σA] ([A≡B] ⊢Δ [σ])
  in  convEqTerm₁ [σA] [σB] [σA≡σB] ([t≡u] ⊢Δ [σ])

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module Abstract where

abstract

  f
    : {A : Set}
    → A
    → A
  f x
    = x

  g
    : {A : Set}
    → A
    → A
  g x
    = x

  h
    : {A : Set}
    → A
    → A
  h x
    = f x

  _
    : {A : Set}
    → A
    → A
  _
    = λ x → x

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
-- 2012-03-06 Andreas
-- Errors during printing of debug messages should not propagate to the
-- top level

{-# OPTIONS -v tc.meta.assign:10 #-}
module Issue578 where

-- Skipping import of Level will leave us with no level builtins
-- import Level

data D : Set where

-- This will generate a debug message, but it cannot be printed
-- since there are no bindings for the level builtins.

-- However, the file should still succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2017-01-19, issue #2416, probably regression
-- Give failed for constrained size

-- {-# OPTIONS -v interaction.give:40 #-}
-- {-# OPTIONS -v tc.conv:10 #-}
-- {-# OPTIONS -v tc.conv.coerce:70 #-}
-- {-# OPTIONS -v tc.size:40 #-}
-- {-# OPTIONS -v tc.check.internal:40 #-}

open import Common.Size
open import Common.Equality

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

postulate
  divideBySuc : Nat ∞ → ∀ k → Nat k → Nat k
  div-self : ∀ l (n : Nat l) → divideBySuc n (↑ l) (suc {! l !} n) ≡ suc l zero

-- Cannot solve size constraints
-- [i, n] i ≤ _j_19 i n
-- [i, n] (↑ _j_19 i n) ≤ _i_18 i n
-- [i, n] (↑ _j_20 i n) ≤ _i_18 i n
-- Reason: inconsistent upper bound for 20
-- when checking that zero is a valid argument to a function of type


text:
open import Auto
open import Function using (const)
open import Data.Bool using (Bool; true; false)
open import Data.Bool.Show as Bool using ()
open import Data.List using (_∷_; [])
open import Data.Maybe
open import Data.Nat using (ℕ; suc; zero)
open import Data.Nat.Show as Nat using ()
open import Data.String using (String; _++_)
open import Data.Sum renaming (_⊎_ to Either; inj₁ to left; inj₂ to right)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

module Auto.Example.TypeClasses where

--------------------------------------------------------------------------------
-- * We can construct a class for the Show function (as a dependent record) * --
--------------------------------------------------------------------------------

record Show (A : Set) : Set where
  constructor mkShow
  field
    show : A → String

open Show {{...}}

--------------------------------------------------------------------------------
-- * And set up a list of rules which guide the instance resolution         * --
--------------------------------------------------------------------------------

rules : HintDB
rules = [] << quote instShowEither << quote instShowBool << quote instShowNat
  where
    instShowBool : Show Bool
    instShowBool = mkShow Bool.show

    instShowNat : Show ℕ
    instShowNat = mkShow Nat.show

    instShowEither : {A B : Set} → Show A → Show B → Show (Either A B)
    instShowEither {A} {B} instShowA instShowB = mkShow showEither
      where
        showEither : Either A B → String
        showEither (left  x) = "left "  ++ show x
        showEither (right y) = "right " ++ show y

--------------------------------------------------------------------------------
-- * Using these rules and `auto` we can easily and robustly compute the    * --
-- * instances we need.                                                     * --
--------------------------------------------------------------------------------

example₁ : String
example₁ = show (left true) ++ show (right 4)
  where
    instance
      inst : Show (Either Bool ℕ)
      inst = tactic (auto 5 rules)

--------------------------------------------------------------------------------
-- * This fails due to normalisation from the non-dependent pair _×_ to the * --
-- * dependent pair Σ (as `A × B` is defined as `Σ A (λ _ → B)`).           * --
--------------------------------------------------------------------------------
module DefaultPair where

  open import Data.Product using (_×_; _,_)

  instShowPair : {A B : Set} → Show A → Show B → Show (A × B)
  instShowPair {A} {B} showA showB = record { show = showPair }
    where
      showPair : A × B → String
      showPair (proj₁ , proj₂) = show proj₁ ++ "," ++ show proj₂

  inst : Exception unsupportedSyntax
  inst = unquote (auto 5 (rules << quote instShowPair) g)
    where
      g = quoteTerm (Show (Bool × ℕ))

--------------------------------------------------------------------------------
-- * So we're forced to use a custom pair, which isn't derived from         * --
-- * a dependent pair                                                       * --
--------------------------------------------------------------------------------
module CustomPair where

  data _×_ (A B : Set) : Set where
    _,_ : A → B → A × B

  instShowPair : ∀ {A B} → Show A → Show B → Show (A × B)
  instShowPair {A} {B} showA showB = record { show = showPair }
    where
      showPair : A × B → String
      showPair (proj₁ , proj₂) = show proj₁ ++ "," ++ show proj₂

  example₂ : String
  example₂ = show (true , 1)
    where
      instance
        inst : Show (Bool × ℕ)
        inst = tactic (auto 5 (rules << quote instShowPair))

--------------------------------------------------------------------------------
-- * This fails due to something super weird which I haven't encountered    * --
-- * before at all...                                                       * --
--------------------------------------------------------------------------------
module AbstractPair where

  open import Data.Product as Σ using (Σ)

  abstract
    _×_ : (A B : Set) → Set
    A × B = Σ A (const B)

    instShowPair : ∀ {A B} → Show A → Show B → Show (A × B)
    instShowPair {A} {B} showA showB = record { show = showPair }
      where
        showPair : A × B → String
        showPair (proj₁ Σ., proj₂) = show proj₁ ++ "," ++ show proj₂

    _,_ : {A B : Set} (x : A) (y : B) → A × B
    _,_ = Σ._,_

  --inst : Show (Bool × ℕ)
  --inst = tactic (auto 5 (rules << quote instShowPair))

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda


text:
module Peano where
  data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

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

  data _even : ℕ → Set where
    ZERO : zero even
    STEP : ∀ x → x even → suc (suc x) even

  proof₁ : suc (suc (suc (suc zero))) even
  proof₁ = STEP (suc (suc zero)) (STEP zero ZERO)


text:
{- Name: Bowornmet (Ben) Hudson

-- define the source language from the paper

-}

open import Preliminaries
open import Preorder-withmax

module Source-lang where

  -- define the source language from the paper
  -- we want to focus on arrow, cross, and nat types
  data Tp : Set where
    unit : Tp
    nat : Tp
    susp : Tp → Tp
    _->s_ : Tp → Tp → Tp
    _×s_ : Tp → Tp → Tp

  data Cost : Set where
    0c : Cost
    1c : Cost
    _+c_ : Cost → Cost → Cost

  data Equals0c : Cost → Set where
    Eq0-0c : Equals0c 0c
    Eq0-+c : ∀ {c c'} → Equals0c c → Equals0c c' → Equals0c (c +c c')

  -- represent a context as a list of types
  Ctx = List Tp

  -- de Bruijn indices (for free variables)
  data _∈_ : Tp → Ctx → Set where
    i0 : ∀ {Γ τ}
       → τ ∈ (τ :: Γ)
    iS : ∀ {Γ τ τ1}
       → τ ∈ Γ
       → τ ∈ (τ1 :: Γ)

  data _|-_ : Ctx → Tp → Set where
    unit : ∀ {Γ}
         → Γ |- unit
    var : ∀ {Γ τ}
        → τ ∈ Γ
        → Γ |- τ
    z : ∀ {Γ}
      → Γ |- nat
    suc : ∀ {Γ}
        → (e : Γ |- nat)
        → Γ |- nat
    rec : ∀ {Γ τ}
        → Γ |- nat
        → Γ |- τ
        → (nat :: (susp τ :: Γ)) |- τ
        → Γ |- τ
    lam : ∀ {Γ τ ρ}
        → (ρ :: Γ) |- τ
        → Γ |- (ρ ->s τ)
    app : ∀ {Γ τ1 τ2}
        → Γ |- (τ2 ->s τ1)
        → Γ |- τ2
        → Γ |- τ1
    prod : ∀ {Γ τ1 τ2}
         → Γ |- τ1
         → Γ |- τ2
         → Γ |- (τ1 ×s τ2)
    l-proj : ∀ {Γ τ1 τ2}
           → Γ |- (τ1 ×s τ2)
           → Γ |- τ1
    r-proj : ∀ {Γ τ1 τ2}
           → Γ |- (τ1 ×s τ2)
           → Γ |- τ2
    -- include split, delay/susp/force instead of usual elim rules for products
    delay : ∀ {Γ τ}
          → Γ |- τ
          → Γ |- susp τ
    force : ∀ {Γ τ}
          → Γ |- susp τ
          → Γ |- τ
    split : ∀ {Γ τ τ1 τ2}
          → Γ |- (τ1 ×s τ2)
          → (τ1 :: (τ2 :: Γ)) |- τ
          → Γ |- τ

------weakening and substitution lemmas

 -- renaming function
  rctx : Ctx → Ctx → Set
  rctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → τ ∈ Γ

  -- re: transferring variables in contexts
  lem1 : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) (τ :: Γ')
  lem1 d i0 = i0
  lem1 d (iS x) = iS (d x)

  -- renaming lemma
  ren : ∀ {Γ Γ' τ} → Γ' |- τ → rctx Γ Γ' → Γ |- τ
  ren unit d = unit
  ren (var x) d = var (d x)
  ren z d = z
  ren (suc e) d = suc (ren e d)
  ren (rec e e0 e1) d = rec (ren e d) (ren e0 d) (ren e1 (lem1 (lem1 d)))
  ren (lam e) d = lam (ren e (lem1 d))
  ren (app e1 e2) d = app (ren e1 d) (ren e2 d)
  ren (prod e1 e2) d = prod (ren e1 d) (ren e2 d)
  ren (l-proj e) d = l-proj (ren e d)
  ren (r-proj e) d = r-proj (ren e d)
  ren (delay e) d = delay (ren e d)
  ren (force e) d = force (ren e d)
  ren (split e e1) d = split (ren e d) (ren e1 (lem1 (lem1 d)))

  -- substitution
  sctx : Ctx → Ctx → Set
  sctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → Γ |- τ

  -- weakening a context
  wkn : ∀ {Γ τ1 τ2} → Γ |- τ2 → (τ1 :: Γ) |- τ2
  wkn e = ren e iS

  -- weakening also works with substitution
  wkn-s : ∀ {Γ τ1 Γ'} → sctx Γ Γ' → sctx (τ1 :: Γ) Γ'
  wkn-s d = λ f → wkn (d f)

  wkn-r : ∀ {Γ τ1 Γ'} → rctx Γ Γ' → rctx (τ1 :: Γ) Γ'
  wkn-r d = λ x → iS (d x)

  -- lem2 (need a lemma for subst like we did for renaming)
  lem2 : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) (τ :: Γ')
  lem2 d i0 = var i0
  lem2 d (iS i) = wkn (d i)

  -- another substitution lemma
  lem3 : ∀ {Γ τ} → Γ |- τ → sctx Γ (τ :: Γ)
  lem3 e i0 = e
  lem3 e (iS i) = var i

  lem3' : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ |- τ → sctx Γ (τ :: Γ')
  lem3' Θ e i0 = e
  lem3' Θ e (iS i) = Θ i

  -- one final lemma needed for the last stepping rule. Thank you Professor Licata!
  lem4 : ∀ {Γ τ1 τ2} → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ))
  lem4 e1 e2 i0 = e1
  lem4 e1 e2 (iS i0) = e2
  lem4 e1 e2 (iS (iS i)) = var i

  lem4' : ∀ {Γ Γ' τ1 τ2} → sctx Γ Γ' → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ'))
  lem4' Θ a b i0 = a
  lem4' Θ a b (iS i0) = b
  lem4' Θ a b (iS (iS i)) = Θ i

  lem5 : ∀ {Γ τ1 τ2} → Γ |- (τ1 ×s τ2) → sctx Γ ((τ1 ×s τ2) :: (τ1 :: (τ2 :: Γ)))
  lem5 e i0 = e
  lem5 e (iS i0) = l-proj e
  lem5 e (iS (iS i0)) = r-proj e
  lem5 e (iS (iS (iS i))) = var i

  ids-2 : ∀ {Γ τ} → Γ |- τ → sctx Γ Γ → Γ |- τ
  ids-2 e Θ = e

  -- the 'real' substitution lemma (if (x : τ') :: Γ |- (e : τ) and Γ |- (e : τ') , then Γ |- e[x -> e'] : τ)
  subst : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ' |- τ → Γ |- τ

  subst d unit = unit
  subst d (var x) = d x
  subst d z = z
  subst d (suc x) = suc (subst d x)
  subst d (rec e e0 e1) = rec (subst d e) (subst d e0) (subst (lem2 (lem2 d)) e1)
  subst d (lam e) = lam (subst (lem2 d) e)
  subst d (app e1 e2) = app (subst d e1) (subst d e2)
  subst d (prod e1 e2) = prod (subst d e1) (subst d e2)
  subst d (l-proj e) = l-proj (subst d e)
  subst d (r-proj e) = r-proj (subst d e)
  subst d (delay e) = delay (subst d e)
  subst d (force e) = force (subst d e)
  subst d (split e e1) = split (subst d e) (subst (lem2 (lem2 d)) e1)

  s-comp1 : ∀ {Γ Γ' Γ''} → sctx Γ Γ' → sctx Γ'' Γ → sctx Γ'' Γ'
  s-comp1 Θ Θ' = subst Θ' o Θ

  postulate
    subst-compose : ∀ {Γ Γ' τ τ1} (Θ : sctx Γ Γ') (v : Γ |- τ) (e : (τ :: Γ' |- τ1) )
                  → subst (lem3 v) (subst (lem2 Θ) e) == subst (lem3' Θ v) e
    --subst-compose {Γ} {_} Θ v e = {!!}

  postulate
    subst-compose2 : ∀ {Γ Γ' τ} (Θ : sctx Γ Γ') (n : Γ |- nat) (e1 : Γ' |- τ) (e2 : (nat :: (susp τ :: Γ')) |- τ)
                  →  subst (lem4 n (delay (rec n (subst Θ e1) (subst (lem2 (lem2 Θ)) e2)))) (subst (lem2 (lem2 Θ)) e2) ==
                     subst (lem4' Θ n (delay (rec n (subst Θ e1) (subst (lem2 (lem2 Θ)) e2)))) e2

  postulate
    subst-compose3 : ∀ {Γ Γ' τ τ1 τ2} (Θ : sctx Γ Γ') (e1 : (τ1 :: (τ2 :: Γ')) |- τ) (v1 : Γ |- τ1) (v2 : Γ |- τ2)
                   → subst (lem4 v1 v2) (subst (lem2 (lem2 Θ)) e1) == subst (lem4' Θ v1 v2) e1

  postulate
    subst-compose4 : ∀ {Γ Γ' τ} (Θ : sctx Γ Γ') (v' : Γ |- nat) (r : Γ |- susp τ) (e2 : (nat :: (susp τ :: Γ')) |- τ)
                   → subst (lem4 v' r) (subst (lem2 (lem2 Θ)) e2) == subst (lem4' Θ v' r) e2

-------

  data val : ∀ {τ} → [] |- τ → Set where
    z-isval : val z
    suc-isval : (e : [] |- nat) → (val e)
              → val (suc e)
    pair-isval : ∀ {τ1 τ2} (e1 : [] |- τ1) → (e2 : [] |- τ2)
               → val e1 → val e2
               → val (prod e1 e2)
    lam-isval : ∀ {ρ τ} (e : (ρ :: []) |- τ)
              → val (lam e)
    unit-isval : val unit
    delay-isval : ∀ {τ} (e : [] |- τ) → val (delay e)

  mutual
    -- define evals (e : source exp) (v : value) (c : nat)
    -- analogous to "e evaluates to v in c steps"
    -- see figure 4 of paper
    data evals : {τ : Tp} → [] |- τ → [] |- τ → Cost → Set where
      pair-evals : ∀ {n1 n2}
                 → {τ1 τ2 : Tp} {e1 v1 : [] |- τ1} {e2 v2 : [] |- τ2}
                 → evals e1 v1 n1
                 → evals e2 v2 n2
                 → evals (prod e1 e2) (prod v1 v2) (n1 +c n2)
      lam-evals : ∀ {ρ τ} {e : (ρ :: []) |- τ}
                → evals (lam e) (lam e) 0c
      app-evals : ∀ {n0 n1 n}
               → {τ1 τ2 : Tp} {e0 : [] |- (τ1 ->s τ2)} {e0' : (τ1 :: []) |- τ2} {e1 v1 : [] |- τ1} {v : [] |- τ2}
               → evals e0 (lam e0') n0
               → evals e1 v1 n1
               → evals (subst (lem3 v1) e0') v n
               → evals (app e0 e1) v ((n0 +c n1) +c n)
      z-evals : evals z z 0c
      s-evals : ∀ {n}
              → {e v : [] |- nat}
              → evals e v n
              → evals (suc e) (suc v) n
      unit-evals : evals unit unit 0c
      rec-evals : ∀ {n1 n2}
                  → {τ : Tp} {e v : [] |- nat} {e0 v' : [] |- τ} {e1 : (nat :: (susp τ :: [])) |- τ}
                  → evals e v n1
                  → evals-rec-branch e0 e1 v v' n2
                  → evals (rec e e0 e1) v' (n1 +c (1c +c n2))
      -- adding some new rules to the mix
      delay-evals : {τ : Tp} {e : [] |- τ}
                  → evals (delay e) (delay e) 0c
      force-evals : ∀ {n1 n2}
                  → {τ : Tp} {e' v : [] |- τ} {e : [] |- susp τ}
                  → evals e (delay e') n1
                  → evals e' v n2
                  → evals (force e) v (n1 +c n2)
      split-evals : ∀ {n1 n2}
                  → {τ τ1 τ2 : Tp} {e0 : [] |- (τ1 ×s τ2)} {v1 : [] |- τ1} {v2 : [] |- τ2} {e1 : (τ1 :: (τ2 :: [])) |- τ} {v : [] |- τ}
                  → evals e0 (prod v1 v2) n1
                  → evals (subst (lem4 v1 v2) e1) v n2
                  → evals (split e0 e1) v (n1 +c n2)

    -- means   evals (rec v e0 e1) v' n
    -- but helpful to have a separate type for this
    data evals-rec-branch {τ : Tp} (e0 : [] |- τ) (e1 : (nat :: (susp τ :: [])) |- τ) : (e : [] |- nat) (v : [] |- τ) → Cost → Set where
         evals-rec-z : ∀ {v n} → evals e0 v n → evals-rec-branch e0 e1 z v n
         evals-rec-s : ∀ {v v' n} → evals (subst (lem4 v (delay (rec v e0 e1))) e1) v' n
                               → evals-rec-branch e0 e1 (suc v) v' n

  evals-val : {τ : Tp} {e : [] |- τ} {v : [] |- τ} {n : Cost} → evals e v n → val v
  evals-val (pair-evals D D₁) = pair-isval _ _ (evals-val D) (evals-val D₁)
  evals-val lam-evals = lam-isval _
  evals-val (app-evals D D₁ D₂) = evals-val D₂
  evals-val z-evals = z-isval
  evals-val (s-evals D) = suc-isval _ (evals-val D)
  evals-val unit-evals = unit-isval
  evals-val (rec-evals x (evals-rec-z D)) = evals-val D
  evals-val (rec-evals x (evals-rec-s D)) = evals-val D
  evals-val delay-evals = delay-isval _
  evals-val (force-evals D D₁) = evals-val D₁
  evals-val (split-evals D D₁) = evals-val D₁

  val-evals-inversion : {τ : Tp} {v v' : [] |- τ} {n : Cost} → val v → evals v v' n → (v == v') × Equals0c n
  val-evals-inversion z-isval z-evals = Refl , Eq0-0c
  val-evals-inversion (suc-isval e valv) (s-evals evv) = ap suc (fst IH) , snd IH where
    IH = val-evals-inversion valv evv
  val-evals-inversion (pair-isval e1 e2 valv valv₁) (pair-evals evv evv₁) = ap2 prod (fst IH1) (fst IH2) , Eq0-+c (snd IH1) (snd IH2) where
    IH1 = val-evals-inversion valv evv
    IH2 = val-evals-inversion valv₁ evv₁
  val-evals-inversion (lam-isval e) lam-evals = Refl , Eq0-0c
  val-evals-inversion unit-isval unit-evals = Refl , Eq0-0c
  val-evals-inversion (delay-isval e) delay-evals = Refl , Eq0-0c

---------- some sample programs in the source language

  --dbl(n : nat) = 2*n
  dbl : ∀ {Γ} → Γ |- (nat ->s nat)
  dbl = lam (rec (var i0) z (suc (suc (force (var (iS i0))))))

  --add(x : nat , y : nat) = x+y
  add : ∀ {Γ} → Γ |- (nat ->s (nat ->s nat))
  add = lam (lam (rec (var (iS i0)) (var i0) (suc (force (var (iS i0))))))

  --mult(x : nat , y : nat) = x*y
  mult : ∀ {Γ} → Γ |- (nat ->s (nat ->s nat))
  mult = lam (lam (rec (var (iS i0)) z (app (app add (var (iS (iS i0)))) (force (var (iS i0))))))

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
------------------------------------------------------------------------
-- Lemmas related to application of substitutions
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Application.Application222
  {i u e} {Uni : IndexedUniverse i u e}
  where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Application.Application221
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.Map
open import deBruijn.Substitution.Data.Simple
open import Function using (_$_)
open import Level using (_⊔_)
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

-- Lemmas related to application.

record Application₂₂₂
  {t₁} {T₁ : Term-like t₁}
  {t₂} {T₂ : Term-like t₂}

  -- Simple substitutions for the first kind of terms.
  (simple₁ : Simple T₁)

  -- Simple substitutions for the second kind of terms.
  (simple₂ : Simple T₂)

  -- A translation from the first to the second kind of terms.
  (trans : [ T₁ ⟶⁼ T₂ ])
  : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where

  open Term-like T₁ using () renaming (_⊢_ to _⊢₁_)
  open Term-like T₂ using ([_]) renaming (_⊢_ to _⊢₂_; _≅-⊢_ to _≅-⊢₂_)
  open Simple simple₁
    using ()
    renaming ( id to id₁; sub to sub₁; var to var₁
             ; wk to wk₁; wk[_] to wk₁[_]
             ; _↑ to _↑₁; _↑_ to _↑₁_; _↑⁺_ to _↑⁺₁_; _↑₊_ to _↑₊₁_
             ; _↑⋆ to _↑⋆₁; _↑⁺⋆_ to _↑⁺⋆₁_
             )
  open Simple simple₂
    using ()
    renaming ( var to var₂
             ; weaken to weaken₂; weaken[_] to weaken₂[_]; wk⁺ to wk⁺₂
             ; wk-subst to wk-subst₂; wk-subst[_] to wk-subst₂[_]
             ; _↑ to _↑₂; _↑_ to _↑₂_; _↑⁺_ to _↑⁺₂_; _↑₊_ to _↑₊₂_
             )

  field
    application₂₂₁ : Application₂₂₁ simple₁ simple₂ trans

  open Application₂₂₁ application₂₂₁ public

  abstract

    -- A variant of suc-/∋-↑.

    suc-/⊢⋆-↑⋆ :
      ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
      σ {τ} (x : Γ ∋ τ) (ρs : Subs T₁ ρ̂) →
      var₂ · suc[ σ ] x /⊢⋆ ρs ↑⋆₁ ≅-⊢₂
      var₂ · x /⊢⋆ (ρs ▻ wk₁[ σ /⋆ ρs ])
    suc-/⊢⋆-↑⋆ σ x ε = begin
      [ var₂ · suc x    ]  ≡⟨ P.sym $ var-/⊢-wk-↑⁺ ε x ⟩
      [ var₂ · x /⊢ wk₁ ]  ∎
    suc-/⊢⋆-↑⋆ σ x (ρs ▻ ρ) = begin
      [ var₂ · suc[ σ ] x /⊢⋆ ρs ↑⋆₁ /⊢ ρ ↑₁      ]  ≡⟨ /⊢-cong (suc-/⊢⋆-↑⋆ σ x ρs) (P.refl {x = [ ρ ↑₁ ]}) ⟩
      [ var₂ · x /⊢⋆ ρs /⊢ wk₁[ σ /⋆ ρs ] /⊢ ρ ↑₁ ]  ≡⟨ P.sym $ /⊢-/⊢-wk (σ /⋆ ρs) (var₂ · x /⊢⋆ ρs) ρ ⟩
      [ var₂ · x /⊢⋆ ρs /⊢ ρ /⊢ wk₁               ]  ∎

    -- The antecedent of var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ follows from a less
    -- complicated statement.

    var-/⊢⋆-⇒-var-/⊢⋆-↑⁺⋆ :
      ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} {ρs₁ : Subs T₁ ρ̂} {ρs₂ : Subs T₁ ρ̂} →
      (∀ {σ} (x : Γ ∋ σ) → var₂ · x /⊢⋆ ρs₁ ≅-⊢₂ var₂ · x /⊢⋆ ρs₂) →
      ∀ Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
      var₂ · x /⊢⋆ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢₂ var₂ · x /⊢⋆ ρs₂ ↑⁺⋆₁ Γ⁺
    var-/⊢⋆-⇒-var-/⊢⋆-↑⁺⋆                   hyp ε        x    = hyp x
    var-/⊢⋆-⇒-var-/⊢⋆-↑⁺⋆ {ρs₁ = ρs₁} {ρs₂} hyp (Γ⁺ ▻ σ) zero = begin
      [ var₂ · zero /⊢⋆ ρs₁ ↑⁺⋆₁ (Γ⁺ ▻ σ) ]  ≡⟨ zero-/⊢⋆-↑⋆ σ (ρs₁ ↑⁺⋆₁ Γ⁺) ⟩
      [ var₂ · zero                       ]  ≡⟨ P.sym $ zero-/⊢⋆-↑⋆ σ (ρs₂ ↑⁺⋆₁ Γ⁺) ⟩
      [ var₂ · zero /⊢⋆ ρs₂ ↑⁺⋆₁ (Γ⁺ ▻ σ) ]  ∎
    var-/⊢⋆-⇒-var-/⊢⋆-↑⁺⋆ {ρs₁ = ρs₁} {ρs₂} hyp (Γ⁺ ▻ σ) (suc x) = begin
      [ var₂ · suc x /⊢⋆ ρs₁ ↑⁺⋆₁ (Γ⁺ ▻ σ)  ]  ≡⟨ suc-/⊢⋆-↑⋆ σ x (ρs₁ ↑⁺⋆₁ Γ⁺) ⟩
      [ var₂ · x     /⊢⋆ ρs₁ ↑⁺⋆₁ Γ⁺ /⊢ wk₁ ]  ≡⟨ /⊢-cong (var-/⊢⋆-⇒-var-/⊢⋆-↑⁺⋆ hyp Γ⁺ x) (P.refl {x = [ wk₁ ]}) ⟩
      [ var₂ · x     /⊢⋆ ρs₂ ↑⁺⋆₁ Γ⁺ /⊢ wk₁ ]  ≡⟨ P.sym $ suc-/⊢⋆-↑⋆ σ x (ρs₂ ↑⁺⋆₁ Γ⁺) ⟩
      [ var₂ · suc x /⊢⋆ ρs₂ ↑⁺⋆₁ (Γ⁺ ▻ σ)  ]  ∎

    -- Variants of var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ which may be easier to use.

    var-/⊢⋆-⇒-/⊢⋆-↑⁺⋆ :
      ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs₁ : Subs T₁ ρ̂) (ρs₂ : Subs T₁ ρ̂) →
      (∀ {σ} (x : Γ ∋ σ) → var₂ · x /⊢⋆ ρs₁ ≅-⊢₂ var₂ · x /⊢⋆ ρs₂) →
      ∀ Γ⁺ {σ} (t : Γ ++⁺ Γ⁺ ⊢₂ σ) →
      t /⊢⋆ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t /⊢⋆ ρs₂ ↑⁺⋆₁ Γ⁺
    var-/⊢⋆-⇒-/⊢⋆-↑⁺⋆ ρs₁ ρs₂ hyp =
      var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ ρs₁ ρs₂ (var-/⊢⋆-⇒-var-/⊢⋆-↑⁺⋆ hyp)

    var-/⊢⋆-⇒-/⊢⋆ :
      ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs₁ : Subs T₁ ρ̂) (ρs₂ : Subs T₁ ρ̂) →
      (∀ {σ} (x : Γ ∋ σ) → var₂ · x /⊢⋆ ρs₁ ≅-⊢₂ var₂ · x /⊢⋆ ρs₂) →
      ∀ {σ} (t : Γ ⊢₂ σ) → t /⊢⋆ ρs₁ ≅-⊢₂ t /⊢⋆ ρs₂
    var-/⊢⋆-⇒-/⊢⋆ ρs₁ ρs₂ hyp = var-/⊢⋆-⇒-/⊢⋆-↑⁺⋆ ρs₁ ρs₂ hyp ε

    -- The identity substitution has no effect.

    /⊢-id : ∀ {Γ σ} (t : Γ ⊢₂ σ) → t /⊢ id₁ ≅-⊢₂ t
    /⊢-id = var-/⊢⋆-⇒-/⊢⋆ (ε ▻ id₁) ε var-/⊢-id

    -- id is a right identity of _∘_.

    ∘-id : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₂ ρ̂) → ρ ∘ id₁ ≅-⇨ ρ
    ∘-id ρ = extensionality P.refl λ x → begin
        [ x /∋ ρ ∘ id₁  ]  ≡⟨ /∋-∘ x ρ id₁ ⟩
        [ x /∋ ρ /⊢ id₁ ]  ≡⟨ /⊢-id (x /∋ ρ) ⟩
        [ x /∋ ρ        ]  ∎

    -- Lifting distributes over composition.

    ∘-↑ : ∀ {Γ Δ Ε} σ {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
          (ρ₁ : Sub T₂ ρ̂₁) (ρ₂ : Sub T₁ ρ̂₂) →
          (ρ₁ ∘ ρ₂) ↑₂ σ ≅-⇨ ρ₁ ↑₂ σ ∘ ρ₂ ↑₁
    ∘-↑ σ ρ₁ ρ₂ =
      let ρ₂↑ = ρ₂ ↑₁ (σ / ρ₁)

          lemma₁ = begin
            [ wk-subst₂ (ρ₁ ∘ ρ₂)              ]  ≡⟨ P.refl ⟩
            [ map weaken₂ (map (app ρ₂) ρ₁)    ]  ≡⟨ P.sym $ map-[∘] weaken₂ (app ρ₂) ρ₁ ⟩
            [ map (weaken₂ [∘] app ρ₂) ρ₁      ]  ≡⟨ map-cong-ext₁ P.refl
                                                       (λ t → begin
                                                          [ weaken₂ · (t /⊢ ρ₂) ]  ≡⟨ P.sym $ /⊢-wk (t /⊢ ρ₂) ⟩
                                                          [ t /⊢ ρ₂ /⊢ wk₁      ]  ≡⟨ /⊢-/⊢-wk (σ / ρ₁) t ρ₂ ⟩
                                                          [ t /⊢ wk₁ /⊢ ρ₂↑     ]  ≡⟨ /⊢-cong (/⊢-wk t) P.refl ⟩
                                                          [ weaken₂ · t /⊢ ρ₂↑  ]  ∎)
                                                       (P.refl {x = [ ρ₁ ]}) ⟩
            [ map (app ρ₂↑ [∘] weaken₂) ρ₁     ]  ≡⟨ map-[∘] (app ρ₂↑) weaken₂ ρ₁ ⟩
            [ map (app ρ₂↑) (map (weaken₂) ρ₁) ]  ∎

          lemma₂ = begin
            [ var₂ · zero           ]  ≡⟨ P.sym $ trans-var zero ⟩
            [ trans · (var₁ · zero) ]  ≡⟨ trans-cong (P.sym $ Simple.zero-/∋-↑ simple₁ (σ / ρ₁) ρ₂) ⟩
            [ trans · (zero /∋ ρ₂↑) ]  ≡⟨ P.sym $ var-/⊢ zero ρ₂↑ ⟩
            [ var₂ · zero /⊢ ρ₂↑    ]  ∎

      in begin
      [ (ρ₁ ∘ ρ₂) ↑₂                                                  ]  ≡⟨ Simple.unfold-↑ simple₂ (ρ₁ ∘ ρ₂) ⟩
      [ wk-subst₂ (ρ₁ ∘ ρ₂) ▻ var₂ · zero                             ]  ≡⟨ ▻⇨-cong P.refl lemma₁ lemma₂ ⟩
      [ map (app ρ₂↑) (map weaken₂[ σ / ρ₁ ] ρ₁) ▻ var₂ · zero /⊢ ρ₂↑ ]  ≡⟨ P.sym $
                                                                              map-▻ (app ρ₂↑) (wk-subst₂[ σ / ρ₁ ] ρ₁) (var₂ · zero) ⟩
      [ map (app ρ₂↑) (wk-subst₂[ σ / ρ₁ ] ρ₁ ▻ var₂ · zero)          ]  ≡⟨ map-cong (app ρ₂↑ ∎-⟶)
                                                                                (P.sym $ Simple.unfold-↑ simple₂ ρ₁) ⟩
      [ map (app ρ₂↑) (ρ₁ ↑₂)                                         ]  ≡⟨ P.refl ⟩
      [ ρ₁ ↑₂ ∘ ρ₂ ↑₁                                                 ]  ∎

    -- N-ary lifting distributes over composition.

    ∘-↑⁺ : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
           (ρ₁ : Sub T₂ ρ̂₁) (ρ₂ : Sub T₁ ρ̂₂) Γ⁺ →
           (ρ₁ ∘ ρ₂) ↑⁺₂ Γ⁺ ≅-⇨ ρ₁ ↑⁺₂ Γ⁺ ∘ ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁)
    ∘-↑⁺ ρ₁ ρ₂ ε        = P.refl
    ∘-↑⁺ ρ₁ ρ₂ (Γ⁺ ▻ σ) = begin
      [ ((ρ₁ ∘ ρ₂) ↑⁺₂ Γ⁺) ↑₂                   ]  ≡⟨ Simple.↑-cong simple₂ (∘-↑⁺ ρ₁ ρ₂ Γ⁺) P.refl ⟩
      [ (ρ₁ ↑⁺₂ Γ⁺ ∘ ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁)) ↑₂      ]  ≡⟨ ∘-↑ σ (ρ₁ ↑⁺₂ Γ⁺) (ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁)) ⟩
      [ (ρ₁ ↑⁺₂ Γ⁺) ↑₂ ∘ (ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁)) ↑₁ ]  ∎

    ∘-↑₊ : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
           (ρ₁ : Sub T₂ ρ̂₁) (ρ₂ : Sub T₁ ρ̂₂) Γ₊ →
           (ρ₁ ∘ ρ₂) ↑₊₂ Γ₊ ≅-⇨ ρ₁ ↑₊₂ Γ₊ ∘ ρ₂ ↑₊₁ (Γ₊ /₊ ρ₁)
    ∘-↑₊ ρ₁ ρ₂ ε        = P.refl
    ∘-↑₊ ρ₁ ρ₂ (σ ◅ Γ₊) = begin
      [ (ρ₁             ∘ ρ₂   ) ↑₂ σ ↑₊₂ Γ₊      ]  ≡⟨ Simple.↑₊-cong simple₂ (∘-↑ σ ρ₁ ρ₂) (P.refl {x = [ Γ₊ ]}) ⟩
      [ (ρ₁ ↑₂ σ        ∘ ρ₂ ↑₁)      ↑₊₂ Γ₊      ]  ≡⟨ ∘-↑₊ (ρ₁ ↑₂ σ) (ρ₂ ↑₁) Γ₊ ⟩
      [ ρ₁ ↑₊₂ (σ ◅ Γ₊) ∘ ρ₂ ↑₊₁ ((σ ◅ Γ₊) /₊ ρ₁) ]  ∎

    -- First weakening and then substituting something for the first
    -- variable is equivalent to doing nothing.

    /⊢-wk-/⊢-sub : ∀ {Γ σ τ} (t : Γ ⊢₂ τ) (t′ : Γ ⊢₁ σ) →
                   t /⊢ wk₁ /⊢ sub₁ t′ ≅-⊢₂ t
    /⊢-wk-/⊢-sub t t′ = var-/⊢⋆-⇒-/⊢⋆ (ε ▻ wk₁ ▻ sub₁ t′) ε (λ x → begin
      [ var₂ · x /⊢ wk₁ /⊢ sub₁ t′ ]  ≡⟨ /⊢-cong (/∋-≅-⊢-var x wk₁ (Simple./∋-wk simple₁ x)) P.refl ⟩
      [ var₂ · suc x /⊢ sub₁ t′    ]  ≡⟨ suc-/⊢-sub x t′ ⟩
      [ var₂ · x                   ]  ∎) t

    -- Weakening a substitution and composing with sub is the same as
    -- doing nothing.

    wk-subst-∘-sub : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₂ ρ̂) (t : Δ ⊢₁ σ) →
                     wk-subst₂ ρ ∘ sub₁ t ≅-⇨ ρ
    wk-subst-∘-sub ρ t = extensionality P.refl λ x →
      let lemma = begin
            [ x /∋ wk-subst₂ ρ   ]  ≡⟨ Simple./∋-wk-subst simple₂ x ρ ⟩
            [ weaken₂ · (x /∋ ρ) ]  ≡⟨ P.sym $ /⊢-wk (x /∋ ρ) ⟩
            [ x /∋ ρ /⊢ wk₁      ]  ∎
      in begin
        [ x /∋ wk-subst₂ ρ ∘ sub₁ t    ]  ≡⟨ /∋-∘ x (wk-subst₂ ρ) (sub₁ t) ⟩
        [ x /∋ wk-subst₂ ρ /⊢ sub₁ t   ]  ≡⟨ /⊢-cong lemma P.refl ⟩
        [ x /∋ ρ /⊢ wk₁ /⊢ sub₁ t      ]  ≡⟨ /⊢-wk-/⊢-sub (x /∋ ρ) t ⟩
        [ x /∋ ρ                       ]  ∎

    -- Unfolding lemma for wk⁺.

    wk⁺-▻ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) {σ} →
            wk⁺₂ (Γ⁺ ▻ σ) ≅-⇨ wk⁺₂ Γ⁺ ∘ wk₁[ σ ]
    wk⁺-▻ Γ⁺ {σ = σ} = begin
      [ wk⁺₂ (Γ⁺ ▻ σ)       ]  ≡⟨ P.refl ⟩
      [ wk-subst₂ (wk⁺₂ Γ⁺) ]  ≡⟨ P.sym $ ∘-wk (wk⁺₂ Γ⁺) ⟩
      [ wk⁺₂ Γ⁺ ∘ wk₁       ]  ∎

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
------------------------------------------------------------------------
-- Convenient syntax for relational reasoning using transitive
-- relations
------------------------------------------------------------------------

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

module Relation.Binary.TransReasoning where

open import Level using (suc; _⊔_)
open import Data.Context using (Ctx)
open import Data.Fin.Substitution.Typed using (Typing)
open import Data.Fin.Substitution.TypedRelation using (TypedRel)
open import Data.Nat using (ℕ)
open import Data.Product using (_,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_; subst)
open import Relation.Binary
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Transitive relations that are not necessarily reflexive
--
-- Following the convention used in the standard library, we define
-- transitive binary relations using a pair of records (see
-- Relation.Binary).

record IsTransRel {a ℓ₁ ℓ₂} {A : Set a}
                  (_≈_ : Rel A ℓ₁) -- The underlying equality.
                  (_∼_ : Rel A ℓ₂) -- The relation.
                  : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence _≈_
    trans         : Transitive _∼_

    -- _∼_ respects the underlying equality _≈_.
    --
    -- (This always true for preorders, but not necessarily for
    -- irreflexive relations.)
    ∼-resp-≈      : _∼_ Respects₂ _≈_

  module Eq = IsEquivalence isEquivalence

record TransRel c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _∼_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
    _∼_        : Rel Carrier ℓ₂  -- The relation.
    isTransRel : IsTransRel _≈_ _∼_

  open IsTransRel isTransRel public

-- Sanity check: every pre-order is a transitive relation in the above
-- sense...
preorderIsTransRel : ∀ {c ℓ₁ ℓ₂} → Preorder c ℓ₁ ℓ₂ → TransRel c ℓ₁ ℓ₂
preorderIsTransRel P = record
 { isTransRel = record
   { isEquivalence = isEquivalence
   ; trans         = trans
   ; ∼-resp-≈      = ∼-resp-≈
   }
 }
 where open IsPreorder (Preorder.isPreorder P)

-- ... and so is every strict partial order.
strictPartialOrderIsTransRel : ∀ {c ℓ₁ ℓ₂} →
                               StrictPartialOrder c ℓ₁ ℓ₂ → TransRel c ℓ₁ ℓ₂
strictPartialOrderIsTransRel SPO = record
 { isTransRel = record
   { isEquivalence = isEquivalence
   ; trans         = trans
   ; ∼-resp-≈      = <-resp-≈
   }
 }
 where open IsStrictPartialOrder (StrictPartialOrder.isStrictPartialOrder SPO)

-- A form of relational reasoning for transitive relations.
--
-- The structure of this module is adapted from the
-- Relation.Binary.PreorderReasoning module of the standard library.
-- It differs from the latter in that
--
--  1. it allows reasoning about relations that are transitive but not
--     reflexive, and
--
--  2. the _IsRelatedTo_ predicate is extended with an additional
--     index that tracks whether elements of the carrier are actually
--     related in the transitive relation _∼_ or just in the
--     underlying equality _≈_.
--
-- Proofs that elements x, y are related as (x IsRelatedTo y In rel)
-- can be converted back to proofs that x ∼ y using begin_, whereas
-- proofs of (x IsRelatedTo y In eq) are too weak to do so.  Since the
-- relation _∼_ is not assumed to be reflexive (i.e. not necessarily a
-- preorder) _∎ can only construct proofs of the weaker form (x ∎ : x
-- IsRelatedTo x In eq).  Consequently, at least one use of _∼⟨_⟩_ is
-- necessary to conclude a proof.

module TransRelReasoning {c ℓ₁ ℓ₂} (R : TransRel c ℓ₁ ℓ₂) where

  open TransRel R

  infix  4 _IsRelatedTo_In_
  infix  3 _∎
  infixr 2 _∼⟨_⟩_ _≈⟨_⟩_ _≈⟨⟩_
  infix  1 begin_

  -- Codes for the relation _∼_ and the underlying equality _≈_.
  data RelC : Set where
    rel eq : RelC

  -- A generic relation combining _∼_ and equality.
  data _IsRelatedTo_In_ (x y : Carrier) : RelC → Set (ℓ₁ ⊔ ℓ₂) where
    relTo : (x∼y : x ∼ y) → x IsRelatedTo y In rel
    eqTo  : (x≈y : x ≈ y) → x IsRelatedTo y In eq

  begin_ : ∀ {x y} → x IsRelatedTo y In rel → x ∼ y
  begin (relTo x∼y) = x∼y

  _∼⟨_⟩_ : ∀ x {y z c} → x ∼ y → y IsRelatedTo z In c → x IsRelatedTo z In rel
  _ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)
  _ ∼⟨ x∼y ⟩ eqTo  y≈z = relTo (proj₁ ∼-resp-≈ y≈z x∼y)

  _≈⟨_⟩_ : ∀ x {y z c} → x ≈ y → y IsRelatedTo z In c → x IsRelatedTo z In c
  x ≈⟨ x≈y ⟩ relTo y∼z = relTo (proj₂ ∼-resp-≈ (Eq.sym x≈y) y∼z)
  x ≈⟨ x≈y ⟩ eqTo  y≈z = eqTo (Eq.trans x≈y y≈z)

  _≈⟨⟩_ : ∀ x {y c} → x IsRelatedTo y In c → x IsRelatedTo y In c
  _ ≈⟨⟩ rt-x∼y = rt-x∼y

  _∎ : ∀ x → x IsRelatedTo x In eq
  _ ∎ = eqTo Eq.refl

------------------------------------------------------------------------
-- FIXME: the following should go into a different module (probably
-- into Data.Fin.Substitution.{Typed,TypedRel})

-- A form of pre-order reasoning for transitive relations in a context.
record TransCtxTermRelReasoning {t₁ t₂ ℓ} {T₁ : Pred ℕ t₁} {T₂ : Pred ℕ t₂}
                                (_⊢_∼_ : Typing T₁ T₂ T₂ ℓ)
                                : Set (t₁ ⊔ t₂ ⊔ ℓ) where

  -- Transitivity of _⊢_∼_ for a given context.
  field ∼-trans : ∀ {n} {Γ : Ctx T₁ n} → Transitive (Γ ⊢_∼_)

  module _ {n} {Γ : Ctx T₁ n} where

    ∼-transRel : TransRel _ _ _
    ∼-transRel = record
      { Carrier = T₂ n
      ; _≈_     = _≡_
      ; _∼_     = Γ ⊢_∼_
      ; isTransRel = record
        { isEquivalence = P.isEquivalence
        ; trans         = ∼-trans
        ; ∼-resp-≈      = subst (Γ ⊢ _ ∼_) , subst (Γ ⊢_∼ _)
        }
      }
    open TransRelReasoning ∼-transRel public
      renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _≈⟨⟩_ to _≡⟨⟩_)

-- A form of pre-order reasoning for typed transitive relations.
record TypedTransRelReasoning {t₁ t₂ t₃ ℓ} {T₁ : Pred ℕ t₁}
                              {T₂ : Pred ℕ t₂} {T₃ : Pred ℕ t₃}
                              (_⊢_∼_∈_ : TypedRel T₁ T₂ T₂ T₃ ℓ)
                              : Set (t₁ ⊔ t₂ ⊔ t₃ ⊔ ℓ) where

  -- Transitivity of _⊢_∼_∈_ for a given context and T₃-"type".
  field ∼-trans : ∀ {n} {Γ : Ctx T₁ n} {t} → Transitive (Γ ⊢_∼_∈ t)

  module _ {n} {Γ : Ctx T₁ n} {t : T₃ n} where

    ∼-transRel : TransRel _ _ _
    ∼-transRel = record
      { Carrier = T₂ n
      ; _≈_     = _≡_
      ; _∼_     = Γ ⊢_∼_∈ t
      ; isTransRel = record
        { isEquivalence = P.isEquivalence
        ; trans         = ∼-trans
        ; ∼-resp-≈      = subst (Γ ⊢ _ ∼_∈ _) , subst (Γ ⊢_∼ _ ∈ _)
        }
      }
    open TransRelReasoning ∼-transRel public
      renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _≈⟨⟩_ to _≡⟨⟩_)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
open import Relation.Binary using (Preorder)
open import Relation.Binary.PropositionalEquality
open import Level

module Category.Monad.Monotone.State {ℓ}(pre : Preorder ℓ ℓ ℓ)(H : Preorder.Carrier pre → Set ℓ) where

open Preorder pre renaming (Carrier to I; _∼_ to _≤_; refl to ≤-refl; trans to ≤-trans)

open import Data.Unit using (⊤; tt)
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Unary.Monotone pre
open import Data.Product
open import Data.List.All
open import Category.Monad
open import Category.Monad.Monotone pre
open import Category.Monad.Identity

MST : (Set ℓ → Set ℓ) → Pt I ℓ
MST M P = H ⇒ (λ i → M (∃ λ j → i ≤ j × H j × P j))

MSt : Pt I ℓ
MSt = MST Identity

record StateMonad (M : Pt I ℓ) : Set (suc ℓ) where
  field
    runState : ∀ {P} → (H ↗ H ∩ P) ⊆ M P

  get : ∀ {i} → M H i
  get = runState λ _ μ → μ , μ

module _ {M}⦃ Mon : RawMonad {ℓ} M ⦄ where
  private module M = RawMonad Mon

  instance
    open RawMPMonad hiding (_>>=_; ts)
    mst-monad : RawMPMonad (MST M)
    return mst-monad px μ = M.return (_ , ≤-refl , μ , px)
    _≥=_ mst-monad c f  μ = c μ M.>>= λ where
      (i₁ , ext₁ , μ₁ , pv) → (f ext₁ pv μ₁) M.>>= λ where
        (i₂ , ext₂ , μ₂ , pw) → M.return (i₂ , ≤-trans ext₁ ext₂ , μ₂ , pw)

    open StateMonad
    mst-monad-ops : StateMonad (MST M)
    runState (mst-monad-ops) f μ = let μ' , p = f ≤-refl μ in M.return (_ , ≤-refl , μ' , p)


text:
data Bool : Set where
  true : Bool
  false : Bool

record Eq (t : Set) : Set where
   field _==_ : t → t → Bool

open Eq {{...}}

-- Now package this into a record type for "sets with boolean equality":
record EqSet : Set₁ where
  field
    set : Set
    instance eq : Eq set

open EqSet

equality : {{A : EqSet}} (x y : set A) → Bool
equality x y = x == y

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-

Constant structure: _ ↦ A

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Relational.Constant where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.HITs.PropositionalTruncation
open import Cubical.HITs.SetQuotients

open import Cubical.Structures.Constant

private
  variable
    ℓ ℓ' : Level

-- Structured relations

module _ (A : hSet ℓ') where

  ConstantRelStr : StrRel {ℓ = ℓ} (ConstantStructure (A .fst)) ℓ'
  ConstantRelStr _ a₀ a₁ = a₀ ≡ a₁

  constantSuitableRel : SuitableStrRel {ℓ = ℓ} (ConstantStructure (A .fst)) ConstantRelStr
  constantSuitableRel .quo _ _ _ = isContrSingl _
  constantSuitableRel .symmetric _ = sym
  constantSuitableRel .transitive _ _ = _∙_
  constantSuitableRel .set _ = A .snd
  constantSuitableRel .prop _ = A .snd

  constantRelMatchesEquiv : StrRelMatchesEquiv {ℓ = ℓ} ConstantRelStr (ConstantEquivStr (A .fst))
  constantRelMatchesEquiv _ _ _ = idEquiv _

  constantRelAction : StrRelAction {ℓ = ℓ} ConstantRelStr
  constantRelAction .actStr _ a = a
  constantRelAction .actStrId _ = refl
  constantRelAction .actRel _ a a' p = p

  constantPositiveRel : PositiveStrRel {ℓ = ℓ} constantSuitableRel
  constantPositiveRel .act = constantRelAction
  constantPositiveRel .reflexive a = refl
  constantPositiveRel .detransitive R R' p = ∣ _ , p , refl ∣
  constantPositiveRel .quo R = isoToIsEquiv isom
    where
    open Iso
    isom : Iso _ _
    isom .fun = _
    isom .inv = [_]
    isom .rightInv _ = refl
    isom .leftInv = elimProp (λ _ → squash/ _ _) (λ a → refl)

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:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 12-univalence where

import 11-function-extensionality
open 11-function-extensionality public

-- Section 10.1 Type extensionality

equiv-eq : {i : Level} {A : UU i} {B : UU i} → Id A B → A ≃ B
equiv-eq {A = A} refl = pair id (is-equiv-id A)

UNIVALENCE : {i : Level} (A B : UU i) → UU (lsuc i)
UNIVALENCE A B = is-equiv (equiv-eq {A = A} {B = B})

is-contr-total-equiv-UNIVALENCE : {i : Level} (A : UU i) →
  ((B : UU i) → UNIVALENCE A B) → is-contr (Σ (UU i) (λ X → A ≃ X))
is-contr-total-equiv-UNIVALENCE A UA =
  fundamental-theorem-id' A
    ( pair id (is-equiv-id A))
    ( λ B → equiv-eq {B = B})
    ( UA)

UNIVALENCE-is-contr-total-equiv : {i : Level} (A : UU i) →
  is-contr (Σ (UU i) (λ X → A ≃ X)) → (B : UU i) → UNIVALENCE A B
UNIVALENCE-is-contr-total-equiv A c =
  fundamental-theorem-id A
    ( pair id (is-equiv-id A))
    ( c)
    ( λ B → equiv-eq {B = B})

ev-id : {i j : Level} {A : UU i} (P : (B : UU i) → (A ≃ B) → UU j) →
  ((B : UU i) (e : A ≃ B) → P B e) → P A (pair id (is-equiv-id A))
ev-id {A = A} P f = f A (pair id (is-equiv-id A))

IND-EQUIV : {i j : Level} {A : UU i} → ((B : UU i) (e : A ≃ B) → UU j) → UU _
IND-EQUIV P = sec (ev-id P)

triangle-ev-id : {i j : Level} {A : UU i}
  (P : (Σ (UU i) (λ X → A ≃ X)) → UU j) →
  (ev-pt (Σ (UU i) (λ X → A ≃ X)) (pair A (pair id (is-equiv-id A))) P)
  ~ ((ev-id (λ X e → P (pair X e))) ∘ (ev-pair {A = UU i} {B = λ X → A ≃ X} {C = P}))
triangle-ev-id P f = refl

abstract
  IND-EQUIV-is-contr-total-equiv : {i j : Level} (A : UU i) →
    is-contr (Σ (UU i) (λ X → A ≃ X)) →
    (P : (Σ (UU i) (λ X → A ≃ X)) → UU j) → IND-EQUIV (λ B e → P (pair B e))
  IND-EQUIV-is-contr-total-equiv {i} {j} A c P =
    section-comp
      ( ev-pt (Σ (UU i) (λ X → A ≃ X)) (pair A (pair id (is-equiv-id A))) P)
      ( ev-id (λ X e → P (pair X e)))
      ( ev-pair {A = UU i} {B = λ X → A ≃ X} {C = P})
      ( triangle-ev-id P)
      ( sec-ev-pair (UU i) (λ X → A ≃ X) P)
      ( is-sing-is-contr (Σ (UU i) (λ X → A ≃ X))
        ( pair
          ( pair A (pair id (is-equiv-id A)))
          ( λ t →
            ( inv (contraction c (pair A (pair id (is-equiv-id A))))) ∙
            ( contraction c t)))
        ( P)
        ( pair A (equiv-id A)))

abstract
  is-contr-total-equiv-IND-EQUIV : {i : Level} (A : UU i) →
    ( {j : Level} (P : (Σ (UU i) (λ X → A ≃ X)) → UU j) →
      IND-EQUIV (λ B e → P (pair B e))) →
    is-contr (Σ (UU i) (λ X → A ≃ X))
  is-contr-total-equiv-IND-EQUIV {i} A ind =
    is-contr-is-sing
      ( Σ (UU i) (λ X → A ≃ X))
      ( pair A (pair id (is-equiv-id A)))
      ( λ P → section-comp'
        ( ev-pt (Σ (UU i) (λ X → A ≃ X)) (pair A (pair id (is-equiv-id A))) P)
        ( ev-id (λ X e → P (pair X e)))
        ( ev-pair {A = UU i} {B = λ X → A ≃ X} {C = P})
        ( triangle-ev-id P)
        ( sec-ev-pair (UU i) (λ X → A ≃ X) P)
        ( ind P))

-- The univalence axiom

postulate univalence : {i : Level} (A B : UU i) → UNIVALENCE A B

eq-equiv : {i : Level} (A B : UU i) → (A ≃ B) → Id A B
eq-equiv A B = inv-is-equiv (univalence A B)

abstract
  is-contr-total-equiv : {i : Level} (A : UU i) →
    is-contr (Σ (UU i) (λ X → A ≃ X))
  is-contr-total-equiv A = is-contr-total-equiv-UNIVALENCE A (univalence A)

abstract
  Ind-equiv : {i j : Level} (A : UU i) (P : (B : UU i) (e : A ≃ B) → UU j) →
    sec (ev-id P)
  Ind-equiv A P =
    IND-EQUIV-is-contr-total-equiv A
    ( is-contr-total-equiv A)
    ( λ t → P (pr1 t) (pr2 t))

ind-equiv : {i j : Level} (A : UU i) (P : (B : UU i) (e : A ≃ B) → UU j) →
  P A (pair id (is-equiv-id A)) → {B : UU i} (e : A ≃ B) → P B e
ind-equiv A P p {B} = pr1 (Ind-equiv A P) p B

-- Subuniverses

is-subuniverse :
  {l1 l2 : Level} (P : UU l1 → UU l2) → UU ((lsuc l1) ⊔ l2)
is-subuniverse P = is-subtype P

subuniverse :
  (l1 l2 : Level) → UU ((lsuc l1) ⊔ (lsuc l2))
subuniverse l1 l2 = Σ (UU l1 → UU l2) is-subuniverse

{- By univalence, subuniverses are closed under equivalences. -}
in-subuniverse-equiv :
  {l1 l2 : Level} (P : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → P X → P Y
in-subuniverse-equiv P e = tr P (eq-equiv _ _ e)

in-subuniverse-equiv' :
  {l1 l2 : Level} (P : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → P Y → P X
in-subuniverse-equiv' P e = tr P (inv (eq-equiv _ _ e))

total-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) → UU ((lsuc l1) ⊔ l2)
total-subuniverse {l1} P = Σ (UU l1) (pr1 P)

{- We also introduce the notion of 'global subuniverse'. The handling of
   universe levels is a bit more complicated here, since (l : Level) → A l are
   kinds but not types. -}

is-global-subuniverse :
  (α : Level → Level) (P : (l : Level) → subuniverse l (α l)) →
  (l1 l2 : Level) → UU _
is-global-subuniverse α P l1 l2 =
  (X : UU l1) (Y : UU l2) → X ≃ Y → (pr1 (P l1)) X → (pr1 (P l2)) Y

{- Next we characterize the identity type of a subuniverse. -}

Eq-total-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) →
  (s t : total-subuniverse P) → UU l1
Eq-total-subuniverse (pair P H) (pair X p) t = X ≃ (pr1 t)

Eq-total-subuniverse-eq :
  {l1 l2 : Level} (P : subuniverse l1 l2) →
  (s t : total-subuniverse P) → Id s t → Eq-total-subuniverse P s t
Eq-total-subuniverse-eq (pair P H) (pair X p) .(pair X p) refl = equiv-id X

abstract
  is-contr-total-Eq-total-subuniverse :
    {l1 l2 : Level} (P : subuniverse l1 l2)
    (s : total-subuniverse P) →
    is-contr (Σ (total-subuniverse P) (λ t → Eq-total-subuniverse P s t))
  is-contr-total-Eq-total-subuniverse (pair P H) (pair X p) =
    is-contr-total-Eq-substructure (is-contr-total-equiv X) H X (equiv-id X) p

abstract
  is-equiv-Eq-total-subuniverse-eq :
    {l1 l2 : Level} (P : subuniverse l1 l2)
    (s t : total-subuniverse P) → is-equiv (Eq-total-subuniverse-eq P s t)
  is-equiv-Eq-total-subuniverse-eq (pair P H) (pair X p) =
    fundamental-theorem-id
      ( pair X p)
      ( equiv-id X)
      ( is-contr-total-Eq-total-subuniverse (pair P H) (pair X p))
      ( Eq-total-subuniverse-eq (pair P H) (pair X p))

eq-Eq-total-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) →
  {s t : total-subuniverse P} → Eq-total-subuniverse P s t → Id s t
eq-Eq-total-subuniverse P {s} {t} =
  inv-is-equiv (is-equiv-Eq-total-subuniverse-eq P s t)

-- Section 12.2 Univalence implies function extensionality

is-equiv-postcomp-univalence :
  {l1 l2 : Level} {X Y : UU l1} (A : UU l2) (e : X ≃ Y) →
  is-equiv (postcomp A (map-equiv e))
is-equiv-postcomp-univalence {X = X} A =
  ind-equiv X
    ( λ Y e → is-equiv (postcomp A (map-equiv e)))
    ( is-equiv-id (A → X))

weak-funext-univalence :
  {l : Level} {A : UU l} {B : A → UU l} → WEAK-FUNEXT A B
weak-funext-univalence {A = A} {B} is-contr-B =
  is-contr-retract-of
    ( fib (postcomp A (pr1 {B = B})) id)
    ( pair
      ( λ f → pair (λ x → pair x (f x)) refl)
      ( pair
        ( λ h x → tr B (htpy-eq (pr2 h) x) (pr2 (pr1 h x)))
        ( htpy-refl)))
    ( is-contr-map-is-equiv
      ( is-equiv-postcomp-univalence A (equiv-pr1 is-contr-B))
      ( id))

funext-univalence :
  {l : Level} {A : UU l} {B : A → UU l} (f : (x : A) → B x) → FUNEXT f
funext-univalence {A = A} {B} f =
  FUNEXT-WEAK-FUNEXT (λ A B → weak-funext-univalence) A B f

-- Section 12.3 Groups in univalent mathematics

{- We first introduce semi-groups, and then groups. We do this because the
   category of groups is a full subcategory of the category of semi-groups.
   In particular, it is a proposition for a semi-group to be a group. Therefore
   this approach gives us in a straightforward way that equality of groups is
   equality of semi-groups. This will be useful in showing that group
   isomorphisms are equivalent to identifications of groups. -}

has-associative-mul :
  {l : Level} (X : UU-Set l) → UU l
has-associative-mul X =
  Σ ( ( type-Set X) →
      ( ( type-Set X) → (type-Set X))) (λ μ →
    ( x y z : type-Set X) → Id (μ (μ x y) z) (μ x (μ y z)))

Semi-Group :
  (l : Level) → UU (lsuc l)
Semi-Group l = Σ (UU-Set l) has-associative-mul

{- Bureaucracy of semi-groups. -}

set-Semi-Group :
  {l : Level} → Semi-Group l → UU-Set l
set-Semi-Group G = pr1 G

type-Semi-Group :
  {l : Level} → Semi-Group l → UU l
type-Semi-Group G = pr1 (set-Semi-Group G)

is-set-type-Semi-Group :
  {l : Level} (G : Semi-Group l) → is-set (type-Semi-Group G)
is-set-type-Semi-Group G = pr2 (set-Semi-Group G)

associative-mul-Semi-Group :
  {l : Level} (G : Semi-Group l) →
  has-associative-mul (set-Semi-Group G)
associative-mul-Semi-Group G = pr2 G

mul-Semi-Group :
  {l : Level} (G : Semi-Group l) →
  type-Semi-Group G →
    type-Semi-Group G → type-Semi-Group G
mul-Semi-Group G = pr1 (associative-mul-Semi-Group G)

is-associative-mul-Semi-Group :
  {l : Level} (G : Semi-Group l) (x y z : type-Semi-Group G) →
  Id ( mul-Semi-Group G (mul-Semi-Group G x y) z)
     ( mul-Semi-Group G x (mul-Semi-Group G y z))
is-associative-mul-Semi-Group G = pr2 (associative-mul-Semi-Group G)

{- The property that a semi-group is a monoid is just that the semi-group
   possesses a unit that satisfies the left and right unit laws. -}

is-unital :
  {l : Level} → Semi-Group l → UU l
is-unital G =
  Σ ( type-Semi-Group G)
    ( λ e →
      ( (y : type-Semi-Group G) → Id (mul-Semi-Group G e y) y) ×
      ( (x : type-Semi-Group G) → Id (mul-Semi-Group G x e) x))

{- We show that is-unital is a proposition. -}

abstract
  is-prop-is-unital' :
    {l : Level} (G : Semi-Group l) → is-prop' (is-unital G)
  is-prop-is-unital' (pair (pair X is-set-X) (pair μ assoc-μ))
    (pair e (pair left-unit-e right-unit-e))
    (pair e' (pair left-unit-e' right-unit-e')) =
    eq-subtype
      ( λ e → is-prop-prod
        ( is-prop-Π (λ y → is-set-X (μ e y) y))
        ( is-prop-Π (λ x → is-set-X (μ x e) x)))
      ( (inv (left-unit-e' e)) ∙ (right-unit-e e'))

abstract
  is-prop-is-unital :
    {l : Level} (G : Semi-Group l) → is-prop (is-unital G)
  is-prop-is-unital G = is-prop-is-prop' (is-prop-is-unital' G)

{- The property that a monoid is a group is just the property that the monoid
   that every element is invertible, i.e., it comes equipped with an inverse
   operation that satisfies the left and right inverse laws. -}

is-group' :
  {l : Level} (G : Semi-Group l) → is-unital G → UU l
is-group' G is-unital-G =
  Σ ( type-Semi-Group G → type-Semi-Group G)
    ( λ i →
      ( (x : type-Semi-Group G) →
        Id (mul-Semi-Group G (i x) x) (pr1 is-unital-G)) ×
      ( (x : type-Semi-Group G) →
        Id (mul-Semi-Group G x (i x)) (pr1 is-unital-G)))

is-group :
  {l : Level} (G : Semi-Group l) → UU l
is-group G =
  Σ (is-unital G) (is-group' G)

Group :
  (l : Level) → UU (lsuc l)
Group l = Σ (Semi-Group l) is-group

{- Some bureaucracy of Groups. -}

semi-group-Group :
  {l : Level} → Group l → Semi-Group l
semi-group-Group G = pr1 G

set-Group :
  {l : Level} → Group l → UU-Set l
set-Group G = pr1 (semi-group-Group G)

type-Group :
  {l : Level} → Group l → UU l
type-Group G = pr1 (set-Group G)

is-set-type-Group :
  {l : Level} (G : Group l) → is-set (type-Group G)
is-set-type-Group G = pr2 (set-Group G)

associative-mul-Group :
  {l : Level} (G : Group l) → has-associative-mul (set-Group G)
associative-mul-Group G = pr2 (semi-group-Group G)

mul-Group :
  {l : Level} (G : Group l) →
  type-Group G → type-Group G → type-Group G
mul-Group G = pr1 (associative-mul-Group G)

is-associative-mul-Group :
  {l : Level} (G : Group l) (x y z : type-Group G) →
  Id (mul-Group G (mul-Group G x y) z) (mul-Group G x (mul-Group G y z))
is-associative-mul-Group G = pr2 (associative-mul-Group G)

is-group-Group :
  {l : Level} (G : Group l) → is-group (semi-group-Group G)
is-group-Group G = pr2 G

is-unital-Group :
  {l : Level} (G : Group l) → is-unital (semi-group-Group G)
is-unital-Group G = pr1 (is-group-Group G)

unit-Group :
  {l : Level} (G : Group l) → type-Group G
unit-Group G = pr1 (is-unital-Group G)

left-unit-law-Group :
  {l : Level} (G : Group l) (x : type-Group G) →
  Id (mul-Group G (unit-Group G) x) x
left-unit-law-Group G = pr1 (pr2 (is-unital-Group G))

right-unit-law-Group :
  {l : Level} (G : Group l) (x : type-Group G) →
  Id (mul-Group G x (unit-Group G)) x
right-unit-law-Group G = pr2 (pr2 (is-unital-Group G))

has-inverses-Group :
  {l : Level} (G : Group l) →
  is-group' (semi-group-Group G) (is-unital-Group G)
has-inverses-Group G = pr2 (is-group-Group G)

inv-Group :
  {l : Level} (G : Group l) →
  type-Group G → type-Group G
inv-Group G = pr1 (has-inverses-Group G)

left-inverse-law-Group :
  {l : Level} (G : Group l) (x : type-Group G) →
  Id (mul-Group G (inv-Group G x) x) (unit-Group G)
left-inverse-law-Group G = pr1 (pr2 (has-inverses-Group G))

right-inverse-law-Group :
  {l : Level} (G : Group l) (x : type-Group G) →
  Id (mul-Group G x (inv-Group G x)) (unit-Group G)
right-inverse-law-Group G = pr2 (pr2 (has-inverses-Group G))

{- We show that being a group is a proposition. -}

abstract
  is-prop-is-group' :
    {l : Level} (G : Semi-Group l) (e : is-unital G) → is-prop' (is-group' G e)
  is-prop-is-group'
    ( pair (pair G is-set-G) (pair μ assoc-G))
    ( pair e (pair left-unit-G right-unit-G))
    ( pair i (pair left-inv-i right-inv-i))
    ( pair i' (pair left-inv-i' right-inv-i')) =
    eq-subtype
      ( λ i →
        is-prop-prod
          ( is-prop-Π (λ x → is-set-G (μ (i x) x) e))
          ( is-prop-Π (λ x → is-set-G (μ x (i x)) e)))
      ( eq-htpy
        ( λ x →                                             -- ix
          ( inv (left-unit-G (i x))) ∙                      -- = 1·(ix)
          ( ( ap (λ y → μ y (i x)) (inv (left-inv-i' x))) ∙ -- = (i'x·x)·(ix)
            ( ( assoc-G (i' x) x (i x)) ∙                   -- = (i'x)·(x·i'x)
              ( ( ap (μ (i' x)) (right-inv-i x)) ∙          -- = (i'x)·1
                ( right-unit-G (i' x)))))))                 -- = i'x

abstract
  is-prop-is-group :
    {l : Level} (G : Semi-Group l) → is-prop (is-group G)
  is-prop-is-group G =
    is-prop-Σ
      ( is-prop-is-unital G)
      ( λ e → is-prop-is-prop' (is-prop-is-group' G e))

{- We give two examples of groups. The first is the group ℤ of integers. The
   second is the loop space of a pointed 1-type.  -}

{- The group of integers. -}

semi-group-ℤ : Semi-Group lzero
semi-group-ℤ = pair set-ℤ (pair add-ℤ associative-add-ℤ)

group-ℤ : Group lzero
group-ℤ =
  pair
    ( semi-group-ℤ)
    ( pair
      ( pair zero-ℤ (pair left-unit-law-add-ℤ right-unit-law-add-ℤ))
      ( pair neg-ℤ (pair left-inverse-law-add-ℤ right-inverse-law-add-ℤ)))

{- The loop space of a 1-type as a group. -}

loop-space :
  {l : Level} {A : UU l} → A → UU l
loop-space a = Id a a

set-loop-space :
  {l : Level} (A : UU l) (a : A) (is-set-Ω : is-set (Id a a)) → UU-Set l
set-loop-space A a is-set-Ω = pair (Id a a) is-set-Ω

semi-group-loop-space :
  {l : Level} (A : UU l) (a : A) (is-set-Ω : is-set (Id a a)) → Semi-Group l
semi-group-loop-space A a is-set-Ω =
  pair
    ( set-loop-space A a is-set-Ω)
    ( pair (λ p q → p ∙ q) assoc)

group-loop-space :
  {l : Level} (A : UU l) (a : A) (is-set-Ω : is-set (Id a a)) → Group l
group-loop-space A a is-set-Ω =
  pair
    ( semi-group-loop-space A a is-set-Ω)
    ( pair
      ( pair refl (pair (λ q → left-unit) (λ p → right-unit)))
      ( pair inv (pair left-inv right-inv)))

set-loop-space-1-type :
  {l : Level} (A : 1-type l) (a : pr1 A) → UU-Set l
set-loop-space-1-type (pair A is-1-type-A) a =
  set-loop-space A a (is-1-type-A a a)

semi-group-loop-space-1-type :
  {l : Level} (A : 1-type l) (a : pr1 A) → Semi-Group l
semi-group-loop-space-1-type (pair A is-1-type-A) a =
  semi-group-loop-space A a (is-1-type-A a a)

group-loop-space-1-type :
  {l : Level} (A : 1-type l) (a : pr1 A) → Group l
group-loop-space-1-type (pair A is-1-type-A) a =
  group-loop-space A a (is-1-type-A a a)

{- We introduce the automorphism group on a set X. -}

aut-Set :
  {l : Level} (X : UU-Set l) → UU-Set l
aut-Set X = set-equiv X X

associative-comp-equiv :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} →
  (e : A ≃ B) (f : B ≃ C) (g : C ≃ D) →
  Id ((g ∘e f) ∘e e) (g ∘e (f ∘e e))
associative-comp-equiv e f g = eq-htpy-equiv htpy-refl

has-associative-mul-aut-Set :
  {l : Level} (X : UU-Set l) → has-associative-mul (aut-Set X)
has-associative-mul-aut-Set X =
  pair
    ( λ e f → f ∘e e)
    ( λ e f g → inv (associative-comp-equiv e f g))

aut-Semi-Group :
  {l : Level} (X : UU-Set l) → Semi-Group l
aut-Semi-Group X =
  pair
    ( aut-Set X)
    ( has-associative-mul-aut-Set X)

left-unit-law-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  Id ((equiv-id Y) ∘e e) e
left-unit-law-equiv e = eq-htpy-equiv htpy-refl

right-unit-law-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  Id (e ∘e (equiv-id X)) e
right-unit-law-equiv e = eq-htpy-equiv htpy-refl

is-unital-aut-Semi-Group :
  {l : Level} (X : UU-Set l) → is-unital (aut-Semi-Group X)
is-unital-aut-Semi-Group X =
  pair
    ( equiv-id (type-Set X))
    ( pair
      ( right-unit-law-equiv)
      ( left-unit-law-equiv))

left-inverse-law-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  Id ((inv-equiv e) ∘e e) (equiv-id X)
left-inverse-law-equiv e =
  eq-htpy-equiv (isretr-inv-is-equiv (is-equiv-map-equiv e))

right-inverse-law-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  Id (e ∘e (inv-equiv e)) (equiv-id Y)
right-inverse-law-equiv e =
  eq-htpy-equiv (issec-inv-is-equiv (is-equiv-map-equiv e))

is-group-aut-Semi-Group' :
  {l : Level} (X : UU-Set l) →
  is-group' (aut-Semi-Group X) (is-unital-aut-Semi-Group X)
is-group-aut-Semi-Group' X =
  pair
    ( inv-equiv)
    ( pair right-inverse-law-equiv left-inverse-law-equiv)

aut-Group :
  {l : Level} → UU-Set l → Group l
aut-Group X =
  pair
    ( aut-Semi-Group X)
    ( pair (is-unital-aut-Semi-Group X) (is-group-aut-Semi-Group' X))

{- Now we introduce homomorphisms of semi-groups. Group homomorphisms are just
   homomorphisms between their underlying semi-groups. -}

preserves-mul :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  (type-Semi-Group G → type-Semi-Group H) → UU (l1 ⊔ l2)
preserves-mul G H f =
  (x y : type-Semi-Group G) →
      Id (f (mul-Semi-Group G x y)) (mul-Semi-Group H (f x) (f y))

abstract
  is-prop-preserves-mul :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : type-Semi-Group G → type-Semi-Group H) →
    is-prop (preserves-mul G H f)
  is-prop-preserves-mul G (pair (pair H is-set-H) (pair μ-H assoc-H)) f =
    is-prop-Π (λ x →
      is-prop-Π (λ y →
        is-set-H (f (mul-Semi-Group G x y)) (μ-H (f x) (f y))))

hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
hom-Semi-Group G H =
  Σ ( type-Semi-Group G → type-Semi-Group H)
    ( preserves-mul G H)

{- Bureaucracy of homomorphisms of semi-groups. -}

map-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( hom-Semi-Group G H) →
  ( type-Semi-Group G) → (type-Semi-Group H)
map-hom-Semi-Group G H f = pr1 f

preserves-mul-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( f : hom-Semi-Group G H) →
  preserves-mul G H (map-hom-Semi-Group G H f)
preserves-mul-hom-Semi-Group G H f = pr2 f

{- We characterize the identity type of the semi-group homomorphisms. -}

htpy-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2)
  (f g : hom-Semi-Group G H) → UU (l1 ⊔ l2)
htpy-hom-Semi-Group G H f g =
  (map-hom-Semi-Group G H f) ~ (map-hom-Semi-Group G H g)

reflexive-htpy-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( f : hom-Semi-Group G H) → htpy-hom-Semi-Group G H f f
reflexive-htpy-hom-Semi-Group G H f = htpy-refl

htpy-hom-Semi-Group-eq :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( f g : hom-Semi-Group G H) → Id f g → htpy-hom-Semi-Group G H f g
htpy-hom-Semi-Group-eq G H f .f refl = reflexive-htpy-hom-Semi-Group G H f

abstract
  is-contr-total-htpy-hom-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) →
    is-contr (Σ (hom-Semi-Group G H) (htpy-hom-Semi-Group G H f))
  is-contr-total-htpy-hom-Semi-Group G H f =
    is-contr-total-Eq-substructure
      ( is-contr-total-htpy (map-hom-Semi-Group G H f))
      ( is-prop-preserves-mul G H)
      ( map-hom-Semi-Group G H f)
      ( htpy-refl)
      ( preserves-mul-hom-Semi-Group G H f)

abstract
  is-equiv-htpy-hom-Semi-Group-eq :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f g : hom-Semi-Group G H) → is-equiv (htpy-hom-Semi-Group-eq G H f g)
  is-equiv-htpy-hom-Semi-Group-eq G H f =
    fundamental-theorem-id f
      ( reflexive-htpy-hom-Semi-Group G H f)
      ( is-contr-total-htpy-hom-Semi-Group G H f)
      ( htpy-hom-Semi-Group-eq G H f)

eq-htpy-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  { f g : hom-Semi-Group G H} → htpy-hom-Semi-Group G H f g → Id f g
eq-htpy-hom-Semi-Group G H {f} {g} =
  inv-is-equiv (is-equiv-htpy-hom-Semi-Group-eq G H f g)

{- We show that the type of semi-group homomorphisms between two semi-groups is
   a set. -}

is-set-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  is-set (hom-Semi-Group G H)
is-set-hom-Semi-Group G H (pair f μ-f) (pair g μ-g) =
  is-prop-is-equiv
    ( htpy-hom-Semi-Group G H (pair f μ-f) (pair g μ-g))
    ( htpy-hom-Semi-Group-eq G H (pair f μ-f) (pair g μ-g))
    ( is-equiv-htpy-hom-Semi-Group-eq G H (pair f μ-f) (pair g μ-g))
    ( is-prop-Π (λ x → is-set-type-Semi-Group H (f x) (g x)))

{- We introduce group homomorphisms. -}

hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) → UU (l1 ⊔ l2)
hom-Group G H =
  hom-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)

{- Bureaucracy of group homomorphisms. -}

map-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( hom-Group G H) →
  ( type-Group G) → (type-Group H)
map-hom-Group G H f = pr1 f

preserves-mul-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f : hom-Group G H) →
  preserves-mul
    ( semi-group-Group G)
    ( semi-group-Group H)
    ( map-hom-Group G H f)
preserves-mul-hom-Group G H f = pr2 f

{- We characterize the identity type of the group homomorphisms. -}

htpy-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2)
  (f g : hom-Group G H) → UU (l1 ⊔ l2)
htpy-hom-Group G H =
  htpy-hom-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)

reflexive-htpy-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f : hom-Group G H) → htpy-hom-Group G H f f
reflexive-htpy-hom-Group G H =
  reflexive-htpy-hom-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)

htpy-hom-Group-eq :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f g : hom-Group G H) → Id f g → htpy-hom-Group G H f g
htpy-hom-Group-eq G H =
  htpy-hom-Semi-Group-eq
    ( semi-group-Group G)
    ( semi-group-Group H)

abstract
  is-contr-total-htpy-hom-Group :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f : hom-Group G H) →
    is-contr (Σ (hom-Group G H) (htpy-hom-Group G H f))
  is-contr-total-htpy-hom-Group G H =
    is-contr-total-htpy-hom-Semi-Group
      ( semi-group-Group G)
      ( semi-group-Group H)

abstract
  is-equiv-htpy-hom-Group-eq :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f g : hom-Group G H) → is-equiv (htpy-hom-Group-eq G H f g)
  is-equiv-htpy-hom-Group-eq G H =
    is-equiv-htpy-hom-Semi-Group-eq
      ( semi-group-Group G)
      ( semi-group-Group H)

eq-htpy-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  { f g : hom-Group G H} → htpy-hom-Group G H f g → Id f g
eq-htpy-hom-Group G H =
  eq-htpy-hom-Semi-Group (semi-group-Group G) (semi-group-Group H)

{- Next, we construct the identity group homomorphism, and we show that
   compositions of group homomorphisms are again group homomorphisms. -}

preserves-mul-id :
  {l : Level} (G : Semi-Group l) → preserves-mul G G id
preserves-mul-id (pair (pair G is-set-G) (pair μ-G assoc-G)) x y = refl

id-Semi-Group :
  {l : Level} (G : Semi-Group l) → hom-Semi-Group G G
id-Semi-Group G =
  pair id (preserves-mul-id G)

id-Group :
  {l : Level} (G : Group l) → hom-Group G G
id-Group G = id-Semi-Group (semi-group-Group G)

composition-Semi-Group :
  {l1 l2 l3 : Level} →
  (G : Semi-Group l1) (H : Semi-Group l2) (K : Semi-Group l3) →
  (hom-Semi-Group H K) → (hom-Semi-Group G H) → (hom-Semi-Group G K)
composition-Semi-Group G H K (pair g μ-g) (pair f μ-f) =
  pair
    ( g ∘ f)
    ( λ x y → (ap g (μ-f x y)) ∙ (μ-g (f x) (f y)))

composition-Group :
  {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (K : Group l3) →
  (hom-Group H K) → (hom-Group G H) → (hom-Group G K)
composition-Group G H K =
  composition-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)
    ( semi-group-Group K)

{- Next, we prove the that the laws for a category hold for group homomorphisms,
   i.e., we show that composition is associative and satisfies the left and
   right unit laws. Before we show that these laws hold, we will characterize
   the identity type of the types of semi-group homomorphisms and group
   homomorphisms. -}

associative-Semi-Group :
  { l1 l2 l3 l4 : Level} (G : Semi-Group l1) (H : Semi-Group l2)
  ( K : Semi-Group l3) (L : Semi-Group l4) (h : hom-Semi-Group K L) →
  ( g : hom-Semi-Group H K) (f : hom-Semi-Group G H) →
  Id ( composition-Semi-Group G H L
       ( composition-Semi-Group H K L h g) f)
     ( composition-Semi-Group G K L h
       ( composition-Semi-Group G H K g f))
associative-Semi-Group G H K L (pair h μ-h) (pair g μ-g) (pair f μ-f) =
  eq-htpy-hom-Semi-Group G L htpy-refl

left-unit-law-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2)
  ( f : hom-Semi-Group G H) →
  Id ( composition-Semi-Group G H H (id-Semi-Group H) f) f
left-unit-law-Semi-Group G
  (pair (pair H is-set-H) (pair μ-H assoc-H)) (pair f μ-f) =
  eq-htpy-hom-Semi-Group G
    ( pair (pair H is-set-H) (pair μ-H assoc-H))
    ( htpy-refl)

right-unit-law-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2)
  ( f : hom-Semi-Group G H) →
  Id ( composition-Semi-Group G G H f (id-Semi-Group G)) f
right-unit-law-Semi-Group
  (pair (pair G is-set-G) (pair μ-G assoc-G)) H (pair f μ-f) =
  eq-htpy-hom-Semi-Group
    ( pair (pair G is-set-G) (pair μ-G assoc-G)) H htpy-refl

{- Now we introduce the notion of group isomorphism. Finally, we will show that
   isomorphic groups are equal. -}

is-iso-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( f : hom-Semi-Group G H) → UU (l1 ⊔ l2)
is-iso-Semi-Group G H f =
  Σ ( hom-Semi-Group H G) (λ g →
    ( Id (composition-Semi-Group H G H f g) (id-Semi-Group H)) ×
    ( Id (composition-Semi-Group G H G g f) (id-Semi-Group G)))

iso-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
iso-Semi-Group G H =
  Σ (hom-Semi-Group G H) (is-iso-Semi-Group G H)

abstract
  is-prop-is-iso-Semi-Group' :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) → is-prop' (is-iso-Semi-Group G H f)
  is-prop-is-iso-Semi-Group' G H f
    (pair g (pair issec isretr)) (pair g' (pair issec' isretr')) =
    eq-subtype
      ( λ h →
        is-prop-prod
          ( is-set-hom-Semi-Group H H
            ( composition-Semi-Group H G H f h)
            ( id-Semi-Group H))
          ( is-set-hom-Semi-Group G G
            ( composition-Semi-Group G H G h f)
            ( id-Semi-Group G)))
      ( ( inv (left-unit-law-Semi-Group H G g)) ∙
        ( ( inv (ap (λ h → composition-Semi-Group H G G h g) isretr')) ∙
          ( ( associative-Semi-Group H G H G g' f g) ∙
            ( ( ap (composition-Semi-Group H H G g') issec) ∙
              ( right-unit-law-Semi-Group H G g')))))

abstract
  is-prop-is-iso-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) → is-prop (is-iso-Semi-Group G H f)
  is-prop-is-iso-Semi-Group G H f =
    is-prop-is-prop' (is-prop-is-iso-Semi-Group' G H f)

abstract
  preserves-mul-inv-is-equiv-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H)
    ( is-equiv-f : is-equiv (map-hom-Semi-Group G H f)) →
    preserves-mul H G (inv-is-equiv is-equiv-f)
  preserves-mul-inv-is-equiv-Semi-Group
    ( pair (pair G is-set-G) (pair μ-G assoc-G))
    ( pair (pair H is-set-H) (pair μ-H assoc-H))
    ( pair f μ-f) is-equiv-f x y =
    inv-is-equiv
      ( is-emb-is-equiv f is-equiv-f
        ( inv-is-equiv is-equiv-f (μ-H x y))
        ( μ-G (inv-is-equiv is-equiv-f x) (inv-is-equiv is-equiv-f y)))
      ( ( ( issec-inv-is-equiv is-equiv-f (μ-H x y)) ∙
          ( ( ap (λ t → μ-H t y) (inv (issec-inv-is-equiv is-equiv-f x))) ∙
            ( ap
              ( μ-H (f (inv-is-equiv is-equiv-f x)))
              ( inv (issec-inv-is-equiv is-equiv-f y))))) ∙
        ( inv (μ-f (inv-is-equiv is-equiv-f x) (inv-is-equiv is-equiv-f y))))

abstract
  is-iso-is-equiv-hom-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) (is-equiv-f : is-equiv (pr1 f)) →
    is-iso-Semi-Group G H f
  is-iso-is-equiv-hom-Semi-Group
    ( pair (pair G is-set-G) (pair μ-G assoc-G))
    ( pair (pair H is-set-H) (pair μ-H assoc-H))
    ( pair f μ-f) is-equiv-f =
    pair
      ( pair
        ( inv-is-equiv is-equiv-f)
        ( preserves-mul-inv-is-equiv-Semi-Group
          ( pair (pair G is-set-G) (pair μ-G assoc-G))
          ( pair (pair H is-set-H) (pair μ-H assoc-H))
          ( pair f μ-f) is-equiv-f))
      ( pair
        ( eq-htpy-hom-Semi-Group
          ( pair (pair H is-set-H) (pair μ-H assoc-H))
          ( pair (pair H is-set-H) (pair μ-H assoc-H))
          ( issec-inv-is-equiv is-equiv-f))
        ( eq-htpy-hom-Semi-Group
          ( pair (pair G is-set-G) (pair μ-G assoc-G))
          ( pair (pair G is-set-G) (pair μ-G assoc-G))
          ( isretr-inv-is-equiv is-equiv-f)))

abstract
  is-equiv-hom-is-iso-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) (is-iso-f : is-iso-Semi-Group G H f) →
    ( is-equiv (pr1 f))
  is-equiv-hom-is-iso-Semi-Group
    ( pair (pair G is-set-G) (pair μ-G assoc-G))
    ( pair (pair H is-set-H) (pair μ-H assoc-H))
    ( pair f μ-f)
    ( pair (pair g μ-g) (pair issec isretr)) =
    is-equiv-has-inverse g
      ( htpy-eq (ap pr1 issec))
      ( htpy-eq (ap pr1 isretr))

equiv-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
equiv-Semi-Group G H =
  Σ ( type-Semi-Group G ≃ type-Semi-Group H)
    ( λ e → preserves-mul G H (map-equiv e))

total-is-equiv-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
total-is-equiv-hom-Semi-Group G H =
  Σ (hom-Semi-Group G H) (λ f → is-equiv (map-hom-Semi-Group G H f))

preserves-mul' :
  { l1 l2 : Level} (G : Semi-Group l1) (H : UU-Set l2)
  ( μ-H : has-associative-mul H) →
  ( e : (type-Semi-Group G) ≃ (type-Set H)) →
  UU (l1 ⊔ l2)
preserves-mul' G H μ-H e = preserves-mul G (pair H μ-H) (map-equiv e)

equiv-Semi-Group' :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
equiv-Semi-Group' G H = equiv-Semi-Group G (pair (pr1 H) (pr2 H))

abstract
  equiv-iso-Semi-Group-equiv-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    equiv-Semi-Group' G H ≃ iso-Semi-Group G H
  equiv-iso-Semi-Group-equiv-Semi-Group G H =
    ( ( ( equiv-total-subtype
          ( λ f → is-subtype-is-equiv (map-hom-Semi-Group G H f))
          ( is-prop-is-iso-Semi-Group G H)
          ( is-iso-is-equiv-hom-Semi-Group G H)
          ( is-equiv-hom-is-iso-Semi-Group G H)) ∘e
        ( ( inv-equiv
            ( equiv-Σ-assoc
              ( type-Semi-Group G → type-Semi-Group H)
              ( preserves-mul G H)
              ( λ f → is-equiv (map-hom-Semi-Group G H f)))) ∘e
          ( equiv-tot
            ( λ f → equiv-swap-prod (is-equiv f) (preserves-mul G H f))))) ∘e
      ( equiv-Σ-assoc
        ( type-Semi-Group G → type-Semi-Group H)
        ( is-equiv)
        ( λ e → preserves-mul G H (map-equiv e)))) ∘e
    ( equiv-tr (equiv-Semi-Group G) (η-pair H))

center-total-preserves-mul-id :
  { l1 : Level} (G : Semi-Group l1) →
  Σ (has-associative-mul (pr1 G)) (λ μ → preserves-mul G (pair (pr1 G) μ) id)
center-total-preserves-mul-id (pair (pair G is-set-G) (pair μ-G assoc-G)) =
  pair (pair μ-G assoc-G) (λ x y → refl)

contraction-total-preserves-mul-id :
  { l1 : Level} (G : Semi-Group l1) →
  ( t : Σ ( has-associative-mul (pr1 G))
          ( λ μ → preserves-mul G (pair (pr1 G) μ) id)) →
  Id (center-total-preserves-mul-id G) t
contraction-total-preserves-mul-id
  ( pair (pair G is-set-G) (pair μ-G assoc-G))
  ( pair (pair μ-G' assoc-G') μ-id) =
  eq-subtype
    ( λ μ →
      is-prop-preserves-mul
        ( pair (pair G is-set-G) (pair μ-G assoc-G))
        ( pair (pair G is-set-G) μ) id)
    ( eq-subtype
      ( λ μ →
        is-prop-Π (λ x →
          is-prop-Π (λ y →
            is-prop-Π (λ z →
              is-set-G (μ (μ x y) z) (μ x (μ y z))))))
      ( eq-htpy (λ x → eq-htpy (λ y → μ-id x y))))

is-contr-total-preserves-mul-id :
  { l1 : Level} (G : Semi-Group l1) →
  is-contr (Σ (has-associative-mul (pr1 G)) (λ μ → preserves-mul G (pair (pr1 G) μ) id))
is-contr-total-preserves-mul-id G =
  pair
    ( center-total-preserves-mul-id G)
    ( contraction-total-preserves-mul-id G)

is-contr-total-equiv-Semi-Group :
  { l1 : Level} (G : Semi-Group l1) →
  is-contr (Σ (Semi-Group l1) (λ H → equiv-Semi-Group' G H))
is-contr-total-equiv-Semi-Group {l1} G =
  is-contr-total-Eq-structure
    ( preserves-mul' G)
    ( is-contr-total-Eq-substructure
      ( is-contr-total-equiv (type-Semi-Group G))
      ( is-prop-is-set)
      ( type-Semi-Group G)
      ( equiv-id (type-Semi-Group G))
      ( is-set-type-Semi-Group G))
    ( pair (pr1 G) (equiv-id (type-Semi-Group G)))
    ( is-contr-total-preserves-mul-id G)

is-contr-total-iso-Semi-Group :
  { l1 : Level} (G : Semi-Group l1) →
  is-contr (Σ (Semi-Group l1) (iso-Semi-Group G))
is-contr-total-iso-Semi-Group {l1} G =
  is-contr-equiv'
    ( Σ (Semi-Group l1) (λ H → equiv-Semi-Group' G H))
    ( equiv-tot (λ H → equiv-iso-Semi-Group-equiv-Semi-Group G H))
    ( is-contr-total-equiv-Semi-Group G)

iso-id-Semi-Group :
  { l1 : Level} (G : Semi-Group l1) → iso-Semi-Group G G
iso-id-Semi-Group G =
  pair
    ( id-Semi-Group G)
    ( pair
      ( id-Semi-Group G)
      ( pair
        ( left-unit-law-Semi-Group G G (id-Semi-Group G))
        ( right-unit-law-Semi-Group G G (id-Semi-Group G))))

iso-eq-Semi-Group :
  { l1 : Level} (G H : Semi-Group l1) → Id G H → iso-Semi-Group G H
iso-eq-Semi-Group G .G refl = iso-id-Semi-Group G

is-equiv-iso-eq-Semi-Group :
  { l1 : Level} (G H : Semi-Group l1) → is-equiv (iso-eq-Semi-Group G H)
is-equiv-iso-eq-Semi-Group G =
  fundamental-theorem-id G
    ( iso-id-Semi-Group G)
    ( is-contr-total-iso-Semi-Group G)
    ( iso-eq-Semi-Group G)

equiv-iso-eq-Semi-Group :
  { l1 : Level} (G H : Semi-Group l1) → Id G H ≃ iso-Semi-Group G H
equiv-iso-eq-Semi-Group G H =
  pair (iso-eq-Semi-Group G H) (is-equiv-iso-eq-Semi-Group G H)

eq-iso-Semi-Group :
  { l1 : Level} (G H : Semi-Group l1) → iso-Semi-Group G H → Id G H
eq-iso-Semi-Group G H = inv-is-equiv (is-equiv-iso-eq-Semi-Group G H)

{- Finally we show that isomorphic groups are equal. -}

iso-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) → UU (l1 ⊔ l2)
iso-Group G H =
  iso-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)

iso-id-Group :
  { l1 : Level} (G : Group l1) → iso-Group G G
iso-id-Group G = iso-id-Semi-Group (semi-group-Group G)

iso-eq-Group :
  { l1 : Level} (G H : Group l1) → Id G H → iso-Group G H
iso-eq-Group G .G refl = iso-id-Group G

abstract
  equiv-iso-eq-Group' :
    { l1 : Level} (G H : Group l1) → Id G H ≃ iso-Group G H
  equiv-iso-eq-Group' G H =
    ( equiv-iso-eq-Semi-Group
      ( semi-group-Group G)
      ( semi-group-Group H)) ∘e
    ( equiv-ap-pr1-is-subtype is-prop-is-group {s = G} {t = H})

abstract
  is-contr-total-iso-Group :
    { l1 : Level} (G : Group l1) → is-contr (Σ (Group l1) (iso-Group G))
  is-contr-total-iso-Group {l1} G =
    is-contr-equiv'
      ( Σ (Group l1) (Id G))
      ( equiv-tot (λ H → equiv-iso-eq-Group' G H))
      ( is-contr-total-path G)

is-equiv-iso-eq-Group :
  { l1 : Level} (G H : Group l1) → is-equiv (iso-eq-Group G H)
is-equiv-iso-eq-Group G =
  fundamental-theorem-id G
    ( iso-id-Group G)
    ( is-contr-total-iso-Group G)
    ( iso-eq-Group G)

eq-iso-Group :
  { l1 : Level} (G H : Group l1) → iso-Group G H → Id G H
eq-iso-Group G H = inv-is-equiv (is-equiv-iso-eq-Group G H)

-- Exercises

-- Exercise 10.1

tr-equiv-eq-ap : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {x y : A}
  (p : Id x y) → (map-equiv (equiv-eq (ap B p))) ~ tr B p
tr-equiv-eq-ap refl = htpy-refl

-- Exercise 10.2

subuniverse-is-contr :
  {i : Level} → subuniverse i i
subuniverse-is-contr {i} = pair is-contr is-subtype-is-contr

unit' :
  (i : Level) → UU i
unit' i = pr1 (Raise i unit)

abstract
  is-contr-unit' :
    (i : Level) → is-contr (unit' i)
  is-contr-unit' i =
    is-contr-equiv' unit (pr2 (Raise i unit)) is-contr-unit

abstract
  center-UU-contr :
    (i : Level) → total-subuniverse (subuniverse-is-contr {i})
  center-UU-contr i =
    pair (unit' i) (is-contr-unit' i)

  contraction-UU-contr :
    {i : Level} (A : Σ (UU i) is-contr) →
    Id (center-UU-contr i) A
  contraction-UU-contr (pair A is-contr-A) =
    eq-Eq-total-subuniverse subuniverse-is-contr
      ( equiv-is-contr (is-contr-unit' _) is-contr-A)

abstract
  is-contr-UU-contr : (i : Level) → is-contr (Σ (UU i) is-contr)
  is-contr-UU-contr i =
    pair (center-UU-contr i) (contraction-UU-contr)

is-trunc-UU-trunc :
  (k : 𝕋) (i : Level) → is-trunc (succ-𝕋 k) (Σ (UU i) (is-trunc k))
is-trunc-UU-trunc k i X Y =
  is-trunc-is-equiv k
    ( Id (pr1 X) (pr1 Y))
    ( ap pr1)
    ( is-emb-pr1-is-subtype
      ( is-prop-is-trunc k) X Y)
    ( is-trunc-is-equiv k
      ( (pr1 X) ≃ (pr1 Y))
      ( equiv-eq)
      ( univalence (pr1 X) (pr1 Y))
      ( is-trunc-equiv-is-trunc k (pr2 X) (pr2 Y)))

ev-true-false :
  {l : Level} (A : UU l) → (f : bool → A) → A × A
ev-true-false A f = pair (f true) (f false)

map-universal-property-bool :
  {l : Level} {A : UU l} →
  A × A → (bool → A)
map-universal-property-bool (pair x y) true = x
map-universal-property-bool (pair x y) false = y

issec-map-universal-property-bool :
  {l : Level} {A : UU l} →
  ((ev-true-false A) ∘ map-universal-property-bool) ~ id
issec-map-universal-property-bool (pair x y) =
  eq-pair-triv (pair refl refl)

isretr-map-universal-property-bool' :
  {l : Level} {A : UU l} (f : bool → A) →
  (map-universal-property-bool (ev-true-false A f)) ~ f
isretr-map-universal-property-bool' f true = refl
isretr-map-universal-property-bool' f false = refl

isretr-map-universal-property-bool :
  {l : Level} {A : UU l} →
  (map-universal-property-bool ∘ (ev-true-false A)) ~ id
isretr-map-universal-property-bool f =
  eq-htpy (isretr-map-universal-property-bool' f)

universal-property-bool :
  {l : Level} (A : UU l) →
  is-equiv (λ (f : bool → A) → pair (f true) (f false))
universal-property-bool A =
  is-equiv-has-inverse
    map-universal-property-bool
    issec-map-universal-property-bool
    isretr-map-universal-property-bool

ev-true :
  {l : Level} {A : UU l} → (bool → A) → A
ev-true f = f true

triangle-ev-true :
  {l : Level} (A : UU l) →
  (ev-true) ~ (pr1 ∘ (ev-true-false A))
triangle-ev-true A = htpy-refl

aut-bool-bool :
  bool → (bool ≃ bool)
aut-bool-bool true = equiv-id bool
aut-bool-bool false = equiv-neg-𝟚

bool-aut-bool :
  (bool ≃ bool) → bool
bool-aut-bool e = map-equiv e true

decide-true-false :
  (b : bool) → coprod (Id b true) (Id b false)
decide-true-false true = inl refl
decide-true-false false = inr refl

eq-false :
  (b : bool) → (¬ (Id b true)) → (Id b false)
eq-false true p = ind-empty (p refl)
eq-false false p = refl

eq-true :
  (b : bool) → (¬ (Id b false)) → Id b true
eq-true true p = refl
eq-true false p = ind-empty (p refl)

eq-false-equiv' :
  (e : bool ≃ bool) → Id (map-equiv e true) true →
  is-decidable (Id (map-equiv e false) false) → Id (map-equiv e false) false
eq-false-equiv' e p (inl q) = q
eq-false-equiv' e p (inr x) =
  ind-empty
    ( Eq-𝟚-eq true false
      ( ap pr1
        ( is-prop-is-contr'
          ( is-contr-map-is-equiv (is-equiv-map-equiv e) true)
          ( pair true p)
          ( pair false (eq-true (map-equiv e false) x)))))

eq-false-equiv :
  (e : bool ≃ bool) → Id (map-equiv e true) true → Id (map-equiv e false) false
eq-false-equiv e p =
  eq-false-equiv' e p (has-decidable-equality-𝟚 (map-equiv e false) false)

{-
eq-true-equiv :
  (e : bool ≃ bool) →
  ¬ (Id (map-equiv e true) true) → Id (map-equiv e false) true
eq-true-equiv e f = {!!}

issec-bool-aut-bool' :
  ( e : bool ≃ bool) (d : is-decidable (Id (map-equiv e true) true)) →
  htpy-equiv (aut-bool-bool (bool-aut-bool e)) e
issec-bool-aut-bool' e (inl p) true =
  ( htpy-equiv-eq (ap aut-bool-bool p) true) ∙ (inv p)
issec-bool-aut-bool' e (inl p) false =
  ( htpy-equiv-eq (ap aut-bool-bool p) false) ∙
  ( inv (eq-false-equiv e p))
issec-bool-aut-bool' e (inr f) true =
  ( htpy-equiv-eq
    ( ap aut-bool-bool (eq-false (map-equiv e true) f)) true) ∙
  ( inv (eq-false (map-equiv e true) f))
issec-bool-aut-bool' e (inr f) false =
  ( htpy-equiv-eq (ap aut-bool-bool {!eq-true-equiv e ?!}) {!!}) ∙
  ( inv {!!})

issec-bool-aut-bool :
  (aut-bool-bool ∘ bool-aut-bool) ~ id
issec-bool-aut-bool e =
  eq-htpy-equiv
    ( issec-bool-aut-bool' e
      ( has-decidable-equality-𝟚 (map-equiv e true) true))
-}

-- Exercise

unit-classical-Prop : classical-Prop lzero
unit-classical-Prop =
  pair (pair {!!} {!!}) {!!}

raise-unit-classical-Prop :
  (l : Level) → classical-Prop l
raise-unit-classical-Prop l =
  pair
    ( pair
      ( raise l unit)
      ( is-prop-is-equiv' unit
        ( map-raise l unit)
        ( is-equiv-map-raise l unit)
        ( is-prop-unit)))
    ( inl (map-raise l unit star))

bool-classical-Prop :
  (l : Level) → classical-Prop l → bool
bool-classical-Prop l (pair P (inl x)) = true
bool-classical-Prop l (pair P (inr x)) = false

classical-Prop-bool :
  (l : Level) → bool → classical-Prop l
classical-Prop-bool l true = raise-unit-classical-Prop l
classical-Prop-bool l false = {!!}

-- Exercise

{- We show that group homomorphisms preserve the unit. -}

preserves-unit :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f : hom-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)) →
  UU l2
preserves-unit G H f =
  Id (map-hom-Group G H f (unit-Group G)) (unit-Group H)

abstract
  preserves-unit-group-hom :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f : hom-Group G H) → preserves-unit G H f
  preserves-unit-group-hom
    ( pair ( pair (pair G is-set-G) (pair μ-G assoc-G))
           ( pair ( pair e-G (pair left-unit-G right-unit-G))
                  ( pair i-G (pair left-inv-G right-inv-G))))
    ( pair ( pair (pair H is-set-H) (pair μ-H assoc-H))
           ( pair ( pair e-H (pair left-unit-H right-unit-H))
                  ( pair i-H (pair left-inv-H right-inv-H))))
    ( pair f μ-f) =
    ( inv (left-unit-H (f e-G))) ∙
    ( ( ap (λ x → μ-H x (f e-G)) (inv (left-inv-H (f e-G)))) ∙
      ( ( assoc-H (i-H (f e-G)) (f e-G) (f e-G)) ∙
        ( ( ap (μ-H (i-H (f e-G))) (inv (μ-f e-G e-G))) ∙
          ( ( ap (λ x → μ-H (i-H (f e-G)) (f x)) (left-unit-G e-G)) ∙
            ( left-inv-H (f e-G))))))

{- We show that group homomorphisms preserve inverses. -}

preserves-inverses :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f : hom-Group G H) → UU (l1 ⊔ l2)
preserves-inverses G H f =
  ( x : type-Group G) →
  Id ( map-hom-Group G H f (inv-Group G x))
     ( inv-Group H (map-hom-Group G H f x))

abstract
  preserves-inverses-group-hom' :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f : hom-Group G H) →
    preserves-unit G H f → preserves-inverses G H f
  preserves-inverses-group-hom'
    ( pair ( pair (pair G is-set-G) (pair μ-G assoc-G))
           ( pair ( pair e-G (pair left-unit-G right-unit-G))
                  ( pair i-G (pair left-inv-G right-inv-G))))
    ( pair ( pair (pair H is-set-H) (pair μ-H assoc-H))
           ( pair ( pair e-H (pair left-unit-H right-unit-H))
                  ( pair i-H (pair left-inv-H right-inv-H))))
    ( pair f μ-f) preserves-unit-f x =
    ( inv ( right-unit-H (f (i-G x)))) ∙
    ( ( ap (μ-H (f (i-G x))) (inv (right-inv-H (f x)))) ∙
      ( ( inv (assoc-H (f (i-G x)) (f x) (i-H (f x)))) ∙
        ( ( inv (ap (λ y → μ-H y (i-H (f x))) (μ-f (i-G x) x))) ∙
          ( ( ap (λ y → μ-H (f y) (i-H (f x))) (left-inv-G x)) ∙
            ( ( ap
                ( λ y → μ-H y (i-H (f x)))
                ( preserves-unit-f)) ∙
              ( left-unit-H (i-H (f x))))))))

abstract
  preserves-inverses-group-hom :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f : hom-Group G H) → preserves-inverses G H f
  preserves-inverses-group-hom G H f =
    preserves-inverses-group-hom' G H f (preserves-unit-group-hom G H f)

hom-Group' :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) → UU (l1 ⊔ l2)
hom-Group' G H =
  Σ ( hom-Group G H) (λ f →
    ( preserves-unit G H f) × (preserves-inverses G H f))

preserves-all-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  hom-Group G H → hom-Group' G H
preserves-all-hom-Group G H f =
  pair f
    ( pair
      ( preserves-unit-group-hom G H f)
      ( preserves-inverses-group-hom G H f))

-- Exercise

{-
hom-mul-Group :
  {l : Level} (G : Group l) →
  hom-Group G Aut
-}

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro